Test V2I-UP-DSB-TLBI-DSB-ISB2

AArch64 V2I-UP-DSB-TLBI-DSB-ISB2
{
pte_x=(oa:phy_x,valid:1);
0:X3=pte_x;
0:X2=(oa:phy_y,valid:0);
0:X4=x;
y=1;
}
P0             ;
STR X2,[X3]    ;
LDR X5,[X3]    ;
DSB ISH        ;
LSR X9,X4,#12  ;
TLBI VAAE1IS,X9;
DSB ISH        ;
ISB            ;
L0: LDR W1,[X4];
exists(0:X1=0 /\ 0:X5=(oa:phy_y,valid:0) /\ ~fault(P0:L0,x))