Index: head/sys/x86/x86/tsc.c
===================================================================
--- head/sys/x86/x86/tsc.c
+++ head/sys/x86/x86/tsc.c
@@ -143,7 +143,7 @@
  * tsc_freq_intel(), when available.
  */
 static bool
-tsc_freq_cpuid(void)
+tsc_freq_cpuid(uint64_t *res)
 {
 	u_int regs[4];
 
@@ -151,7 +151,7 @@
 		return (false);
 	do_cpuid(0x15, regs);
 	if (regs[0] != 0 && regs[1] != 0 && regs[2] != 0) {
-		tsc_freq = (uint64_t)regs[2] * regs[1] / regs[0];
+		*res = (uint64_t)regs[2] * regs[1] / regs[0];
 		return (true);
 	}
 
@@ -159,7 +159,7 @@
 		return (false);
 	do_cpuid(0x16, regs);
 	if (regs[0] != 0) {
-		tsc_freq = (uint64_t)regs[0] * 1000000;
+		*res = (uint64_t)regs[0] * 1000000;
 		return (true);
 	}
 
@@ -228,7 +228,8 @@
 static void
 probe_tsc_freq(void)
 {
-	uint64_t tsc1, tsc2;
+	uint64_t tmp_freq, tsc1, tsc2;
+	int no_cpuid_override;
 	uint16_t bootflags;
 
 	if (cpu_power_ecx & CPUID_PERF_STAT) {
@@ -299,15 +300,15 @@
 		 */
 		if (acpi_get_fadt_bootflags(&bootflags) &&
 		    (bootflags & ACPI_FADT_LEGACY_DEVICES) == 0 &&
-		    tsc_freq_cpuid()) {
+		    tsc_freq_cpuid(&tmp_freq)) {
 			printf("Skipping TSC calibration since no legacy "
 			    "devices reported by FADT and CPUID works\n");
 			tsc_skip_calibration = 1;
 		}
 	}
 	if (tsc_skip_calibration) {
-		if (tsc_freq_cpuid())
-			;
+		if (tsc_freq_cpuid(&tmp_freq))
+			tsc_freq = tmp_freq;
 		else if (cpu_vendor_id == CPU_VENDOR_INTEL)
 			tsc_freq_intel();
 	} else {
@@ -317,6 +318,32 @@
 		DELAY(1000000);
 		tsc2 = rdtsc();
 		tsc_freq = tsc2 - tsc1;
+
+		/*
+		 * If the difference between calibrated frequency and
+		 * the frequency reported by CPUID 0x15/0x16 leafs
+		 * differ significantly, this probably means that
+		 * calibration is bogus.  It happens on machines
+		 * without 8254 timer and with BIOS not properly
+		 * reporting it in FADT boot flags.
+		 */
+		if (tsc_freq_cpuid(&tmp_freq) && qabs(tsc_freq - tmp_freq) >
+		    uqmin(tsc_freq, tmp_freq)) {
+			no_cpuid_override = 0;
+			TUNABLE_INT_FETCH("machdep.disable_tsc_cpuid_override",
+			    &no_cpuid_override);
+			if (!no_cpuid_override) {
+				if (bootverbose) {
+					printf(
+	"TSC clock: calibration freq %ju Hz, CPUID freq %ju Hz%s\n",
+					    (uintmax_t)tsc_freq,
+					    (uintmax_t)tmp_freq,
+					    no_cpuid_override ? "" :
+					    ", doing CPUID override");
+				}
+				tsc_freq = tmp_freq;
+			}
+		}
 	}
 	if (bootverbose)
 		printf("TSC clock: %ju Hz\n", (intmax_t)tsc_freq);