diff --git a/core/arch/arm/kernel/asm-defines.c b/core/arch/arm/kernel/asm-defines.c
index 6efc2035ad1..f2b7f381bcc 100644
--- a/core/arch/arm/kernel/asm-defines.c
+++ b/core/arch/arm/kernel/asm-defines.c
@@ -7,6 +7,7 @@
 #include <kernel/boot.h>
 #include <kernel/thread.h>
 #include <kernel/thread_private.h>
+#include <mm/core_mmu_arch.h>
 #include <sm/pm.h>
 #include <sm/sm.h>
 #include <types_ext.h>
@@ -157,4 +158,13 @@ DEFINES
 	       offsetof(struct boot_embdata, reloc_offset));
 	DEFINE(BOOT_EMBDATA_RELOC_LEN,
 	       offsetof(struct boot_embdata, reloc_len));
+
+#ifdef CORE_MMU_BASE_TABLE_OFFSET
+	/*
+	 * This define is too complex to be used as an argument for the
+	 * macros add_imm and sub_imm so evaluate it here.
+	 */
+	DEFINE(__CORE_MMU_BASE_TABLE_OFFSET, CORE_MMU_BASE_TABLE_OFFSET);
+#endif
+
 }
diff --git a/core/arch/arm/kernel/thread_a64.S b/core/arch/arm/kernel/thread_a64.S
index 9ceabfacdf3..256195e57c1 100644
--- a/core/arch/arm/kernel/thread_a64.S
+++ b/core/arch/arm/kernel/thread_a64.S
@@ -232,7 +232,7 @@ END_FUNC thread_unwind_user_mode
 
 		/* Update the mapping to use the full kernel mapping */
 		mrs	x0, ttbr0_el1
-		sub	x0, x0, #CORE_MMU_BASE_TABLE_OFFSET
+		sub_imm	x0, __CORE_MMU_BASE_TABLE_OFFSET
 		/* switch to kernel mode ASID */
 		bic	x0, x0, #BIT(TTBR_ASID_SHIFT)
 		msr	ttbr0_el1, x0
@@ -657,7 +657,7 @@ BTI(	bti	j)
 
 	/* Update the mapping to exclude the full kernel mapping */
 	mrs	x0, ttbr0_el1
-	add	x0, x0, #CORE_MMU_BASE_TABLE_OFFSET
+	add_imm	x0, __CORE_MMU_BASE_TABLE_OFFSET
 	orr	x0, x0, #BIT(TTBR_ASID_SHIFT) /* switch to user mode ASID */
 	msr	ttbr0_el1, x0
 	isb
@@ -729,8 +729,8 @@ icache_inv_user_range:
 BTI(	bti	j)
 	/* Update the mapping to exclude the full kernel mapping */
 	mrs	x5, ttbr0_el1	/* this register must be preserved */
-	add	x2, x5, #CORE_MMU_BASE_TABLE_OFFSET
-	orr	x2, x2, #BIT(TTBR_ASID_SHIFT) /* switch to user mode ASID */
+	orr	x2, x5, #BIT(TTBR_ASID_SHIFT) /* switch to user mode ASID */
+	add_imm	x2, __CORE_MMU_BASE_TABLE_OFFSET
 	msr	ttbr0_el1, x2
 	isb