Index: kernel/arch/arm32/include/arch/cp15.h
===================================================================
--- kernel/arch/arm32/include/arch/cp15.h	(revision 5f310ec89435b0cb60122b06655c02413f3977a6)
+++ kernel/arch/arm32/include/arch/cp15.h	(revision a1d636ec8b8f1091eb71c899c2f28a556977f034)
@@ -309,4 +309,5 @@
 enum {
 	TTBR_ADDR_MASK = 0xffffff80,
+#if defined(PROCESSOR_ARCH_armv6) || defined(PROCESSOR_ARCH_armv7_a)
 	TTBR_NOS_FLAG = 1 << 5,
 	TTBR_RGN_MASK = 0x3 << 3,
@@ -317,12 +318,17 @@
 	TTBR_S_FLAG = 1 << 1,
 	TTBR_C_FLAG = 1 << 0,
+#endif
 };
 CONTROL_REG_GEN_READ(TTBR0, c2, 0, c0, 0);
 CONTROL_REG_GEN_WRITE(TTBR0, c2, 0, c0, 0);
+
+#if defined(PROCESSOR_ARCH_armv6) || defined(PROCESSOR_ARCH_armv7_a)
 CONTROL_REG_GEN_READ(TTBR1, c2, 0, c0, 1);
 CONTROL_REG_GEN_WRITE(TTBR1, c2, 0, c0, 1);
 CONTROL_REG_GEN_READ(TTBCR, c2, 0, c0, 2);
 CONTROL_REG_GEN_WRITE(TTBCR, c2, 0, c0, 2);
-
+#endif
+
+#if defined(PROCESSOR_ARCH_armv7)
 CONTROL_REG_GEN_READ(HTCR, c2, 4, c0, 2);
 CONTROL_REG_GEN_WRITE(HTCR, c2, 4, c0, 2);
@@ -339,4 +345,5 @@
 CONTROL_REG_GEN_READ(VTTBRH, c2, 0, c2, 6);
 CONTROL_REG_GEN_WRITE(VTTBRH, c2, 0, c2, 6);
+#endif
 
 CONTROL_REG_GEN_READ(DACR, c3, 0, c0, 0);
Index: kernel/arch/arm32/include/arch/mm/page.h
===================================================================
--- kernel/arch/arm32/include/arch/mm/page.h	(revision 5f310ec89435b0cb60122b06655c02413f3977a6)
+++ kernel/arch/arm32/include/arch/mm/page.h	(revision a1d636ec8b8f1091eb71c899c2f28a556977f034)
@@ -154,5 +154,8 @@
 {
 	uint32_t val = (uint32_t)pt & TTBR_ADDR_MASK;
+#if defined(PROCESSOR_ARCH_armv6) || defined(PROCESSOR_ARCH_armv7_a)
+	// FIXME: TTBR_RGN_WBWA_CACHE is unpredictable on ARMv6
 	val |= TTBR_RGN_WBWA_CACHE | TTBR_C_FLAG;
+#endif
 	TTBR0_write(val);
 }