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;                             /* Use counter of hpet for time keeping, otherwise PIT */
+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;
            print_symbol("rip %s\n", regs->rip);
            if (vxtime.mode == VXTIME_TSC && vxtime.hpet_address) {
                    printk(KERN_WARNING "Falling back to HPET\n");
-                   vxtime.last = hpet_readl(HPET_T0_CMP) - hpet_tick;
+                   if (hpet_use_timer)
+                       vxtime.last = hpet_readl(HPET_T0_CMP) - hpet_tick;
+                   else
+                       vxtime.last = hpet_readl(HPET_COUNTER);
                    vxtime.mode = VXTIME_HPET;
                    do_gettimeoffset = do_gettimeoffset_hpet;
            }
                notsc = 1;
        if (vxtime.hpet_address && notsc) {
                timetype = hpet_use_timer ? "HPET" : "PIT/HPET";
-               vxtime.last = hpet_readl(HPET_T0_CMP) - hpet_tick;
+               if (hpet_use_timer)
+                       vxtime.last = hpet_readl(HPET_T0_CMP) - hpet_tick;
+               else
+                       vxtime.last = hpet_readl(HPET_COUNTER);
                vxtime.mode = VXTIME_HPET;
                do_gettimeoffset = do_gettimeoffset_hpet;
 #ifdef CONFIG_X86_PM_TIMER
 
 extern int hpet_rtc_timer_init(void);
 extern int oem_force_hpet_timer(void);
 
+extern int hpet_use_timer;
+
 #ifdef CONFIG_HPET_EMULATE_RTC
 extern int hpet_mask_rtc_irq_bit(unsigned long bit_mask);
 extern int hpet_set_rtc_irq_bit(unsigned long bit_mask);