diff --git a/bochs/cpu/cpu.h b/bochs/cpu/cpu.h
index 9cf57adf8..bfebd2bc0 100644
--- a/bochs/cpu/cpu.h
+++ b/bochs/cpu/cpu.h
@@ -4679,9 +4679,7 @@ public: // for now...
 #if BX_CPU_LEVEL >= 5
   BX_SMF Bit64u get_TSC();
   BX_SMF void   set_TSC(Bit64u tsc);
-#if BX_SUPPORT_VMX || BX_SUPPORT_SVM
-  BX_SMF Bit64u get_TSC_VMXAdjust(Bit64u tsc);
-#endif
+  BX_SMF Bit64u get_Virtual_TSC(); // takes into account VMX or SVM adjustments
 #endif
 
 #if BX_SUPPORT_PKEYS
diff --git a/bochs/cpu/msr.cc b/bochs/cpu/msr.cc
index 190c034ac..4ea9f607b 100644
--- a/bochs/cpu/msr.cc
+++ b/bochs/cpu/msr.cc
@@ -155,10 +155,7 @@ bool BX_CPP_AttrRegparmN(2) BX_CPU_C::rdmsr(Bit32u index, Bit64u *msr)
 #endif
 
     case BX_MSR_TSC:
-      val64 = BX_CPU_THIS_PTR get_TSC();
-#if BX_SUPPORT_SVM || BX_SUPPORT_VMX
-      val64 = BX_CPU_THIS_PTR get_TSC_VMXAdjust(val64);
-#endif
+      val64 = BX_CPU_THIS_PTR get_Virtual_TSC();
       break;
 
     case BX_MSR_TSC_ADJUST:
diff --git a/bochs/cpu/proc_ctrl.cc b/bochs/cpu/proc_ctrl.cc
index 40b71043f..ec8edbbf6 100644
--- a/bochs/cpu/proc_ctrl.cc
+++ b/bochs/cpu/proc_ctrl.cc
@@ -646,11 +646,15 @@ Bit64u BX_CPU_C::get_TSC(void)
 }
 
 #if BX_SUPPORT_VMX || BX_SUPPORT_SVM
-Bit64u BX_CPU_C::get_TSC_VMXAdjust(Bit64u tsc)
+Bit64u BX_CPU_C::get_Virtual_TSC()
 {
+  Bit64u tsc = BX_CPU_THIS_PTR get_TSC();
 #if BX_SUPPORT_VMX
   if (BX_CPU_THIS_PTR in_vmx_guest) {
     if (VMEXIT(VMX_VM_EXEC_CTRL1_TSC_OFFSET) && SECONDARY_VMEXEC_CONTROL(VMX_VM_EXEC_CTRL2_TSC_SCALING)) {
+      // RDTSC first computes the product of the value of the IA32_TIME_STAMP_COUNTER MSR and
+      // the value of the TSC multiplier. It then shifts the value of the product right 48 bits and loads 
+      // EAX:EDX with <the sum of that shifted value and the value of the TSC offset>.
       Bit128u product_128;
       long_mul(&product_128,tsc,BX_CPU_THIS_PTR vmcs.tsc_multiplier);
       tsc = (product_128.lo >> 48) | (product_128.hi << 16);   // tsc = (uint64) (long128(tsc_value * tsc_multiplier) >> 48);
@@ -694,11 +698,7 @@ void BX_CPP_AttrRegparmN(1) BX_CPU_C::RDTSC(bxInstruction_c *i)
     if (SVM_INTERCEPT(SVM_INTERCEPT0_RDTSC)) Svm_Vmexit(SVM_VMEXIT_RDTSC);
 #endif
 
-  // return ticks
-  Bit64u ticks = BX_CPU_THIS_PTR get_TSC();
-#if BX_SUPPORT_SVM || BX_SUPPORT_VMX
-  ticks = BX_CPU_THIS_PTR get_TSC_VMXAdjust(ticks);
-#endif
+  Bit64u ticks = BX_CPU_THIS_PTR get_Virtual_TSC();
 
   RAX = GET32L(ticks);
   RDX = GET32H(ticks);
@@ -741,11 +741,7 @@ void BX_CPP_AttrRegparmN(1) BX_CPU_C::RDTSCP(bxInstruction_c *i)
     if (SVM_INTERCEPT(SVM_INTERCEPT1_RDTSCP)) Svm_Vmexit(SVM_VMEXIT_RDTSCP);
 #endif
 
-  // return ticks
-  Bit64u ticks = BX_CPU_THIS_PTR get_TSC();
-#if BX_SUPPORT_SVM || BX_SUPPORT_VMX
-  ticks = BX_CPU_THIS_PTR get_TSC_VMXAdjust(ticks);
-#endif
+  Bit64u ticks = BX_CPU_THIS_PTR get_Virtual_TSC();
 
   RAX = GET32L(ticks);
   RDX = GET32H(ticks);
diff --git a/bochs/pc_system.h b/bochs/pc_system.h
index 4eb4f8bfa..a0947b456 100644
--- a/bochs/pc_system.h
+++ b/bochs/pc_system.h
@@ -122,8 +122,8 @@ public:
 
   int register_timer_ticks(void* this_ptr, bx_timer_handler_t, Bit64u ticks,
                            bool continuous, bool active, const char *id);
-  void activate_timer_ticks(unsigned index, Bit64u instructions,
-                            bool continuous);
+  void activate_timer_ticks(unsigned index, Bit64u instructions, bool continuous);
+
   Bit64u time_usec();
   Bit64u time_nsec();
   Bit64u time_usec_sequential();