Index: kernel/arch/mips32/src/mm/tlb.c
===================================================================
--- kernel/arch/mips32/src/mm/tlb.c	(revision 346b12a2767bb66df8633e469fd871fea8c43b5c)
+++ kernel/arch/mips32/src/mm/tlb.c	(revision 63e27efdf2fe6d3fa02bbb5ee1da00df5cc07e9d)
@@ -44,5 +44,5 @@
 #include <print.h>
 #include <log.h>
-#include <debug.h>
+#include <assert.h>
 #include <align.h>
 #include <interrupt.h>
@@ -160,5 +160,5 @@
 #endif
 
-	ASSERT(!index.p);
+	assert(!index.p);
 
 	badvaddr = cp0_badvaddr_read();
@@ -323,5 +323,5 @@
 	int i;
 
-	ASSERT(interrupts_disabled());
+	assert(interrupts_disabled());
 
 	hi_save.value = cp0_entry_hi_read();
@@ -356,6 +356,6 @@
 	int i;
 
-	ASSERT(interrupts_disabled());
-	ASSERT(asid != ASID_INVALID);
+	assert(interrupts_disabled());
+	assert(asid != ASID_INVALID);
 
 	hi_save.value = cp0_entry_hi_read();
@@ -398,5 +398,5 @@
 	tlb_index_t index;
 
-	ASSERT(interrupts_disabled());
+	assert(interrupts_disabled());
 	
 	if (asid == ASID_INVALID)