diff --git a/src/include/pc80/i8254.h b/src/include/pc80/i8254.h
index f4f0dcaab0..964cc974d9 100644
--- a/src/include/pc80/i8254.h
+++ b/src/include/pc80/i8254.h
@@ -59,4 +59,5 @@
 #define PPCB_T2GATE     0x01    /* Bit 0 */
 
 void setup_i8254(void);
-#endif
+
+#endif /* PC80_I8254_H */
diff --git a/src/include/pc80/mc146818rtc.h b/src/include/pc80/mc146818rtc.h
index 46dbd736db..56f8cafe90 100644
--- a/src/include/pc80/mc146818rtc.h
+++ b/src/include/pc80/mc146818rtc.h
@@ -1,6 +1,8 @@
 #ifndef PC80_MC146818RTC_H
 #define PC80_MC146818RTC_H
 
+#if CONFIG_ARCH_X86
+
 #include <arch/io.h>
 #include <types.h>
 
@@ -224,4 +226,6 @@ void cmos_post_log(void);
 static inline void cmos_post_log(void) {}
 #endif /* CONFIG_CMOS_POST */
 
+#endif /* CONFIG_ARCH_X86 */
+
 #endif /*  PC80_MC146818RTC_H */