diff --git a/doc/developer-guides/hld/hv-timer.rst b/doc/developer-guides/hld/hv-timer.rst
index 8a4f07735..b31e3ace3 100644
--- a/doc/developer-guides/hld/hv-timer.rst
+++ b/doc/developer-guides/hld/hv-timer.rst
@@ -45,3 +45,17 @@ Interfaces Design
 .. doxygenfunction:: calibrate_tsc
    :project: Project ACRN
 
+.. doxygenfunction:: us_to_ticks
+   :project: Project ACRN
+
+.. doxygenfunction:: ticks_to_us
+   :project: Project ACRN
+
+.. doxygenfunction:: ticks_to_ms
+   :project: Project ACRN
+
+.. doxygenfunction:: rdtsc
+   :project: Project ACRN
+
+.. doxygenfunction:: get_tsc_khz
+   :project: Project ACRN
diff --git a/hypervisor/arch/x86/guest/vcpuid.c b/hypervisor/arch/x86/guest/vcpuid.c
index f755ac91b..03488fe36 100644
--- a/hypervisor/arch/x86/guest/vcpuid.c
+++ b/hypervisor/arch/x86/guest/vcpuid.c
@@ -139,7 +139,7 @@ static void init_vcpuid_entry(uint32_t leaf, uint32_t subleaf,
 			cpuid_subleaf(leaf, subleaf, &entry->eax, &entry->ebx, &entry->ecx, &entry->edx);
 		} else {
 			/* Use the tsc to derive the emulated 0x16U cpuid. */
-			entry->eax = (uint32_t) (tsc_khz / 1000U);
+			entry->eax = (uint32_t) (get_tsc_khz() / 1000U);
 			entry->ebx = entry->eax;
 			/* Bus frequency: hard coded to 100M */
 			entry->ecx = 100U;
@@ -178,7 +178,7 @@ static void init_vcpuid_entry(uint32_t leaf, uint32_t subleaf,
 	 * EBX, ECX, EDX: RESERVED (reserved fields are set to zero).
 	 */
 	case 0x40000010U:
-		entry->eax = tsc_khz;
+		entry->eax = get_tsc_khz();
 		entry->ebx = 0U;
 		entry->ecx = 0U;
 		entry->edx = 0U;
diff --git a/hypervisor/arch/x86/timer.c b/hypervisor/arch/x86/timer.c
index 6a536e599..c713333fa 100644
--- a/hypervisor/arch/x86/timer.c
+++ b/hypervisor/arch/x86/timer.c
@@ -16,7 +16,15 @@
 #define CAL_MS			10U
 #define MIN_TIMER_PERIOD_US	500U
 
-uint32_t tsc_khz = 0U;
+static uint32_t tsc_khz = 0U;
+
+uint64_t rdtsc(void)
+{
+	uint32_t lo, hi;
+
+	asm volatile("rdtsc" : "=a" (lo), "=d" (hi));
+	return ((uint64_t)hi << 32U) | lo;
+}
 
 static void run_timer(const struct hv_timer *timer)
 {
@@ -283,3 +291,28 @@ void calibrate_tsc(void)
 	tsc_khz = (uint32_t)(tsc_hz / 1000UL);
 	printf("%s, tsc_khz=%lu\n", __func__, tsc_khz);
 }
+
+uint32_t get_tsc_khz(void)
+{
+	return tsc_khz;
+}
+
+/**
+ * Frequency of TSC in KHz (where 1KHz = 1000Hz). Only valid after
+ * calibrate_tsc() returns.
+ */
+
+uint64_t us_to_ticks(uint32_t us)
+{
+	return (((uint64_t)us * (uint64_t)tsc_khz) / 1000UL);
+}
+
+uint64_t ticks_to_us(uint64_t ticks)
+{
+	return (ticks * 1000UL) / (uint64_t)tsc_khz;
+}
+
+uint64_t ticks_to_ms(uint64_t ticks)
+{
+	return ticks / (uint64_t)tsc_khz;
+}
diff --git a/hypervisor/include/arch/x86/timer.h b/hypervisor/include/arch/x86/timer.h
index 9cdce7df3..80e38658e 100644
--- a/hypervisor/include/arch/x86/timer.h
+++ b/hypervisor/include/arch/x86/timer.h
@@ -8,7 +8,6 @@
 #define TIMER_H
 
 #include <list.h>
-#include <rtl.h>
 
 /**
  * @brief Timer
@@ -48,6 +47,36 @@ struct hv_timer {
 
 /* External Interfaces */
 
+#define CYCLES_PER_MS	us_to_ticks(1000U)
+
+/**
+ * @brief convert us to ticks.
+ *
+ * @return ticks
+ */
+uint64_t us_to_ticks(uint32_t us);
+
+/**
+ * @brief convert ticks to us.
+ *
+ * @return microsecond
+ */
+uint64_t ticks_to_us(uint64_t ticks);
+
+/**
+ * @brief convert ticks to ms.
+ *
+ * @return millisecond
+ */
+uint64_t ticks_to_ms(uint64_t ticks);
+
+/**
+ * @brief read tsc.
+ *
+ * @return tsc value
+ */
+uint64_t rdtsc(void);
+
 /**
  * @brief Initialize a timer structure.
  *
@@ -138,6 +167,13 @@ void timer_init(void);
  */
 void calibrate_tsc(void);
 
+/**
+ * @brief  Get tsc.
+ *
+ * @return tsc(KHz)
+ */
+uint32_t get_tsc_khz(void);
+
 /**
  * @}
  */
diff --git a/hypervisor/include/lib/rtl.h b/hypervisor/include/lib/rtl.h
index a3688cc1c..2d5464f9f 100644
--- a/hypervisor/include/lib/rtl.h
+++ b/hypervisor/include/lib/rtl.h
@@ -43,34 +43,4 @@ uint64_t strtoul_hex(const char *nptr);
 char *strstr_s(const char *str1, size_t maxlen1,
 			const char *str2, size_t maxlen2);
 
-/**
- * Frequency of TSC in KHz (where 1KHz = 1000Hz). Only valid after
- * calibrate_tsc() returns.
- */
-extern uint32_t tsc_khz;
-
-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)
-{
-	uint32_t lo, hi;
-
-	asm volatile("rdtsc" : "=a" (lo), "=d" (hi));
-	return ((uint64_t)hi << 32U) | lo;
-}
 #endif /* RTL_H */