Test MP+DSB.ST+addr-TLBI-DSB

AArch64 MP+DSB.ST+addr-TLBI-DSB
{ 
pte_x=(valid:0,oa:phy_x);
0:X2=pte_x;
0:X1=(valid:1,oa:phy_y);
0:X3=x; 1:X3=x;
y=1;
0:X8=z; 1:X8=z;
}
P0              | P1;
STR X1,[X2]     | LDR W7,[X8]    ;
DSB ST          | DSB LD         ;
MOV W7,#1       | LSR X9,X3,#12  ;
STR W7,[X8]     | TLBI VAAE1IS,X9;
                | DSB ISH        ;
                | L0:LDR W4,[X3];
exists (1:X4=0 /\ 1:X7=1 /\ fault(P1:L0,x,MMU:Translation))