Index: kernel/arch/arm32/include/arch/cp15.h
===================================================================
--- kernel/arch/arm32/include/arch/cp15.h	(revision a1d636ec8b8f1091eb71c899c2f28a556977f034)
+++ kernel/arch/arm32/include/arch/cp15.h	(revision f834cc326d52cc89a38cae6dd39b7fd14a419bb3)
@@ -118,8 +118,19 @@
 };
 CONTROL_REG_GEN_READ(CTR, c0, 0, c0, 1);
+
+#if defined(PROCESSOR_ARCH_armv6) || defined(PROCESSOR_ARCH_armv7_a)
 CONTROL_REG_GEN_READ(TCMR, c0, 0, c0, 2);
+
+enum {
+	TLBTR_SEP_FLAG = 1,
+};
+
 CONTROL_REG_GEN_READ(TLBTR, c0, 0, c0, 3);
+#endif
+
+#if defined(PROCESSOR_ARCH_armv7_a)
 CONTROL_REG_GEN_READ(MPIDR, c0, 0, c0, 5);
 CONTROL_REG_GEN_READ(REVIDR, c0, 0, c0, 6);
+#endif
 
 enum {
@@ -442,7 +453,5 @@
 
 CONTROL_REG_GEN_WRITE(TLBIALL, c8, 0, c7, 0);
-#if !defined(PROCESSOR_arm920t)
 CONTROL_REG_GEN_WRITE(TLBIMVA, c8, 0, c7, 1);
-#endif
 #if defined(PROCESSOR_ARCH_armv6) || defined(PROCESSOR_ARCH_armv7_a)
 CONTROL_REG_GEN_WRITE(TLBIASID, c8, 0, c7, 2);
Index: kernel/arch/arm32/src/mm/tlb.c
===================================================================
--- kernel/arch/arm32/src/mm/tlb.c	(revision a1d636ec8b8f1091eb71c899c2f28a556977f034)
+++ kernel/arch/arm32/src/mm/tlb.c	(revision f834cc326d52cc89a38cae6dd39b7fd14a419bb3)
@@ -79,11 +79,20 @@
 static inline void invalidate_page(uintptr_t page)
 {
-#if defined(PROCESSOR_arm920t)
+#if defined(PROCESSOR_ARCH_armv6) || defined(PROCESSOR_ARCH_armv7_a)
+	if (TLBTR_read() & TLBTR_SEP_FLAG) {
+		ITLBIMVA_write(page);
+		DTLBIMVA_write(page);
+	} else {
+		TLBIMVA_write(page);
+	}
+#elif defined(PROCESSOR_arm920t)
 	ITLBIMVA_write(page);
 	DTLBIMVA_write(page);
+#elif defined(PROCESSOR_arm926ej_s)
+	TLBIMVA_write(page);
 #else
-	//TODO: What about TLBIMVAA?
-	TLBIMVA_write(page);
+#error Unknown TLB type
 #endif
+
 	/*
 	 * "A TLB maintenance operation is only guaranteed to be complete after