AArch64 I2V-R-DSB.ST-ISB-R+W { pte_x=(oa:phy_x,valid:0); 0:X3=pte_x; 0:X1=1; 0:X4=x; 1:X3=pte_x; 1:X2=(oa:phy_x,valid:1); } P0 | P1 ; LDR X2,[X3] | STR X2,[X3] ; DSB ST | ; ISB | ; L0: | ; LDR W1,[X4] | ; exists (0:X2=(oa:PA(x)) /\ fault(P0:L0,x,MMU:Translation))