diff --git a/arch/arm64/src/common/arm64_mmu.h b/arch/arm64/src/common/arm64_mmu.h
index 1e95232f343..4337a7efa01 100644
--- a/arch/arm64/src/common/arm64_mmu.h
+++ b/arch/arm64/src/common/arm64_mmu.h
@@ -186,6 +186,26 @@
 #define TTBR_ASID_WIDTH             (16)
 #define TTBR_ASID_MASK              (((1UL << TTBR_ASID_WIDTH) - 1) << TTBR_ASID_SHIFT)
 
+/* TLBI instruction */
+
+#define TLBI_VADDR_SHIFT            (0)
+#define TLBI_VADDR_INPUT_SHIFT      (12) /* From input vaddr to TLBI vaddr field */
+#define TLBI_VADDR_WIDTH            (43)
+#define TLBI_VADDR_MASK             (((1UL << TLBI_VADDR_WIDTH) - 1) << TLBI_VADDR_SHIFT)
+#define TLBI_ASID_SHIFT             (48)
+#define TLBI_ASID_WIDTH             (16)
+#define TLBI_ASID_MASK              (((1UL << TLBI_ASID_WIDTH) - 1) << TLBI_ASID_SHIFT)
+
+/* Create an argument suitable for TLBI, with vaddr and asid as inputs */
+
+#define TLBI_ARG(vaddr, asid)                                       \
+  ({                                                                \
+    uintptr_t __arg;                                                \
+    __arg  = ((vaddr) >> TLBI_VADDR_INPUT_SHIFT) & TLBI_VADDR_MASK; \
+    __arg |= (uintptr_t)(asid) << TLBI_ASID_SHIFT;                  \
+    __arg;                                                          \
+  })
+
 /* Convenience macros to represent the ARMv8-A-specific
  * configuration for memory access permission and
  * cache-ability attribution.
@@ -358,7 +378,7 @@ static inline void mmu_invalidate_tlb_by_vaddr(uintptr_t vaddr)
       "dsb ish\n"
       "isb"
       :
-      : "r" (vaddr)
+      : "r" (TLBI_ARG(vaddr, 0))
       : "memory"
     );
 }