Test IRIW-I2Vpte

AArch64 IRIW-I2Vpte
{
0:X10=pte_x; 3:X10=pte_x;
0:X1=(oa:phy_y,valid:0);
3:X2=(oa:phy_z,valid:1);
1:X4=x; 2:X4=x;
y=1; z=2;
}
P0           | P1             | P2              | P3          ;
STR X1,[X10] | L0:LDR X5,[X4] | LDR X5,[X4]     | STR X2,[X10];
             | LDR X6,[X4]    | L1: LDR X6,[X4] |             ;
exists (1:X6=0 /\ 2:X5=0 /\ [PTE(x)]=(oa:PA(y), valid:0) /\ fault(P1:L0,x,MMU:Translation) /\ fault(P2:L1,x,MMU:Translation)) \/ (1:X6=0 /\ 2:X5=0 /\ [PTE(x)]=(oa:PA(z)) /\ fault(P1:L0,x,MMU:Translation) /\ fault(P2:L1,x,MMU:Translation)) \/ (1:X6=0 /\ 2:X5=0 /\ [PTE(x)]=(oa:PA(z)) /\ fault(P2:L1,x,MMU:Translation) /\ ~fault(P1:L0,x)) \/ (1:X6=0 /\ 2:X5=2 /\ [PTE(x)]=(oa:PA(y), valid:0) /\ fault(P1:L0,x,MMU:Translation) /\ fault(P2:L1,x,MMU:Translation)) \/ (1:X6=0 /\ 2:X5=2 /\ [PTE(x)]=(oa:PA(z)) /\ fault(P1:L0,x,MMU:Translation) /\ fault(P2:L1,x,MMU:Translation)) \/ (1:X6=0 /\ 2:X5=2 /\ [PTE(x)]=(oa:PA(z)) /\ fault(P2:L1,x,MMU:Translation) /\ ~fault(P1:L0,x)) \/ (1:X6=2 /\ 2:X5=0 /\ [PTE(x)]=(oa:PA(y), valid:0) /\ fault(P2:L1,x,MMU:Translation) /\ ~fault(P1:L0,x)) \/ (1:X6=2 /\ 2:X5=0 /\ [PTE(x)]=(oa:PA(z)) /\ fault(P2:L1,x,MMU:Translation) /\ ~fault(P1:L0,x)) \/ (1:X6=2 /\ 2:X5=2 /\ [PTE(x)]=(oa:PA(z)) /\ fault(P2:L1,x,MMU:Translation) /\ ~fault(P1:L0,x))