diff --git a/xen/arch/x86/hvm/hvm.c b/xen/arch/x86/hvm/hvm.c
index fb2d81b1ee..556071cff1 100644
--- a/xen/arch/x86/hvm/hvm.c
+++ b/xen/arch/x86/hvm/hvm.c
@@ -60,7 +60,6 @@
 #include <asm/hvm/nestedhvm.h>
 #include <asm/hvm/event.h>
 #include <asm/hvm/vmx/vmx.h>
-#include <asm/hvm/svm/svm.h> /* for cpu_has_tsc_ratio */
 #include <asm/altp2m.h>
 #include <asm/mtrr.h>
 #include <asm/apic.h>
@@ -312,8 +311,8 @@ void hvm_set_guest_tsc_fixed(struct vcpu *v, u64 guest_tsc, u64 at_tsc)
     else
     {
         tsc = at_tsc ?: rdtsc();
-        if ( cpu_has_tsc_ratio )
-            tsc = hvm_funcs.scale_tsc(v, tsc);
+        if ( hvm_tsc_scaling_supported )
+            tsc = hvm_funcs.tsc_scaling.scale_tsc(v, tsc);
     }
 
     delta_tsc = guest_tsc - tsc;
@@ -344,8 +343,8 @@ u64 hvm_get_guest_tsc_fixed(struct vcpu *v, uint64_t at_tsc)
     else
     {
         tsc = at_tsc ?: rdtsc();
-        if ( cpu_has_tsc_ratio )
-            tsc = hvm_funcs.scale_tsc(v, tsc);
+        if ( hvm_tsc_scaling_supported )
+            tsc = hvm_funcs.tsc_scaling.scale_tsc(v, tsc);
     }
 
     return tsc + v->arch.hvm_vcpu.cache_tsc_offset;
diff --git a/xen/arch/x86/hvm/svm/svm.c b/xen/arch/x86/hvm/svm/svm.c
index e62dfa1cf1..b22d4a1b3a 100644
--- a/xen/arch/x86/hvm/svm/svm.c
+++ b/xen/arch/x86/hvm/svm/svm.c
@@ -1465,6 +1465,9 @@ const struct hvm_function_table * __init start_svm(void)
     if ( !cpu_has_svm_nrips )
         clear_bit(SVM_FEATURE_DECODEASSISTS, &svm_feature_flags);
 
+    if ( cpu_has_tsc_ratio )
+        svm_function_table.tsc_scaling.ratio_frac_bits = 32;
+
 #define P(p,s) if ( p ) { printk(" - %s\n", s); printed = 1; }
     P(cpu_has_svm_npt, "Nested Page Tables (NPT)");
     P(cpu_has_svm_lbrv, "Last Branch Record (LBR) Virtualisation");
@@ -2286,7 +2289,10 @@ static struct hvm_function_table __initdata svm_function_table = {
     .nhvm_intr_blocked = nsvm_intr_blocked,
     .nhvm_hap_walk_L1_p2m = nsvm_hap_walk_L1_p2m,
 
-    .scale_tsc            = svm_scale_tsc,
+    .tsc_scaling = {
+        .max_ratio = ~TSC_RATIO_RSVD_BITS,
+        .scale_tsc = svm_scale_tsc,
+    },
 };
 
 void svm_vmexit_handler(struct cpu_user_regs *regs)
diff --git a/xen/arch/x86/time.c b/xen/arch/x86/time.c
index 5819b9ffdb..2248dfa63f 100644
--- a/xen/arch/x86/time.c
+++ b/xen/arch/x86/time.c
@@ -37,7 +37,6 @@
 #include <asm/hpet.h>
 #include <io_ports.h>
 #include <asm/setup.h> /* for early_time_init */
-#include <asm/hvm/svm/svm.h> /* for cpu_has_tsc_ratio */
 #include <public/arch-x86/cpuid.h>
 
 /* opt_clocksource: Force clocksource to one of: pit, hpet, acpi. */
@@ -815,9 +814,10 @@ static void __update_vcpu_system_time(struct vcpu *v, int force)
     }
     else
     {
-        if ( has_hvm_container_domain(d) && cpu_has_tsc_ratio )
+        if ( has_hvm_container_domain(d) && hvm_tsc_scaling_supported )
         {
-            tsc_stamp            = hvm_funcs.scale_tsc(v, t->local_tsc_stamp);
+            tsc_stamp            =
+                hvm_funcs.tsc_scaling.scale_tsc(v, t->local_tsc_stamp);
             _u.tsc_to_system_mul = d->arch.vtsc_to_ns.mul_frac;
             _u.tsc_shift         = d->arch.vtsc_to_ns.shift;
         }
@@ -1758,7 +1758,7 @@ void tsc_get_info(struct domain *d, uint32_t *tsc_mode,
                   uint32_t *incarnation)
 {
     bool_t enable_tsc_scaling = has_hvm_container_domain(d) &&
-                                cpu_has_tsc_ratio && !d->arch.vtsc;
+                                hvm_tsc_scaling_supported && !d->arch.vtsc;
 
     *incarnation = d->arch.incarnation;
     *tsc_mode = d->arch.tsc_mode;
@@ -1865,7 +1865,7 @@ void tsc_set_info(struct domain *d,
          */
         if ( tsc_mode == TSC_MODE_DEFAULT && host_tsc_is_safe() &&
              (has_hvm_container_domain(d) ?
-              d->arch.tsc_khz == cpu_khz || cpu_has_tsc_ratio :
+              d->arch.tsc_khz == cpu_khz || hvm_tsc_scaling_supported :
               incarnation == 0) )
         {
     case TSC_MODE_NEVER_EMULATE:
@@ -1879,7 +1879,7 @@ void tsc_set_info(struct domain *d,
         d->arch.vtsc = !boot_cpu_has(X86_FEATURE_RDTSCP) ||
                        !host_tsc_is_safe();
         enable_tsc_scaling = has_hvm_container_domain(d) &&
-                             cpu_has_tsc_ratio && !d->arch.vtsc;
+                             hvm_tsc_scaling_supported && !d->arch.vtsc;
         d->arch.tsc_khz = (enable_tsc_scaling && gtsc_khz) ? gtsc_khz : cpu_khz;
         set_time_scale(&d->arch.vtsc_to_ns, d->arch.tsc_khz * 1000 );
         d->arch.ns_to_vtsc = scale_reciprocal(d->arch.vtsc_to_ns);
diff --git a/xen/include/asm-x86/hvm/hvm.h b/xen/include/asm-x86/hvm/hvm.h
index 149fe1c7a7..82d0f9d0c7 100644
--- a/xen/include/asm-x86/hvm/hvm.h
+++ b/xen/include/asm-x86/hvm/hvm.h
@@ -222,7 +222,18 @@ struct hvm_function_table {
     bool_t (*altp2m_vcpu_emulate_ve)(struct vcpu *v);
     int (*altp2m_vcpu_emulate_vmfunc)(struct cpu_user_regs *regs);
 
-    uint64_t (*scale_tsc)(const struct vcpu *v, uint64_t tsc);
+    /*
+     * Parameters and callbacks for hardware-assisted TSC scaling,
+     * which are valid only when the hardware feature is available.
+     */
+    struct {
+        /* number of bits of the fractional part of TSC scaling ratio */
+        uint8_t  ratio_frac_bits;
+        /* maximum-allowed TSC scaling ratio */
+        uint64_t max_ratio;
+
+        uint64_t (*scale_tsc)(const struct vcpu *v, uint64_t tsc);
+    } tsc_scaling;
 };
 
 extern struct hvm_function_table hvm_funcs;
@@ -258,6 +269,9 @@ void hvm_set_guest_tsc_fixed(struct vcpu *v, u64 guest_tsc, u64 at_tsc);
 u64 hvm_get_guest_tsc_fixed(struct vcpu *v, u64 at_tsc);
 #define hvm_get_guest_tsc(v) hvm_get_guest_tsc_fixed(v, 0)
 
+#define hvm_tsc_scaling_supported \
+    (!!hvm_funcs.tsc_scaling.ratio_frac_bits)
+
 int hvm_set_mode(struct vcpu *v, int mode);
 void hvm_init_guest_time(struct domain *d);
 void hvm_set_guest_time(struct vcpu *v, u64 guest_time);