diff --git a/sys/dev/psci/psci_arm.S b/sys/dev/psci/psci_arm.S
index 987e3d154e1b..f756aa951844 100644
--- a/sys/dev/psci/psci_arm.S
+++ b/sys/dev/psci/psci_arm.S
@@ -28,7 +28,8 @@
 #include <machine/asm.h>
 __FBSDID("$FreeBSD$");
 
-.arch_extension virt /* For hvc */
+.arch_extension sec	/* For smc */
+.arch_extension virt	/* For hvc */
 
 /*
  * int psci_hvc_despatch(register_t psci_fnid, register_t...)