Index: kernel/arch/amd64/src/ddi/ddi.c
===================================================================
--- kernel/arch/amd64/src/ddi/ddi.c	(revision c09ff7bd1b88585eb4f2aaba5b1a2d603a5979c7)
+++ kernel/arch/amd64/src/ddi/ddi.c	(revision 63e27efdf2fe6d3fa02bbb5ee1da00df5cc07e9d)
@@ -35,4 +35,5 @@
 #include <ddi/ddi.h>
 #include <arch/ddi/ddi.h>
+#include <assert.h>
 #include <proc/task.h>
 #include <adt/bitmap.h>
@@ -63,5 +64,5 @@
 	
 	if (elements > 0) {
-		ASSERT(TASK->arch.iomap.bits);
+		assert(TASK->arch.iomap.bits);
 		
 		bitmap_t iomap;
Index: kernel/arch/amd64/src/interrupt.c
===================================================================
--- kernel/arch/amd64/src/interrupt.c	(revision c09ff7bd1b88585eb4f2aaba5b1a2d603a5979c7)
+++ kernel/arch/amd64/src/interrupt.c	(revision 63e27efdf2fe6d3fa02bbb5ee1da00df5cc07e9d)
@@ -34,7 +34,7 @@
 
 #include <arch/interrupt.h>
+#include <assert.h>
 #include <print.h>
 #include <log.h>
-#include <debug.h>
 #include <panic.h>
 #include <arch/drivers/i8259.h>
@@ -175,10 +175,10 @@
 static void irq_interrupt(unsigned int n, istate_t *istate)
 {
-	ASSERT(n >= IVT_IRQBASE);
+	assert(n >= IVT_IRQBASE);
 	
 	unsigned int inum = n - IVT_IRQBASE;
 	bool ack = false;
-	ASSERT(inum < IRQ_COUNT);
-	ASSERT((inum != IRQ_PIC_SPUR) && (inum != IRQ_PIC1));
+	assert(inum < IRQ_COUNT);
+	assert((inum != IRQ_PIC_SPUR) && (inum != IRQ_PIC1));
 	
 	irq_t *irq = irq_dispatch_and_lock(inum);
Index: kernel/arch/arm32/src/mach/beagleboardxm/beagleboardxm.c
===================================================================
--- kernel/arch/arm32/src/mach/beagleboardxm/beagleboardxm.c	(revision c09ff7bd1b88585eb4f2aaba5b1a2d603a5979c7)
+++ kernel/arch/arm32/src/mach/beagleboardxm/beagleboardxm.c	(revision 63e27efdf2fe6d3fa02bbb5ee1da00df5cc07e9d)
@@ -35,4 +35,5 @@
 #include <arch/exception.h>
 #include <arch/mach/beagleboardxm/beagleboardxm.h>
+#include <assert.h>
 #include <genarch/drivers/amdm37x/uart.h>
 #include <genarch/drivers/amdm37x/irc.h>
@@ -102,5 +103,5 @@
 	    (void *) km_map(AMDM37x_IRC_BASE_ADDRESS, AMDM37x_IRC_SIZE,
 	    PAGE_NOT_CACHEABLE);
-	ASSERT(beagleboard.irc_addr);
+	assert(beagleboard.irc_addr);
 	omap_irc_init(beagleboard.irc_addr);
 
Index: kernel/arch/arm32/src/mach/beaglebone/beaglebone.c
===================================================================
--- kernel/arch/arm32/src/mach/beaglebone/beaglebone.c	(revision c09ff7bd1b88585eb4f2aaba5b1a2d603a5979c7)
+++ kernel/arch/arm32/src/mach/beaglebone/beaglebone.c	(revision 63e27efdf2fe6d3fa02bbb5ee1da00df5cc07e9d)
@@ -36,4 +36,5 @@
 #include <arch/exception.h>
 #include <arch/mach/beaglebone/beaglebone.h>
+#include <assert.h>
 #include <genarch/drivers/am335x/irc.h>
 #include <genarch/drivers/am335x/uart.h>
@@ -98,8 +99,8 @@
 	    AM335x_CTRL_MODULE_SIZE, PAGE_NOT_CACHEABLE);
 
-	ASSERT(bbone.irc_addr != NULL);
-	ASSERT(bbone.cm_per_addr != NULL);
-	ASSERT(bbone.cm_dpll_addr != NULL);
-	ASSERT(bbone.ctrl_module != NULL);
+	assert(bbone.irc_addr != NULL);
+	assert(bbone.cm_per_addr != NULL);
+	assert(bbone.cm_dpll_addr != NULL);
+	assert(bbone.ctrl_module != NULL);
 
 	/* Initialize the interrupt controller */
Index: kernel/arch/arm32/src/mach/raspberrypi/raspberrypi.c
===================================================================
--- kernel/arch/arm32/src/mach/raspberrypi/raspberrypi.c	(revision c09ff7bd1b88585eb4f2aaba5b1a2d603a5979c7)
+++ kernel/arch/arm32/src/mach/raspberrypi/raspberrypi.c	(revision 63e27efdf2fe6d3fa02bbb5ee1da00df5cc07e9d)
@@ -36,4 +36,5 @@
 #include <arch/exception.h>
 #include <arch/mach/raspberrypi/raspberrypi.h>
+#include <assert.h>
 #include <genarch/drivers/pl011/pl011.h>
 #include <genarch/drivers/bcm2835/irc.h>
@@ -103,5 +104,5 @@
 	raspi.irc = (void *) km_map(BCM2835_IRC_ADDR, sizeof(bcm2835_irc_t),
 				    PAGE_NOT_CACHEABLE);
-	ASSERT(raspi.irc);
+	assert(raspi.irc);
 	bcm2835_irc_init(raspi.irc);
 
Index: kernel/arch/ia32/src/ddi/ddi.c
===================================================================
--- kernel/arch/ia32/src/ddi/ddi.c	(revision c09ff7bd1b88585eb4f2aaba5b1a2d603a5979c7)
+++ kernel/arch/ia32/src/ddi/ddi.c	(revision 63e27efdf2fe6d3fa02bbb5ee1da00df5cc07e9d)
@@ -35,4 +35,5 @@
 #include <ddi/ddi.h>
 #include <arch/ddi/ddi.h>
+#include <assert.h>
 #include <proc/task.h>
 #include <stddef.h>
@@ -63,5 +64,5 @@
 	
 	if (elements > 0) {
-		ASSERT(TASK->arch.iomap.bits);
+		assert(TASK->arch.iomap.bits);
 		
 		bitmap_t iomap;
Index: kernel/arch/ia32/src/interrupt.c
===================================================================
--- kernel/arch/ia32/src/interrupt.c	(revision c09ff7bd1b88585eb4f2aaba5b1a2d603a5979c7)
+++ kernel/arch/ia32/src/interrupt.c	(revision 63e27efdf2fe6d3fa02bbb5ee1da00df5cc07e9d)
@@ -34,4 +34,5 @@
 
 #include <arch/interrupt.h>
+#include <assert.h>
 #include <syscall/syscall.h>
 #include <print.h>
@@ -183,10 +184,10 @@
 static void irq_interrupt(unsigned int n, istate_t *istate __attribute__((unused)))
 {
-	ASSERT(n >= IVT_IRQBASE);
+	assert(n >= IVT_IRQBASE);
 	
 	unsigned int inum = n - IVT_IRQBASE;
 	bool ack = false;
-	ASSERT(inum < IRQ_COUNT);
-	ASSERT((inum != IRQ_PIC_SPUR) && (inum != IRQ_PIC1));
+	assert(inum < IRQ_COUNT);
+	assert((inum != IRQ_PIC_SPUR) && (inum != IRQ_PIC1));
 	
 	irq_t *irq = irq_dispatch_and_lock(inum);
Index: kernel/arch/ia32/src/smp/apic.c
===================================================================
--- kernel/arch/ia32/src/smp/apic.c	(revision c09ff7bd1b88585eb4f2aaba5b1a2d603a5979c7)
+++ kernel/arch/ia32/src/smp/apic.c	(revision 63e27efdf2fe6d3fa02bbb5ee1da00df5cc07e9d)
@@ -38,4 +38,5 @@
 #include <arch/smp/mps.h>
 #include <arch/boot/boot.h>
+#include <assert.h>
 #include <mm/page.h>
 #include <time/delay.h>
@@ -492,5 +493,5 @@
 	
 	/* Program Logical Destination Register. */
-	ASSERT(CPU->id < 8);
+	assert(CPU->id < 8);
 	ldr_t ldr;
 	
Index: kernel/arch/ia32/src/smp/mps.c
===================================================================
--- kernel/arch/ia32/src/smp/mps.c	(revision c09ff7bd1b88585eb4f2aaba5b1a2d603a5979c7)
+++ kernel/arch/ia32/src/smp/mps.c	(revision 63e27efdf2fe6d3fa02bbb5ee1da00df5cc07e9d)
@@ -37,8 +37,8 @@
 #include <config.h>
 #include <log.h>
-#include <debug.h>
 #include <arch/smp/mps.h>
 #include <arch/smp/apic.h>
 #include <arch/smp/smp.h>
+#include <assert.h>
 #include <func.h>
 #include <typedefs.h>
@@ -74,5 +74,5 @@
 static uint8_t mps_cpu_apic_id(size_t i)
 {
-	ASSERT(i < processor_entry_cnt);
+	assert(i < processor_entry_cnt);
 	
 	return processor_entries[i].l_apic_id;
@@ -81,5 +81,5 @@
 static bool mps_cpu_enabled(size_t i)
 {
-	ASSERT(i < processor_entry_cnt);
+	assert(i < processor_entry_cnt);
 	
 	/*
@@ -96,5 +96,5 @@
 static bool mps_cpu_bootstrap(size_t i)
 {
-	ASSERT(i < processor_entry_cnt);
+	assert(i < processor_entry_cnt);
 	
 	return (bool) ((processor_entries[i].cpu_flags & 0x02) == 0x02);
Index: kernel/arch/ia32/src/smp/smp.c
===================================================================
--- kernel/arch/ia32/src/smp/smp.c	(revision c09ff7bd1b88585eb4f2aaba5b1a2d603a5979c7)
+++ kernel/arch/ia32/src/smp/smp.c	(revision 63e27efdf2fe6d3fa02bbb5ee1da00df5cc07e9d)
@@ -38,4 +38,5 @@
 #include <arch/smp/ap.h>
 #include <arch/boot/boot.h>
+#include <assert.h>
 #include <genarch/acpi/acpi.h>
 #include <genarch/acpi/madt.h>
@@ -45,5 +46,4 @@
 #include <func.h>
 #include <panic.h>
-#include <debug.h>
 #include <arch/asm.h>
 #include <mm/page.h>
@@ -83,6 +83,6 @@
 static void cpu_arch_id_init(void)
 {
-	ASSERT(ops != NULL);
-	ASSERT(cpus != NULL);
+	assert(ops != NULL);
+	assert(cpus != NULL);
 	
 	for (unsigned int i = 0; i < config.cpu_count; ++i) {
@@ -102,5 +102,5 @@
 	unsigned int i;
 	
-	ASSERT(ops != NULL);
+	assert(ops != NULL);
 
 	/*
@@ -191,5 +191,5 @@
 int smp_irq_to_pin(unsigned int irq)
 {
-	ASSERT(ops != NULL);
+	assert(ops != NULL);
 	return ops->irq_to_pin(irq);
 }
Index: kernel/arch/ia64/include/arch/mm/page.h
===================================================================
--- kernel/arch/ia64/include/arch/mm/page.h	(revision c09ff7bd1b88585eb4f2aaba5b1a2d603a5979c7)
+++ kernel/arch/ia64/include/arch/mm/page.h	(revision 63e27efdf2fe6d3fa02bbb5ee1da00df5cc07e9d)
@@ -38,4 +38,8 @@
 
 #include <arch/mm/frame.h>
+
+#ifndef __ASM__
+#include <assert.h>
+#endif
 
 #define PAGE_SIZE   FRAME_SIZE
@@ -232,5 +236,5 @@
 	uint64_t ret;
 	
-	ASSERT(i < REGION_REGISTERS);
+	assert(i < REGION_REGISTERS);
 	
 	asm volatile (
@@ -250,5 +254,5 @@
 NO_TRACE static inline void rr_write(size_t i, uint64_t v)
 {
-	ASSERT(i < REGION_REGISTERS);
+	assert(i < REGION_REGISTERS);
 	
 	asm volatile (
Index: kernel/arch/ia64/src/drivers/ski.c
===================================================================
--- kernel/arch/ia64/src/drivers/ski.c	(revision c09ff7bd1b88585eb4f2aaba5b1a2d603a5979c7)
+++ kernel/arch/ia64/src/drivers/ski.c	(revision 63e27efdf2fe6d3fa02bbb5ee1da00df5cc07e9d)
@@ -34,4 +34,5 @@
 
 #include <arch/drivers/ski.h>
+#include <assert.h>
 #include <console/console.h>
 #include <console/chardev.h>
@@ -238,6 +239,6 @@
 void skiin_wire(ski_instance_t *instance, indev_t *srlnin)
 {
-	ASSERT(instance);
-	ASSERT(srlnin);
+	assert(instance);
+	assert(srlnin);
 	
 	instance->srlnin = srlnin;
Index: kernel/arch/ia64/src/interrupt.c
===================================================================
--- kernel/arch/ia64/src/interrupt.c	(revision c09ff7bd1b88585eb4f2aaba5b1a2d603a5979c7)
+++ kernel/arch/ia64/src/interrupt.c	(revision 63e27efdf2fe6d3fa02bbb5ee1da00df5cc07e9d)
@@ -35,9 +35,9 @@
 
 #include <arch/interrupt.h>
+#include <assert.h>
 #include <interrupt.h>
 #include <ddi/irq.h>
 #include <panic.h>
 #include <print.h>
-#include <debug.h>
 #include <console/console.h>
 #include <typedefs.h>
@@ -123,5 +123,5 @@
 static const char *vector_to_string(unsigned int n)
 {
-	ASSERT(n <= VECTOR_MAX);
+	assert(n <= VECTOR_MAX);
 	
 	if (n >= VECTORS_16_BUNDLE_START)
Index: kernel/arch/ia64/src/mm/as.c
===================================================================
--- kernel/arch/ia64/src/mm/as.c	(revision c09ff7bd1b88585eb4f2aaba5b1a2d603a5979c7)
+++ kernel/arch/ia64/src/mm/as.c	(revision 63e27efdf2fe6d3fa02bbb5ee1da00df5cc07e9d)
@@ -36,4 +36,5 @@
 #include <arch/mm/asid.h>
 #include <arch/mm/page.h>
+#include <assert.h>
 #include <genarch/mm/as_ht.h>
 #include <genarch/mm/page_ht.h>
@@ -58,5 +59,5 @@
 	int i;
 	
-	ASSERT(as->asid != ASID_INVALID);
+	assert(as->asid != ASID_INVALID);
 	
 	/*
Index: kernel/arch/ia64/src/mm/page.c
===================================================================
--- kernel/arch/ia64/src/mm/page.c	(revision c09ff7bd1b88585eb4f2aaba5b1a2d603a5979c7)
+++ kernel/arch/ia64/src/mm/page.c	(revision 63e27efdf2fe6d3fa02bbb5ee1da00df5cc07e9d)
@@ -35,4 +35,5 @@
 
 #include <arch/mm/page.h>
+#include <assert.h>
 #include <genarch/mm/page_ht.h>
 #include <mm/asid.h>
@@ -166,5 +167,5 @@
 	bool match;
 
-	ASSERT(v);
+	assert(v);
 
 	vrn = page >> VRN_SHIFT;
@@ -213,5 +214,5 @@
 	uint64_t tag;
 
-	ASSERT(v);
+	assert(v);
 
 	vrn = page >> VRN_SHIFT;
Index: kernel/arch/ia64/src/mm/tlb.c
===================================================================
--- kernel/arch/ia64/src/mm/tlb.c	(revision c09ff7bd1b88585eb4f2aaba5b1a2d603a5979c7)
+++ kernel/arch/ia64/src/mm/tlb.c	(revision 63e27efdf2fe6d3fa02bbb5ee1da00df5cc07e9d)
@@ -48,4 +48,5 @@
 #include <arch/pal/pal.h>
 #include <arch/asm.h>
+#include <assert.h>
 #include <panic.h>
 #include <print.h>
@@ -449,5 +450,5 @@
 	entry.word[1] = 0;
 	
-	ASSERT(t->x);
+	assert(t->x);
 	
 	entry.p = t->p;
@@ -488,9 +489,9 @@
 	va = istate->cr_ifa; /* faulting address */
 	
-	ASSERT(!is_kernel_fault(va));
+	assert(!is_kernel_fault(va));
 
 	bool found = page_mapping_find(AS, va, true, &t);
 	if (found) {
-		ASSERT(t.p);
+		assert(t.p);
 
 		/*
@@ -605,5 +606,5 @@
 	bool found = page_mapping_find(as, va, true, &t);
 	if (found) {
-		ASSERT(t.p);
+		assert(t.p);
 
 		/*
@@ -634,5 +635,5 @@
 void data_nested_tlb_fault(unsigned int n, istate_t *istate)
 {
-	ASSERT(false);
+	assert(false);
 }
 
@@ -656,6 +657,6 @@
 	bool found = page_mapping_find(as, va, true, &t);
 
-	ASSERT(found);
-	ASSERT(t.p);
+	assert(found);
+	assert(t.p);
 
 	if (found && t.p && t.w) {
@@ -685,10 +686,10 @@
 	va = istate->cr_ifa;  /* faulting address */
 
-	ASSERT(!is_kernel_fault(va));
+	assert(!is_kernel_fault(va));
 	
 	bool found = page_mapping_find(AS, va, true, &t);
 
-	ASSERT(found);
-	ASSERT(t.p);
+	assert(found);
+	assert(t.p);
 
 	if (found && t.p && t.x) {
@@ -724,6 +725,6 @@
 	bool found = page_mapping_find(as, va, true, &t);
 
-	ASSERT(found);
-	ASSERT(t.p);
+	assert(found);
+	assert(t.p);
 
 	if (found && t.p) {
@@ -757,5 +758,5 @@
 	va = istate->cr_ifa;  /* faulting address */
 
-	ASSERT(!is_kernel_fault(va));
+	assert(!is_kernel_fault(va));
 	
 	/*
@@ -764,7 +765,7 @@
 	bool found = page_mapping_find(AS, va, true, &t);
 
-	ASSERT(found);
-	ASSERT(t.p);
-	ASSERT(!t.w);
+	assert(found);
+	assert(t.p);
+	assert(!t.w);
 
 	as_page_fault(va, PF_ACCESS_WRITE, istate);
@@ -784,9 +785,9 @@
 	va = istate->cr_ifa;  /* faulting address */
 	
-	ASSERT(!is_kernel_fault(va));
+	assert(!is_kernel_fault(va));
 
 	bool found = page_mapping_find(AS, va, true, &t);
 
-	ASSERT(found);
+	assert(found);
 	
 	if (t.p) {
Index: kernel/arch/mips32/src/exception.c
===================================================================
--- kernel/arch/mips32/src/exception.c	(revision c09ff7bd1b88585eb4f2aaba5b1a2d603a5979c7)
+++ kernel/arch/mips32/src/exception.c	(revision 63e27efdf2fe6d3fa02bbb5ee1da00df5cc07e9d)
@@ -39,5 +39,5 @@
 #include <arch/cp0.h>
 #include <arch.h>
-#include <debug.h>
+#include <assert.h>
 #include <proc/thread.h>
 #include <print.h>
@@ -120,5 +120,5 @@
 {
 	if (*((uint32_t *) istate->epc) == 0x7c03e83b) {
-		ASSERT(THREAD);
+		assert(THREAD);
 		istate->epc += 4;
 		istate->v1 = istate->kt1;
Index: kernel/arch/mips32/src/mm/tlb.c
===================================================================
--- kernel/arch/mips32/src/mm/tlb.c	(revision c09ff7bd1b88585eb4f2aaba5b1a2d603a5979c7)
+++ 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)
Index: kernel/arch/ppc32/src/mm/pht.c
===================================================================
--- kernel/arch/ppc32/src/mm/pht.c	(revision c09ff7bd1b88585eb4f2aaba5b1a2d603a5979c7)
+++ kernel/arch/ppc32/src/mm/pht.c	(revision 63e27efdf2fe6d3fa02bbb5ee1da00df5cc07e9d)
@@ -35,4 +35,5 @@
 #include <arch/mm/pht.h>
 #include <arch/mm/tlb.h>
+#include <assert.h>
 #include <interrupt.h>
 #include <mm/as.h>
@@ -79,6 +80,6 @@
 		found = page_mapping_find(as, badvaddr, true, pte);
 
-		ASSERT(found);
-		ASSERT(pte->present);
+		assert(found);
+		assert(pte->present);
 
 		return found;
Index: kernel/arch/sparc64/src/drivers/pci.c
===================================================================
--- kernel/arch/sparc64/src/drivers/pci.c	(revision c09ff7bd1b88585eb4f2aaba5b1a2d603a5979c7)
+++ kernel/arch/sparc64/src/drivers/pci.c	(revision 63e27efdf2fe6d3fa02bbb5ee1da00df5cc07e9d)
@@ -42,5 +42,5 @@
 #include <mm/slab.h>
 #include <typedefs.h>
-#include <debug.h>
+#include <assert.h>
 #include <log.h>
 #include <str.h>
@@ -175,5 +175,5 @@
 	 * First, verify this is a PCI node.
 	 */
-	ASSERT(str_cmp(ofw_tree_node_name(node), "pci") == 0);
+	assert(str_cmp(ofw_tree_node_name(node), "pci") == 0);
 
 	/*
@@ -210,5 +210,5 @@
 void pci_enable_interrupt(pci_t *pci, int inr)
 {
-	ASSERT(pci->op && pci->op->enable_interrupt);
+	assert(pci->op && pci->op->enable_interrupt);
 	pci->op->enable_interrupt(pci, inr);
 }
@@ -218,5 +218,5 @@
 	pci_t *pci = (pci_t *)pcip;
 
-	ASSERT(pci->op && pci->op->clear_interrupt);
+	assert(pci->op && pci->op->clear_interrupt);
 	pci->op->clear_interrupt(pci, inr);
 }
Index: kernel/arch/sparc64/src/drivers/tick.c
===================================================================
--- kernel/arch/sparc64/src/drivers/tick.c	(revision c09ff7bd1b88585eb4f2aaba5b1a2d603a5979c7)
+++ kernel/arch/sparc64/src/drivers/tick.c	(revision 63e27efdf2fe6d3fa02bbb5ee1da00df5cc07e9d)
@@ -43,5 +43,5 @@
 #include <time/clock.h>
 #include <arch.h>
-#include <debug.h>
+#include <assert.h>
 
 /** Initialize tick and stick interrupt. */
@@ -93,10 +93,10 @@
 	 * Make sure we are servicing interrupt_level_14
 	 */
-	ASSERT(n == TT_INTERRUPT_LEVEL_14);
+	assert(n == TT_INTERRUPT_LEVEL_14);
 	
 	/*
 	 * Make sure we are servicing TICK_INT.
 	 */
-	ASSERT(softint.tick_int);
+	assert(softint.tick_int);
 
 	/*
Index: kernel/arch/sparc64/src/mm/sun4u/as.c
===================================================================
--- kernel/arch/sparc64/src/mm/sun4u/as.c	(revision c09ff7bd1b88585eb4f2aaba5b1a2d603a5979c7)
+++ kernel/arch/sparc64/src/mm/sun4u/as.c	(revision 63e27efdf2fe6d3fa02bbb5ee1da00df5cc07e9d)
@@ -35,8 +35,8 @@
 #include <arch/mm/as.h>
 #include <arch/mm/tlb.h>
+#include <assert.h>
+#include <config.h>
 #include <genarch/mm/page_ht.h>
 #include <genarch/mm/asid_fifo.h>
-#include <debug.h>
-#include <config.h>
 
 #ifdef CONFIG_TSB
@@ -130,6 +130,6 @@
 	uintptr_t base = ALIGN_DOWN(config.base, 1 << KERNEL_PAGE_WIDTH);
 	
-	ASSERT(as->arch.itsb);
-	ASSERT(as->arch.dtsb);
+	assert(as->arch.itsb);
+	assert(as->arch.dtsb);
 	
 	uintptr_t tsb = (uintptr_t) as->arch.itsb;
@@ -202,6 +202,6 @@
 	uintptr_t base = ALIGN_DOWN(config.base, 1 << KERNEL_PAGE_WIDTH);
 	
-	ASSERT(as->arch.itsb);
-	ASSERT(as->arch.dtsb);
+	assert(as->arch.itsb);
+	assert(as->arch.dtsb);
 	
 	uintptr_t tsb = (uintptr_t) as->arch.itsb;
Index: kernel/arch/sparc64/src/mm/sun4u/tlb.c
===================================================================
--- kernel/arch/sparc64/src/mm/sun4u/tlb.c	(revision c09ff7bd1b88585eb4f2aaba5b1a2d603a5979c7)
+++ kernel/arch/sparc64/src/mm/sun4u/tlb.c	(revision 63e27efdf2fe6d3fa02bbb5ee1da00df5cc07e9d)
@@ -41,4 +41,5 @@
 #include <arch/mm/mmu.h>
 #include <arch/interrupt.h>
+#include <assert.h>
 #include <interrupt.h>
 #include <arch.h>
@@ -201,5 +202,5 @@
 	bool found = page_mapping_find(AS, istate->tpc, true, &t);
 	if (found && PTE_EXECUTABLE(&t)) {
-		ASSERT(t.p);
+		assert(t.p);
 
 		/*
@@ -258,5 +259,5 @@
 	bool found = page_mapping_find(as, page_16k, true, &t);
 	if (found) {
-		ASSERT(t.p);
+		assert(t.p);
 
 		/*
@@ -301,5 +302,5 @@
 	bool found = page_mapping_find(as, page_16k, true, &t);
 	if (found && PTE_WRITABLE(&t)) {
-		ASSERT(t.p);
+		assert(t.p);
 
 		/*
Index: kernel/arch/sparc64/src/mm/sun4u/tsb.c
===================================================================
--- kernel/arch/sparc64/src/mm/sun4u/tsb.c	(revision c09ff7bd1b88585eb4f2aaba5b1a2d603a5979c7)
+++ kernel/arch/sparc64/src/mm/sun4u/tsb.c	(revision 63e27efdf2fe6d3fa02bbb5ee1da00df5cc07e9d)
@@ -27,5 +27,5 @@
  */
 
-/** @addtogroup sparc64mm	
+/** @addtogroup sparc64mm
  * @{
  */
@@ -37,8 +37,8 @@
 #include <arch/mm/page.h>
 #include <arch/barrier.h>
+#include <assert.h>
 #include <mm/as.h>
 #include <typedefs.h>
 #include <macros.h>
-#include <debug.h>
 
 /** Invalidate portion of TSB.
@@ -58,6 +58,6 @@
 	size_t cnt;
 	
-	ASSERT(as->arch.itsb);
-	ASSERT(as->arch.dtsb);
+	assert(as->arch.itsb);
+	assert(as->arch.dtsb);
 	
 	i0 = (page >> MMU_PAGE_WIDTH) & ITSB_ENTRY_MASK;
@@ -85,5 +85,5 @@
 	size_t entry;
 
-	ASSERT(index <= 1);
+	assert(index <= 1);
 	
 	as = t->as;
@@ -130,5 +130,5 @@
 	size_t entry;
 	
-	ASSERT(index <= 1);
+	assert(index <= 1);
 
 	as = t->as;
Index: kernel/arch/sparc64/src/mm/sun4v/as.c
===================================================================
--- kernel/arch/sparc64/src/mm/sun4v/as.c	(revision c09ff7bd1b88585eb4f2aaba5b1a2d603a5979c7)
+++ kernel/arch/sparc64/src/mm/sun4v/as.c	(revision 63e27efdf2fe6d3fa02bbb5ee1da00df5cc07e9d)
@@ -37,7 +37,7 @@
 #include <arch/mm/pagesize.h>
 #include <arch/mm/tlb.h>
+#include <assert.h>
 #include <genarch/mm/page_ht.h>
 #include <genarch/mm/asid_fifo.h>
-#include <debug.h>
 #include <config.h>
 #include <arch/sun4v/hypercall.h>
@@ -121,5 +121,5 @@
 	uintptr_t base = ALIGN_DOWN(config.base, 1 << KERNEL_PAGE_WIDTH);
 	
-	ASSERT(as->arch.tsb_description.tsb_base);
+	assert(as->arch.tsb_description.tsb_base);
 	uintptr_t tsb = PA2KA(as->arch.tsb_description.tsb_base);
 	
@@ -160,5 +160,5 @@
 	uintptr_t base = ALIGN_DOWN(config.base, 1 << KERNEL_PAGE_WIDTH);
 	
-	ASSERT(as->arch.tsb_description.tsb_base);
+	assert(as->arch.tsb_description.tsb_base);
 	
 	uintptr_t tsb = PA2KA(as->arch.tsb_description.tsb_base);
Index: kernel/arch/sparc64/src/mm/sun4v/tlb.c
===================================================================
--- kernel/arch/sparc64/src/mm/sun4v/tlb.c	(revision c09ff7bd1b88585eb4f2aaba5b1a2d603a5979c7)
+++ kernel/arch/sparc64/src/mm/sun4v/tlb.c	(revision 63e27efdf2fe6d3fa02bbb5ee1da00df5cc07e9d)
@@ -43,4 +43,5 @@
 #include <arch/mm/tlb.h>
 #include <arch/interrupt.h>
+#include <assert.h>
 #include <interrupt.h>
 #include <arch.h>
@@ -215,5 +216,5 @@
 	bool found = page_mapping_find(AS, va, true, &t);
 	if (found && PTE_EXECUTABLE(&t)) {
-		ASSERT(t.p);
+		assert(t.p);
 
 		/*
@@ -265,5 +266,5 @@
 	bool found = page_mapping_find(as, va, true, &t);
 	if (found) {
-		ASSERT(t.p);
+		assert(t.p);
 
 		/*
@@ -303,5 +304,5 @@
 	bool found = page_mapping_find(as, va, true, &t);
 	if (found && PTE_WRITABLE(&t)) {
-		ASSERT(t.p);
+		assert(t.p);
 
 		/*
@@ -345,5 +346,5 @@
 	__hypercall_fast_ret1(0, 0, 0, 0, 0, CPU_MYID, &myid);
 
-	ASSERT(mmu_fsas[myid].dft < 16);
+	assert(mmu_fsas[myid].dft < 16);
 
 	printf("condition which caused the fault: %s\n",
Index: kernel/arch/sparc64/src/mm/sun4v/tsb.c
===================================================================
--- kernel/arch/sparc64/src/mm/sun4v/tsb.c	(revision c09ff7bd1b88585eb4f2aaba5b1a2d603a5979c7)
+++ kernel/arch/sparc64/src/mm/sun4v/tsb.c	(revision 63e27efdf2fe6d3fa02bbb5ee1da00df5cc07e9d)
@@ -39,8 +39,8 @@
 #include <arch/mm/page.h>
 #include <arch/barrier.h>
+#include <assert.h>
 #include <mm/as.h>
 #include <typedefs.h>
 #include <macros.h>
-#include <debug.h>
 
 /** Invalidate portion of TSB.
@@ -60,5 +60,5 @@
 	size_t cnt;
 	
-	ASSERT(as->arch.tsb_description.tsb_base);
+	assert(as->arch.tsb_description.tsb_base);
 	
 	i0 = (page >> MMU_PAGE_WIDTH) & TSB_ENTRY_MASK;
Index: kernel/arch/sparc64/src/smp/sun4u/ipi.c
===================================================================
--- kernel/arch/sparc64/src/smp/sun4u/ipi.c	(revision c09ff7bd1b88585eb4f2aaba5b1a2d603a5979c7)
+++ kernel/arch/sparc64/src/smp/sun4u/ipi.c	(revision 63e27efdf2fe6d3fa02bbb5ee1da00df5cc07e9d)
@@ -35,4 +35,5 @@
 #include <smp/ipi.h>
 #include <arch/smp/sun4u/ipi.h>
+#include <assert.h>
 #include <cpu.h>
 #include <arch.h>
@@ -103,5 +104,5 @@
 		panic("Interrupt Dispatch Status busy bit set\n");
 	
-	ASSERT(!(pstate_read() & PSTATE_IE_BIT));
+	assert(!(pstate_read() & PSTATE_IE_BIT));
 	
 	do {
@@ -185,5 +186,5 @@
 void ipi_unicast_arch(unsigned int cpu_id, int ipi)
 {
-	ASSERT(&cpus[cpu_id] != CPU);
+	assert(&cpus[cpu_id] != CPU);
 	
 	if (ipi == IPI_SMP_CALL) {
Index: kernel/arch/sparc64/src/sparc64.c
===================================================================
--- kernel/arch/sparc64/src/sparc64.c	(revision c09ff7bd1b88585eb4f2aaba5b1a2d603a5979c7)
+++ kernel/arch/sparc64/src/sparc64.c	(revision 63e27efdf2fe6d3fa02bbb5ee1da00df5cc07e9d)
@@ -70,5 +70,5 @@
 
 	if (config.cpu_active == 1) {
-		STATIC_ASSERT(UWB_SIZE <= UWB_ALIGNMENT);
+		static_assert(UWB_SIZE <= UWB_ALIGNMENT, "");
 		/* Create slab cache for the userspace window buffers */
 		uwb_cache = slab_cache_create("uwb_cache", UWB_SIZE,