diff --git a/sys/arm64/vmm/vmm_hyp.c b/sys/arm64/vmm/vmm_hyp.c
--- a/sys/arm64/vmm/vmm_hyp.c
+++ b/sys/arm64/vmm/vmm_hyp.c
@@ -619,6 +619,13 @@
 {
 	uint64_t end, r, start;
 	uint64_t host_vttbr;
+#ifdef VMM_VHE
+	uint64_t host_tcr;
+#endif
+
+#ifdef VMM_VHE
+	dsb(ishst);
+#endif
 
 #define	TLBI_VA_SHIFT			12
 #define	TLBI_VA_MASK			((1ul << 44) - 1)
@@ -631,6 +638,12 @@
 	WRITE_SPECIALREG(vttbr_el2, vttbr);
 	isb();
 
+#ifdef VMM_VHE
+	host_tcr = READ_SPECIALREG(tcr_el2);
+	WRITE_SPECIALREG(tcr_el2, host_tcr & ~HCR_TGE);
+	isb();
+#endif
+
 	/*
 	 * The CPU can cache the stage 1 + 2 combination so we need to ensure
 	 * the stage 2 is invalidated first, then when this has completed we
@@ -655,7 +668,12 @@
 	dsb(ish);
 	isb();
 
-	/* Switch back t othe host vttbr */
+#ifdef VMM_VHE
+	WRITE_SPECIALREG(tcr_el2, host_tcr);
+	isb();
+#endif
+
+	/* Switch back to the host vttbr */
 	WRITE_SPECIALREG(vttbr_el2, host_vttbr);
 	isb();
 }
@@ -665,6 +683,10 @@
 {
 	uint64_t host_vttbr;
 
+#ifdef VMM_VHE
+	dsb(ishst);
+#endif
+
 	/* Switch to the guest vttbr */
 	/* TODO: Handle Cortex-A57/A72 erratum 131936 */
 	host_vttbr = READ_SPECIALREG(vttbr_el2);