diff --git a/sys/arm/arm/devmap.c b/sys/arm/arm/devmap.c
index d9bdd9cac200..1c60a15f6e27 100644
--- a/sys/arm/arm/devmap.c
+++ b/sys/arm/arm/devmap.c
@@ -31,6 +31,8 @@ __FBSDID("$FreeBSD$");
  * Routines for mapping device memory.
  */
 
+#include "opt_ddb.h"
+
 #include <sys/param.h>
 #include <sys/systm.h>
 #include <vm/vm.h>
@@ -53,6 +55,36 @@ static struct arm_devmap_entry	akva_devmap_entries[AKVA_DEVMAP_MAX_ENTRIES];
 static u_int			akva_devmap_idx;
 static vm_offset_t		akva_devmap_vaddr = ARM_VECTORS_HIGH;
 
+/*
+ * Print the contents of the static mapping table using the provided printf-like
+ * output function (which will be either printf or db_printf).
+ */
+static void
+devmap_dump_table(int (*prfunc)(const char *, ...))
+{
+	const struct arm_devmap_entry *pd;
+
+	if (devmap_table == NULL || devmap_table[0].pd_size == 0) {
+		prfunc("No static device mappings.\n");
+		return;
+	}
+
+	prfunc("Static device mappings:\n");
+	for (pd = devmap_table; pd->pd_size != 0; ++pd) {
+		prfunc("  0x%08x - 0x%08x mapped at VA 0x%08x\n",
+		    pd->pd_pa, pd->pd_pa + pd->pd_size - 1, pd->pd_va);
+	}
+}
+
+/*
+ * Print the contents of the static mapping table.  Used for bootverbose.
+ */
+void
+arm_devmap_print_table()
+{
+	devmap_dump_table(printf);
+}
+
 /*
  * Return the "last" kva address used by the registered devmap table.  It's
  * actually the lowest address used by the static mappings, i.e., the address of
@@ -266,3 +298,13 @@ pmap_unmapdev(vm_offset_t va, vm_size_t size)
 	kva_free(va, origsize);
 }
 
+#ifdef DDB
+#include <ddb/ddb.h>
+
+DB_SHOW_COMMAND(devmap, db_show_devmap)
+{
+	devmap_dump_table(db_printf);
+}
+
+#endif /* DDB */
+
diff --git a/sys/arm/arm/machdep.c b/sys/arm/arm/machdep.c
index c48933d2c68c..1a85d60d1378 100644
--- a/sys/arm/arm/machdep.c
+++ b/sys/arm/arm/machdep.c
@@ -379,10 +379,10 @@ cpu_startup(void *dummy)
 			vm_paddr_t size;
 
 			size = phys_avail[indx + 1] - phys_avail[indx];
-			printf("%#08jx - %#08jx, %ju bytes (%ju pages)\n",
+			printf("  0x%08jx - 0x%08jx, %ju KBytes (%ju pages)\n",
 			    (uintmax_t)phys_avail[indx],
 			    (uintmax_t)phys_avail[indx + 1] - 1,
-			    (uintmax_t)size, (uintmax_t)size / PAGE_SIZE);
+			    (uintmax_t)size / 1024, (uintmax_t)size / PAGE_SIZE);
 		}
 	}
 
@@ -392,6 +392,9 @@ cpu_startup(void *dummy)
 	    (uintmax_t)ptoa(cnt.v_free_count),
 	    (uintmax_t)ptoa(cnt.v_free_count) / 1048576);
 
+	if (bootverbose)
+		arm_devmap_print_table();
+
 	bufinit();
 	vm_pager_bufferinit();
 	pcb->un_32.pcb32_und_sp = (u_int)thread0.td_kstack +