diff --git a/sys/arm64/arm64/pmap.c b/sys/arm64/arm64/pmap.c
--- a/sys/arm64/arm64/pmap.c
+++ b/sys/arm64/arm64/pmap.c
@@ -2051,21 +2051,14 @@
 	uint64_t r;
 
 	PMAP_ASSERT_STAGE1(pmap);
+	MPASS(pmap != kernel_pmap);
 
 	dsb(ishst);
-	if (pmap == kernel_pmap) {
-		__asm __volatile("tlbi vmalle1is");
-		if (pmap_multiple_tlbi) {
-			dsb(ish);
-			__asm __volatile("tlbi vmalle1is");
-		}
-	} else {
-		r = ASID_TO_OPERAND(COOKIE_TO_ASID(pmap->pm_cookie));
+	r = ASID_TO_OPERAND(COOKIE_TO_ASID(pmap->pm_cookie));
+	__asm __volatile("tlbi aside1is, %0" : : "r" (r));
+	if (pmap_multiple_tlbi) {
+		dsb(ish);
 		__asm __volatile("tlbi aside1is, %0" : : "r" (r));
-		if (pmap_multiple_tlbi) {
-			dsb(ish);
-			__asm __volatile("tlbi aside1is, %0" : : "r" (r));
-		}
 	}
 	dsb(ish);
 	isb();