diff --git a/src/arch/arm/32/kernel/vspace.c b/src/arch/arm/32/kernel/vspace.c
index 93b77e105..cfff1e0a4 100644
--- a/src/arch/arm/32/kernel/vspace.c
+++ b/src/arch/arm/32/kernel/vspace.c
@@ -162,33 +162,24 @@ BOOT_CODE void map_kernel_frame(paddr_t paddr, pptr_t vaddr, vm_rights_t vm_righ
 
     assert(vaddr >= PPTR_TOP); /* vaddr lies in the region the global PT covers */
 #ifndef CONFIG_ARM_HYPERVISOR_SUPPORT
+    word_t tex;
     if (vm_attributes_get_armPageCacheable(attributes)) {
-        armKSGlobalPT[idx] =
-            pte_pte_small_new(
-                paddr,
-                0, /* global */
-                SMP_TERNARY(1, 0), /* shareable if SMP enabled, otherwise unshared */
-                0, /* APX = 0, privileged full access */
-                5, /* TEX = 0b1(Cached)01(Outer Write Allocate) */
-                APFromVMRights(vm_rights),
-                0, /* C (Inner write allocate) */
-                1, /* B (Inner write allocate) */
-                0  /* executable */
-            );
+        tex = 5; /* TEX = 0b1(Cached)01(Outer Write Allocate) */
     } else {
-        armKSGlobalPT[idx] =
-            pte_pte_small_new(
-                paddr,
-                0, /* global */
-                SMP_TERNARY(1, 0), /* shareable if SMP enabled, otherwise unshared */
-                0, /* APX = 0, privileged full access */
-                0, /* TEX = 0 */
-                APFromVMRights(vm_rights),
-                0, /* Shared device */
-                1, /* Shared device */
-                0  /* executable */
-            );
+        tex = 0;
     }
+    armKSGlobalPT[idx] =
+        pte_pte_small_new(
+            paddr,
+            0, /* global */
+            SMP_TERNARY(1, 0), /* shareable if SMP enabled, otherwise unshared */
+            0, /* APX = 0, privileged full access */
+            tex,
+            APFromVMRights(vm_rights),
+            0, /* C (Inner write allocate) */
+            1, /* B (Inner write allocate) */
+            0  /* executable */
+        );
 #else /* CONFIG_ARM_HYPERVISOR_SUPPORT */
     armHSGlobalPT[idx] =
         pteS1_pteS1_small_new(
diff --git a/src/arch/arm/64/kernel/vspace.c b/src/arch/arm/64/kernel/vspace.c
index 206882fac..6ad9aeaa1 100644
--- a/src/arch/arm/64/kernel/vspace.c
+++ b/src/arch/arm/64/kernel/vspace.c
@@ -223,37 +223,27 @@ BOOT_CODE void map_kernel_frame(paddr_t paddr, pptr_t vaddr, vm_rights_t vm_righ
 {
     assert(vaddr >= PPTR_TOP);
 
+#ifdef CONFIG_ARM_HYPERVISOR_SUPPORT
+    word_t uxn = vm_attributes_get_armExecuteNever(attributes);
+#else
+    word_t uxn = 1; /* unprivileged execute never */
+#endif /* CONFIG_ARM_HYPERVISOR_SUPPORT */
+    word_t attr_index;
+    word_t shareable;
     if (vm_attributes_get_armPageCacheable(attributes)) {
-        armKSGlobalKernelPT[GET_PT_INDEX(vaddr)] = pte_new(
-#ifdef CONFIG_ARM_HYPERVISOR_SUPPORT
-                                                       vm_attributes_get_armExecuteNever(attributes),
-#else
-                                                       1, /* unprivileged execute never */
-#endif
-                                                       paddr,
-                                                       0,                          /* global */
-                                                       1,                          /* access flag */
-                                                       SMP_TERNARY(SMP_SHARE, 0),          /* Inner-shareable if SMP enabled, otherwise unshared */
-                                                       APFromVMRights(vm_rights),
-                                                       NORMAL,
-                                                       RESERVED
-                                                   );
+        attr_index = NORMAL;
+        shareable = SMP_TERNARY(SMP_SHARE, 0);
     } else {
-        armKSGlobalKernelPT[GET_PT_INDEX(vaddr)] = pte_new(
-#ifdef CONFIG_ARM_HYPERVISOR_SUPPORT
-                                                       vm_attributes_get_armExecuteNever(attributes),
-#else
-                                                       1, /* unprivileged execute never */
-#endif
-                                                       paddr,
-                                                       0,                          /* global */
-                                                       1,                          /* access flag */
-                                                       0,                          /* Ignored - Outter shareable */
-                                                       APFromVMRights(vm_rights),
-                                                       DEVICE_nGnRnE,
-                                                       RESERVED
-                                                   );
+        attr_index = DEVICE_nGnRnE;
+        shareable = 0;
     }
+    armKSGlobalKernelPT[GET_PT_INDEX(vaddr)] = pte_new(uxn, paddr,
+                                                       0, /* global */
+                                                       1, /* access flag */
+                                                       shareable,
+                                                       APFromVMRights(vm_rights),
+                                                       attr_index,
+                                                       RESERVED);
 }
 
 BOOT_CODE void map_kernel_window(void)