Test MP-ISB1

AArch64 MP-ISB1
{ 
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]      | LDAR X7,[X8]   ;
DSB ST           | L1: LDR X4,[X3];
MOV X7,#1        |                ;
STLR X7,[X8]     |                ;
L0: LDAR X4,[X3] |                ;
exists (1:X4=0 /\ 1:X7=0 /\ fault(P0:L0,x,MMU:Translation) /\ fault(P1:L1,x,MMU:Translation)) \/ (1:X4=0 /\ 1:X7=1 /\ fault(P0:L0,x,MMU:Translation) /\ fault(P1:L1,x,MMU:Translation)) \/ (1:X4=1 /\ 1:X7=0 /\ fault(P0:L0,x,MMU:Translation) /\ ~fault(P1:L1,x)) \/ (1:X4=1 /\ 1:X7=1 /\ fault(P0:L0,x,MMU:Translation) /\ ~fault(P1:L1,x))