unsigned int cpu_khz;                                  /* TSC clocks / usec, not used here */
 static unsigned long hpet_period;                      /* fsecs / HPET clock */
 unsigned long hpet_tick;                               /* HPET clocks / interrupt */
-static int hpet_use_timer;
+static int hpet_use_timer;                             /* Use counter of hpet for time keeping, otherwise PIT */
 unsigned long vxtime_hz = PIT_TICK_RATE;
 int report_lost_ticks;                         /* command line option */
 unsigned long long monotonic_base;
        if (!hpet_init())
                 vxtime_hz = (1000000000000000L + hpet_period / 2) /
                        hpet_period;
+       else
+               vxtime.hpet_address = 0;
 
        if (hpet_use_timer) {
                cpu_khz = hpet_calibrate_tsc();