Test V2I-R-DSB.ST-TLBI-DSB.ISH-ISB-R+W

AArch64 V2I-R-DSB.ST-TLBI-DSB.ISH-ISB-R+W
{
pte_x=(oa:phy_x,valid:1);

0:X3=pte_x;

0:X4=x;

1:X2=(oa:phy_x,valid:0);
1:X3=pte_x;
}
 P0             | P1          ;
 LDR X2,[X3]    | STR X2,[X3] ;
 DSB ST         |             ;
 LSR X9,X4,#12  |             ;
 TLBI VAAE1,X9  |             ;
 DSB ISH        |             ;
 ISB            |             ;
L0:             |             ;
 LDR W1,[X4]    |             ;
exists (0:X2=(oa:PA(x), valid:0) /\ ~fault(P0:L0,x))