AArch64 V2I-RW+W { pte_x=(oa:phy_x,valid:1); 0:X3=pte_x; 1:X3=pte_x; 1:X2=(oa:phy_y,valid:0); 0:X4=x; 1:X4=x; y=1; 0:X6=(oa:phy_z,valid:1); z=2; } P0 | P1 ; | STR X2,[X3] ; LDR X5,[X3] | ; DSB ISH | ; LSR X9,X4,#12 | ; TLBI VAAE1IS,X9 | ; DSB ISH | ; ISB | ; STR X6,[X3] | ; exists(pte_x=(oa:phy_y,valid:0) /\ 0:X5=(oa:phy_y,valid:0))