diff --git a/include/arch/arm/arch/32/mode/hardware.h b/include/arch/arm/arch/32/mode/hardware.h
index b7fb4183eb853c7a4f4fa41d30cdb356f5d2a945..70bee6a49c5823e013384220659660d170104c7f 100644
--- a/include/arch/arm/arch/32/mode/hardware.h
+++ b/include/arch/arm/arch/32/mode/hardware.h
@@ -14,8 +14,10 @@
 #define __ARCH_HARDWARE_32_H
 
 #include <config.h>
+#ifndef __ASSEMBLER__
 #include <arch/machine/hardware.h>
 #include <plat/api/constants.h>
+#endif
 
 /*
  * 0xffe00000 asid id slot (arm/arch/kernel/vspace.h)
@@ -34,6 +36,8 @@
 #define KDEV_PPTR 0xfff00000
 #define PADDR_TOP (PPTR_TOP - BASE_OFFSET)
 
+#ifndef __ASSEMBLER__
 #include <plat/machine/hardware.h>
+#endif
 
 #endif /* __ARCH_HARDWARE_32_H */