diff --git a/src/arch/x86/smbios.c b/src/arch/x86/smbios.c
index 725d808d56..7deac63dd6 100644
--- a/src/arch/x86/smbios.c
+++ b/src/arch/x86/smbios.c
@@ -657,7 +657,26 @@ static int smbios_write_type4(unsigned long *current, int handle)
 	t->processor_version = smbios_processor_name(t->eos);
 	t->processor_family = (res.eax > 0) ? 0x0c : 0x6;
 	t->processor_type = 3; /* System Processor */
-	t->core_count = (res.ebx >> 16) & 0xff;
+	/*
+	 * If CPUID leaf 11 is available, calculate "core count" by dividing
+	 * SMT_ID (logical processors in a core) by Core_ID (number of cores).
+	 * This seems to be the way to arrive to a number of cores mentioned on
+	 * ark.intel.com.
+	 */
+	if (cpu_have_cpuid() && cpuid_get_max_func() >= 0xb) {
+		uint32_t leaf_b_cores = 0, leaf_b_threads = 0;
+		res = cpuid_ext(0xb, 1);
+		leaf_b_cores = res.ebx;
+		res = cpuid_ext(0xb, 0);
+		leaf_b_threads = res.ebx;
+		/* if hyperthreading is not available, pretend this is 1 */
+		if (leaf_b_threads == 0) {
+			leaf_b_threads = 1;
+		}
+		t->core_count = leaf_b_cores / leaf_b_threads;
+	} else {
+		t->core_count = (res.ebx >> 16) & 0xff;
+	}
 	/* Assume we enable all the cores always, capped only by MAX_CPUS */
 	t->core_enabled = MIN(t->core_count, CONFIG_MAX_CPUS);
 	t->l1_cache_handle = 0xffff;