diff --git a/hypervisor/arch/x86/cpu.c b/hypervisor/arch/x86/cpu.c
index 7d7c7534d..56826adc5 100644
--- a/hypervisor/arch/x86/cpu.c
+++ b/hypervisor/arch/x86/cpu.c
@@ -497,12 +497,12 @@ static void bsp_boot_post(void)
 		pr_acrnlog("HV version %d.%d-rc%d-%s-%s %s build by %s, start time %lluus",
 			HV_MAJOR_VERSION, HV_MINOR_VERSION, HV_RC_VERSION,
 			HV_BUILD_TIME, HV_BUILD_VERSION, HV_BUILD_TYPE,
-			HV_BUILD_USER, TICKS_TO_US(start_tsc));
+			HV_BUILD_USER, ticks_to_us(start_tsc));
 	else
 		pr_acrnlog("HV version %d.%d-%s-%s %s build by %s, start time %lluus",
 			HV_MAJOR_VERSION, HV_MINOR_VERSION,
 			HV_BUILD_TIME, HV_BUILD_VERSION, HV_BUILD_TYPE,
-			HV_BUILD_USER, TICKS_TO_US(start_tsc));
+			HV_BUILD_USER, ticks_to_us(start_tsc));
 
 	pr_acrnlog("API version %d.%d",
 			HV_API_MAJOR_VERSION, HV_API_MINOR_VERSION);
diff --git a/hypervisor/arch/x86/cpuid.c b/hypervisor/arch/x86/cpuid.c
index 3d37106e9..0d6eadd53 100644
--- a/hypervisor/arch/x86/cpuid.c
+++ b/hypervisor/arch/x86/cpuid.c
@@ -139,7 +139,7 @@ static void init_vcpuid_entry(__unused struct vm *vm,
 	 * EBX, ECX, EDX: RESERVED (reserved fields are set to zero).
 	 */
 	case 0x40000010:
-		entry->eax = (uint32_t)(tsc_hz / 1000);
+		entry->eax = tsc_khz;
 		entry->ebx = 0;
 		entry->ecx = 0;
 		entry->edx = 0;
diff --git a/hypervisor/arch/x86/timer.c b/hypervisor/arch/x86/timer.c
index a54701029..42cf75712 100644
--- a/hypervisor/arch/x86/timer.c
+++ b/hypervisor/arch/x86/timer.c
@@ -11,7 +11,7 @@
 #define CAL_MS			10
 #define MIN_TIMER_PERIOD_US	500
 
-uint64_t tsc_hz = 1000000000;
+uint32_t tsc_khz = 0U;
 
 static void run_timer(struct timer *timer)
 {
@@ -79,7 +79,7 @@ int add_timer(struct timer *timer)
 	/* limit minimal periodic timer cycle period */
 	if (timer->mode == TICK_MODE_PERIODIC)
 		timer->period_in_cycle = max(timer->period_in_cycle,
-				US_TO_TICKS(MIN_TIMER_PERIOD_US));
+				us_to_ticks(MIN_TIMER_PERIOD_US));
 
 	pcpu_id  = get_cpu_id();
 	cpu_timer = &per_cpu(cpu_timers, pcpu_id);
@@ -285,8 +285,10 @@ static uint64_t native_calibrate_tsc(void)
 
 void calibrate_tsc(void)
 {
+	uint64_t tsc_hz;
 	tsc_hz = native_calibrate_tsc();
 	if (tsc_hz == 0U)
 		tsc_hz = pit_calibrate_tsc(CAL_MS);
-	printf("%s, tsc_hz=%lu\n", __func__, tsc_hz);
+	tsc_khz = (uint32_t)(tsc_hz / 1000UL);
+	printf("%s, tsc_khz=%lu\n", __func__, tsc_khz);
 }
diff --git a/hypervisor/common/hv_main.c b/hypervisor/common/hv_main.c
index 44e612aef..2028b5030 100644
--- a/hypervisor/common/hv_main.c
+++ b/hypervisor/common/hv_main.c
@@ -148,7 +148,7 @@ void get_vmexit_profile(char *str, int str_max)
 	int len, size = str_max;
 
 	len = snprintf(str, size, "\r\nNow(us) = %16lld\r\n",
-			TICKS_TO_US(rdtsc()));
+			ticks_to_us(rdtsc()));
 	size -= len;
 	str += len;
 
@@ -169,7 +169,7 @@ void get_vmexit_profile(char *str, int str_max)
 		for (cpu = 0; cpu < phys_cpu_num; cpu++) {
 			len = snprintf(str, size, "\t%10lld\t%10lld",
 				per_cpu(vmexit_cnt, cpu)[i],
-				TICKS_TO_US(per_cpu(vmexit_time, cpu)[i]));
+				ticks_to_us(per_cpu(vmexit_time, cpu)[i]));
 			size -= len;
 			str += len;
 		}
diff --git a/hypervisor/debug/logmsg.c b/hypervisor/debug/logmsg.c
index beaa035fb..44cce6d11 100644
--- a/hypervisor/debug/logmsg.c
+++ b/hypervisor/debug/logmsg.c
@@ -101,7 +101,7 @@ void do_logmsg(uint32_t severity, const char *fmt, ...)
 	timestamp = rdtsc();
 
 	/* Scale time-stamp appropriately */
-	timestamp = TICKS_TO_US(timestamp);
+	timestamp = ticks_to_us(timestamp);
 
 	/* Get CPU ID */
 	cpu_id = get_cpu_id();
diff --git a/hypervisor/include/lib/rtl.h b/hypervisor/include/lib/rtl.h
index 5d4a14ca3..ff020f11a 100644
--- a/hypervisor/include/lib/rtl.h
+++ b/hypervisor/include/lib/rtl.h
@@ -44,12 +44,28 @@ int atoi(const char *str);
 long strtol_deci(const char *nptr);
 uint64_t strtoul_hex(const char *nptr);
 
-extern uint64_t tsc_hz;
-#define US_TO_TICKS(x)	((x) * tsc_hz / 1000000UL)
-#define CYCLES_PER_MS	US_TO_TICKS(1000UL)
+/**
+ * Frequency of TSC in KHz (where 1KHz = 1000Hz). Only valid after
+ * calibrate_tsc() returns.
+ */
+extern uint32_t tsc_khz;
 
-#define TICKS_TO_US(x)	((((x) * (1000000UL >> 8)) / tsc_hz) << 8)
-#define TICKS_TO_MS(x)	(((x) * 1000UL) / tsc_hz)
+static inline uint64_t us_to_ticks(uint32_t us)
+{
+	return ((uint64_t)us * (uint64_t)tsc_khz / 1000UL);
+}
+
+#define CYCLES_PER_MS	us_to_ticks(1000U)
+
+static inline uint64_t ticks_to_us(uint64_t ticks)
+{
+	return (ticks * 1000UL) / (uint64_t)tsc_khz;
+}
+
+static inline uint64_t ticks_to_ms(uint64_t ticks)
+{
+	return ticks / (uint64_t)tsc_khz;
+}
 
 static inline uint64_t rdtsc(void)
 {
diff --git a/hypervisor/lib/udelay.c b/hypervisor/lib/udelay.c
index efdca430d..9ba1fa062 100644
--- a/hypervisor/lib/udelay.c
+++ b/hypervisor/lib/udelay.c
@@ -11,7 +11,7 @@ void udelay(uint32_t us)
 	uint64_t dest_tsc, delta_tsc;
 
 	/* Calculate number of ticks to wait */
-	delta_tsc = US_TO_TICKS(us);
+	delta_tsc = us_to_ticks(us);
 	dest_tsc = rdtsc() + delta_tsc;
 
 	/* Loop until time expired */