diff --git a/libsel4simple/include/simple/simple.h b/libsel4simple/include/simple/simple.h
index ac8fb0b..9305926 100644
--- a/libsel4simple/include/simple/simple.h
+++ b/libsel4simple/include/simple/simple.h
@@ -560,6 +560,7 @@
 }
 #endif
 
+#ifdef CONFIG_ARM_SMMU
 static inline seL4_CPtr simple_get_sid_ctrl(simple_t *simple)
 {
     return simple_init_cap(simple, seL4_CapSMMUSIDControl);
@@ -569,6 +570,7 @@
 {
     return simple_init_cap(simple, seL4_CapSMMUCBControl);
 }
+#endif
 
 static inline void simple_print(simple_t *simple)
 {