diff --git a/arch/x86/vmx.c b/arch/x86/vmx.c
index db860a56a..75af69974 100644
--- a/arch/x86/vmx.c
+++ b/arch/x86/vmx.c
@@ -94,38 +94,15 @@ static inline int exec_vmxon(void *addr)
 	return status;
 }
 
-int check_vmx_support(void)
+bool get_vmx_cap(void)
 {
 	uint32_t eax, ebx, ecx, edx;
-	int ret_val = 0;
-	uint64_t tmp64;
 
 	/* Run CPUID to determine if VTX support available */
 	cpuid(CPUID_FEATURES, &eax, &ebx, &ecx, &edx);
 
 	/* See if VMX feature bit is set in ECX */
-	if (!(ecx & CPUID_ECX_VMX)) {
-		/* Log and return error */
-		pr_fatal("VMX not supported by CPU");
-		ret_val = -EINVAL;
-	} else {
-		/* Read feature control MSR */
-		tmp64 = msr_read(MSR_IA32_FEATURE_CONTROL);
-
-		/* See if feature control MSR is locked and VMX not enabled
-		 * appropriately
-		 */
-		if ((tmp64 & MSR_IA32_FEATURE_CONTROL_LOCK) &&
-		    (!(tmp64 & MSR_IA32_FEATURE_CONTROL_VMX_NO_SMX))) {
-			/* Log and return error */
-			pr_fatal("MSR_IA32_FEATURE_CONTROL: Lock bit is on and VMXON bit is off");
-			pr_fatal(" Cannot do vmxon");
-			ret_val = -EINVAL;
-		}
-	}
-
-	/* Return status to caller */
-	return ret_val;
+	return !!(ecx & CPUID_ECX_VMX);
 }
 
 int exec_vmxon_instr(void)
diff --git a/common/hv_main.c b/common/hv_main.c
index 300190e96..15e267402 100644
--- a/common/hv_main.c
+++ b/common/hv_main.c
@@ -152,8 +152,8 @@ int hv_main(int cpu_id)
 			"cpu_id/tsc_aux mismatch");
 
 	/* Check if virtualization extensions are supported */
-	ret = check_vmx_support();
-	ASSERT(ret == 0, "VMX not supported!");
+	ret = get_vmx_cap();
+	ASSERT(ret == 1, "VMX not supported!");
 
 	/* Enable virtualization extensions */
 	ret = exec_vmxon_instr();
diff --git a/include/arch/x86/vmx.h b/include/arch/x86/vmx.h
index 6d21e1be7..284f13495 100644
--- a/include/arch/x86/vmx.h
+++ b/include/arch/x86/vmx.h
@@ -413,7 +413,7 @@
 #define PAGE_PROTECTED_MODE     2
 
 /* External Interfaces */
-int check_vmx_support(void);
+bool get_vmx_cap(void);
 int exec_vmxon_instr(void);
 uint64_t exec_vmread(uint32_t field);
 uint64_t exec_vmread64(uint32_t field_full);