…
AArch64 IRIW-V2Vpte+64
{
0:X10=pte_x; 3:X10=pte_x;
0:X1=(oa:phy_y,valid:1);
3:X2=(oa:phy_z,valid:1);
1:X4=x; 2:X4=x;
int64_t x;
int64_t y=1; int64_t z=2;
int64_t 1:X5;
int64_t 1:X6;
int64_t 2:X5;
int64_t 2:X6;
}
P0 | P1 | P2 | P3 ;
STR X1,[X10] | LDR X5,[X4] | LDR X5,[X4] | STR X2,[X10];
| LDR X6,[X4] | LDR X6,[X4] | ;
exists (1:X5=0 /\ 1:X6=0 /\ 2:X5=0 /\ 2:X6=1 /\ [PTE(x)]=(oa:PA(z))) \/ (1:X5=0 /\ 1:X6=0 /\ 2:X5=1 /\ 2:X6=0 /\ [PTE(x)]=(oa:PA(y))) \/ (1:X5=0 /\ 1:X6=0 /\ 2:X5=1 /\ 2:X6=0 /\ [PTE(x)]=(oa:PA(z))) \/ (1:X5=0 /\ 1:X6=0 /\ 2:X5=1 /\ 2:X6=2 /\ [PTE(x)]=(oa:PA(y))) \/ (1:X5=0 /\ 1:X6=0 /\ 2:X5=1 /\ 2:X6=2 /\ [PTE(x)]=(oa:PA(z))) \/ (1:X5=0 /\ 1:X6=0 /\ 2:X5=2 /\ 2:X6=0 /\ [PTE(x)]=(oa:PA(y))) \/ (1:X5=0 /\ 1:X6=0 /\ 2:X5=2 /\ 2:X6=0 /\ [PTE(x)]=(oa:PA(z))) \/ (1:X5=0 /\ 1:X6=0 /\ 2:X5=2 /\ 2:X6=1 /\ [PTE(x)]=(oa:PA(y))) \/ (1:X5=0 /\ 1:X6=0 /\ 2:X5=2 /\ 2:X6=1 /\ [PTE(x)]=(oa:PA(z))) \/ (1:X5=0 /\ 1:X6=1 /\ 2:X5=0 /\ 2:X6=1 /\ [PTE(x)]=(oa:PA(y))) \/ (1:X5=0 /\ 1:X6=1 /\ 2:X5=0 /\ 2:X6=1 /\ [PTE(x)]=(oa:PA(z))) \/ (1:X5=0 /\ 1:X6=1 /\ 2:X5=0 /\ 2:X6=2 /\ [PTE(x)]=(oa:PA(y))) \/ (1:X5=0 /\ 1:X6=1 /\ 2:X5=0 /\ 2:X6=2 /\ [PTE(x)]=(oa:PA(z))) \/ (1:X5=0 /\ 1:X6=1 /\ 2:X5=1 /\ 2:X6=0 /\ [PTE(x)]=(oa:PA(y))) \/ (1:X5=0 /\ 1:X6=1 /\ 2:X5=1 /\ 2:X6=0 /\ [PTE(x)]=(oa:PA(z))) \/ (1:X5=0 /\ 1:X6=1 /\ 2:X5=1 /\ 2:X6=1 /\ [PTE(x)]=(oa:PA(y))) \/ (1:X5=0 /\ 1:X6=1 /\ 2:X5=1 /\ 2:X6=1 /\ [PTE(x)]=(oa:PA(z))) \/ (1:X5=0 /\ 1:X6=1 /\ 2:X5=1 /\ 2:X6=2 /\ [PTE(x)]=(oa:PA(y))) \/ (1:X5=0 /\ 1:X6=1 /\ 2:X5=1 /\ 2:X6=2 /\ [PTE(x)]=(oa:PA(z))) \/ (1:X5=0 /\ 1:X6=1 /\ 2:X5=2 /\ 2:X6=0 /\ [PTE(x)]=(oa:PA(y))) \/ (1:X5=0 /\ 1:X6=1 /\ 2:X5=2 /\ 2:X6=0 /\ [PTE(x)]=(oa:PA(z))) \/ (1:X5=0 /\ 1:X6=1 /\ 2:X5=2 /\ 2:X6=1 /\ [PTE(x)]=(oa:PA(y))) \/ (1:X5=0 /\ 1:X6=1 /\ 2:X5=2 /\ 2:X6=1 /\ [PTE(x)]=(oa:PA(z))) \/ (1:X5=0 /\ 1:X6=1 /\ 2:X5=2 /\ 2:X6=2 /\ [PTE(x)]=(oa:PA(y))) \/ (1:X5=0 /\ 1:X6=1 /\ 2:X5=2 /\ 2:X6=2 /\ [PTE(x)]=(oa:PA(z))) \/ (1:X5=0 /\ 1:X6=2 /\ 2:X5=0 /\ 2:X6=1 /\ [PTE(x)]=(oa:PA(y))) \/ (1:X5=0 /\ 1:X6=2 /\ 2:X5=0 /\ 2:X6=1 /\ [PTE(x)]=(oa:PA(z))) \/ (1:X5=0 /\ 1:X6=2 /\ 2:X5=0 /\ 2:X6=2 /\ [PTE(x)]=(oa:PA(y))) \/ (1:X5=0 /\ 1:X6=2 /\ 2:X5=0 /\ 2:X6=2 /\ [PTE(x)]=(oa:PA(z))) \/ (1:X5=0 /\ 1:X6=2 /\ 2:X5=1 /\ 2:X6=0 /\ [PTE(x)]=(oa:PA(y))) \/ (1:X5=0 /\ 1:X6=2 /\ 2:X5=1 /\ 2:X6=0 /\ [PTE(x)]=(oa:PA(z))) \/ (1:X5=0 /\ 1:X6=2 /\ 2:X5=1 /\ 2:X6=1 /\ [PTE(x)]=(oa:PA(y))) \/ (1:X5=0 /\ 1:X6=2 /\ 2:X5=1 /\ 2:X6=1 /\ [PTE(x)]=(oa:PA(z))) \/ (1:X5=0 /\ 1:X6=2 /\ 2:X5=1 /\ 2:X6=2 /\ [PTE(x)]=(oa:PA(y))) \/ (1:X5=0 /\ 1:X6=2 /\ 2:X5=1 /\ 2:X6=2 /\ [PTE(x)]=(oa:PA(z))) \/ (1:X5=0 /\ 1:X6=2 /\ 2:X5=2 /\ 2:X6=0 /\ [PTE(x)]=(oa:PA(y))) \/ (1:X5=0 /\ 1:X6=2 /\ 2:X5=2 /\ 2:X6=0 /\ [PTE(x)]=(oa:PA(z))) \/ (1:X5=0 /\ 1:X6=2 /\ 2:X5=2 /\ 2:X6=1 /\ [PTE(x)]=(oa:PA(y))) \/ (1:X5=0 /\ 1:X6=2 /\ 2:X5=2 /\ 2:X6=1 /\ [PTE(x)]=(oa:PA(z))) \/ (1:X5=0 /\ 1:X6=2 /\ 2:X5=2 /\ 2:X6=2 /\ [PTE(x)]=(oa:PA(y))) \/ (1:X5=0 /\ 1:X6=2 /\ 2:X5=2 /\ 2:X6=2 /\ [PTE(x)]=(oa:PA(z))) \/ (1:X5=1 /\ 1:X6=0 /\ 2:X5=0 /\ 2:X6=0 /\ [PTE(x)]=(oa:PA(y))) \/ (1:X5=1 /\ 1:X6=0 /\ 2:X5=0 /\ 2:X6=0 /\ [PTE(x)]=(oa:PA(z))) \/ (1:X5=1 /\ 1:X6=0 /\ 2:X5=0 /\ 2:X6=1 /\ [PTE(x)]=(oa:PA(y))) \/ (1:X5=1 /\ 1:X6=0 /\ 2:X5=0 /\ 2:X6=1 /\ [PTE(x)]=(oa:PA(z))) \/ (1:X5=1 /\ 1:X6=0 /\ 2:X5=0 /\ 2:X6=2 /\ [PTE(x)]=(oa:PA(y))) \/ (1:X5=1 /\ 1:X6=0 /\ 2:X5=0 /\ 2:X6=2 /\ [PTE(x)]=(oa:PA(z))) \/ (1:X5=1 /\ 1:X6=0 /\ 2:X5=1 /\ 2:X6=0 /\ [PTE(x)]=(oa:PA(y))) \/ (1:X5=1 /\ 1:X6=0 /\ 2:X5=1 /\ 2:X6=0 /\ [PTE(x)]=(oa:PA(z))) \/ (1:X5=1 /\ 1:X6=0 /\ 2:X5=1 /\ 2:X6=1 /\ [PTE(x)]=(oa:PA(y))) \/ (1:X5=1 /\ 1:X6=0 /\ 2:X5=1 /\ 2:X6=1 /\ [PTE(x)]=(oa:PA(z))) \/ (1:X5=1 /\ 1:X6=0 /\ 2:X5=1 /\ 2:X6=2 /\ [PTE(x)]=(oa:PA(y))) \/ (1:X5=1 /\ 1:X6=0 /\ 2:X5=1 /\ 2:X6=2 /\ [PTE(x)]=(oa:PA(z))) \/ (1:X5=1 /\ 1:X6=0 /\ 2:X5=2 /\ 2:X6=0 /\ [PTE(x)]=(oa:PA(y))) \/ (1:X5=1 /\ 1:X6=0 /\ 2:X5=2 /\ 2:X6=0 /\ [PTE(x)]=(oa:PA(z))) \/ (1:X5=1 /\ 1:X6=0 /\ 2:X5=2 /\ 2:X6=1 /\ [PTE(x)]=(oa:PA(y))) \/ (1:X5=1 /\ 1:X6=0 /\ 2:X5=2 /\ 2:X6=1 /\ [PTE(x)]=(oa:PA(z))) \/ (1:X5=1 /\ 1:X6=0 /\ 2:X5=2 /\ 2:X6=2 /\ [PTE(x)]=(oa:PA(y))) \/ (1:X5=1 /\ 1:X6=0 /\ 2:X5=2 /\ 2:X6=2 /\ [PTE(x)]=(oa:PA(z))) \/ (1:X5=1 /\ 1:X6=1 /\ 2:X5=0 /\ 2:X6=1 /\ [PTE(x)]=(oa:PA(y))) \/ (1:X5=1 /\ 1:X6=1 /\ 2:X5=0 /\ 2:X6=1 /\ [PTE(x)]=(oa:PA(z))) \/ (1:X5=1 /\ 1:X6=1 /\ 2:X5=0 /\ 2:X6=2 /\ [PTE(x)]=(oa:PA(y))) \/ (1:X5=1 /\ 1:X6=1 /\ 2:X5=0 /\ 2:X6=2 /\ [PTE(x)]=(oa:PA(z))) \/ (1:X5=1 /\ 1:X6=1 /\ 2:X5=1 /\ 2:X6=0 /\ [PTE(x)]=(oa:PA(y))) \/ (1:X5=1 /\ 1:X6=1 /\ 2:X5=1 /\ 2:X6=0 /\ [PTE(x)]=(oa:PA(z))) \/ (1:X5=1 /\ 1:X6=1 /\ 2:X5=1 /\ 2:X6=2 /\ [PTE(x)]=(oa:PA(y))) \/ (1:X5=1 /\ 1:X6=1 /\ 2:X5=1 /\ 2:X6=2 /\ [PTE(x)]=(oa:PA(z))) \/ (1:X5=1 /\ 1:X6=1 /\ 2:X5=2 /\ 2:X6=0 /\ [PTE(x)]=(oa:PA(y))) \/ (1:X5=1 /\ 1:X6=1 /\ 2:X5=2 /\ 2:X6=0 /\ [PTE(x)]=(oa:PA(z))) \/ (1:X5=1 /\ 1:X6=1 /\ 2:X5=2 /\ 2:X6=1 /\ [PTE(x)]=(oa:PA(y))) \/ (1:X5=1 /\ 1:X6=1 /\ 2:X5=2 /\ 2:X6=1 /\ [PTE(x)]=(oa:PA(z))) \/ (1:X5=1 /\ 1:X6=2 /\ 2:X5=0 /\ 2:X6=0 /\ [PTE(x)]=(oa:PA(y))) \/ (1:X5=1 /\ 1:X6=2 /\ 2:X5=0 /\ 2:X6=0 /\ [PTE(x)]=(oa:PA(z))) \/ (1:X5=1 /\ 1:X6=2 /\ 2:X5=0 /\ 2:X6=1 /\ [PTE(x)]=(oa:PA(y))) \/ (1:X5=1 /\ 1:X6=2 /\ 2:X5=0 /\ 2:X6=1 /\ [PTE(x)]=(oa:PA(z))) \/ (1:X5=1 /\ 1:X6=2 /\ 2:X5=0 /\ 2:X6=2 /\ [PTE(x)]=(oa:PA(y))) \/ (1:X5=1 /\ 1:X6=2 /\ 2:X5=0 /\ 2:X6=2 /\ [PTE(x)]=(oa:PA(z))) \/ (1:X5=1 /\ 1:X6=2 /\ 2:X5=1 /\ 2:X6=0 /\ [PTE(x)]=(oa:PA(y))) \/ (1:X5=1 /\ 1:X6=2 /\ 2:X5=1 /\ 2:X6=0 /\ [PTE(x)]=(oa:PA(z))) \/ (1:X5=1 /\ 1:X6=2 /\ 2:X5=1 /\ 2:X6=1 /\ [PTE(x)]=(oa:PA(y))) \/ (1:X5=1 /\ 1:X6=2 /\ 2:X5=1 /\ 2:X6=1 /\ [PTE(x)]=(oa:PA(z))) \/ (1:X5=1 /\ 1:X6=2 /\ 2:X5=1 /\ 2:X6=2 /\ [PTE(x)]=(oa:PA(y))) \/ (1:X5=1 /\ 1:X6=2 /\ 2:X5=1 /\ 2:X6=2 /\ [PTE(x)]=(oa:PA(z))) \/ (1:X5=1 /\ 1:X6=2 /\ 2:X5=2 /\ 2:X6=0 /\ [PTE(x)]=(oa:PA(y))) \/ (1:X5=1 /\ 1:X6=2 /\ 2:X5=2 /\ 2:X6=0 /\ [PTE(x)]=(oa:PA(z))) \/ (1:X5=1 /\ 1:X6=2 /\ 2:X5=2 /\ 2:X6=1 /\ [PTE(x)]=(oa:PA(y))) \/ (1:X5=1 /\ 1:X6=2 /\ 2:X5=2 /\ 2:X6=1 /\ [PTE(x)]=(oa:PA(z))) \/ (1:X5=1 /\ 1:X6=2 /\ 2:X5=2 /\ 2:X6=2 /\ [PTE(x)]=(oa:PA(y))) \/ (1:X5=1 /\ 1:X6=2 /\ 2:X5=2 /\ 2:X6=2 /\ [PTE(x)]=(oa:PA(z))) \/ (1:X5=2 /\ 1:X6=0 /\ 2:X5=0 /\ 2:X6=0 /\ [PTE(x)]=(oa:PA(y))) \/ (1:X5=2 /\ 1:X6=0 /\ 2:X5=0 /\ 2:X6=0 /\ [PTE(x)]=(oa:PA(z))) \/ (1:X5=2 /\ 1:X6=0 /\ 2:X5=0 /\ 2:X6=1 /\ [PTE(x)]=(oa:PA(y))) \/ (1:X5=2 /\ 1:X6=0 /\ 2:X5=0 /\ 2:X6=1 /\ [PTE(x)]=(oa:PA(z))) \/ (1:X5=2 /\ 1:X6=0 /\ 2:X5=0 /\ 2:X6=2 /\ [PTE(x)]=(oa:PA(y))) \/ (1:X5=2 /\ 1:X6=0 /\ 2:X5=0 /\ 2:X6=2 /\ [PTE(x)]=(oa:PA(z))) \/ (1:X5=2 /\ 1:X6=0 /\ 2:X5=1 /\ 2:X6=0 /\ [PTE(x)]=(oa:PA(y))) \/ (1:X5=2 /\ 1:X6=0 /\ 2:X5=1 /\ 2:X6=0 /\ [PTE(x)]=(oa:PA(z))) \/ (1:X5=2 /\ 1:X6=0 /\ 2:X5=1 /\ 2:X6=1 /\ [PTE(x)]=(oa:PA(y))) \/ (1:X5=2 /\ 1:X6=0 /\ 2:X5=1 /\ 2:X6=1 /\ [PTE(x)]=(oa:PA(z))) \/ (1:X5=2 /\ 1:X6=0 /\ 2:X5=1 /\ 2:X6=2 /\ [PTE(x)]=(oa:PA(y))) \/ (1:X5=2 /\ 1:X6=0 /\ 2:X5=1 /\ 2:X6=2 /\ [PTE(x)]=(oa:PA(z))) \/ (1:X5=2 /\ 1:X6=0 /\ 2:X5=2 /\ 2:X6=0 /\ [PTE(x)]=(oa:PA(y))) \/ (1:X5=2 /\ 1:X6=0 /\ 2:X5=2 /\ 2:X6=0 /\ [PTE(x)]=(oa:PA(z))) \/ (1:X5=2 /\ 1:X6=0 /\ 2:X5=2 /\ 2:X6=1 /\ [PTE(x)]=(oa:PA(y))) \/ (1:X5=2 /\ 1:X6=0 /\ 2:X5=2 /\ 2:X6=1 /\ [PTE(x)]=(oa:PA(z))) \/ (1:X5=2 /\ 1:X6=0 /\ 2:X5=2 /\ 2:X6=2 /\ [PTE(x)]=(oa:PA(y))) \/ (1:X5=2 /\ 1:X6=0 /\ 2:X5=2 /\ 2:X6=2 /\ [PTE(x)]=(oa:PA(z))) \/ (1:X5=2 /\ 1:X6=1 /\ 2:X5=0 /\ 2:X6=0 /\ [PTE(x)]=(oa:PA(y))) \/ (1:X5=2 /\ 1:X6=1 /\ 2:X5=0 /\ 2:X6=0 /\ [PTE(x)]=(oa:PA(z))) \/ (1:X5=2 /\ 1:X6=1 /\ 2:X5=0 /\ 2:X6=1 /\ [PTE(x)]=(oa:PA(y))) \/ (1:X5=2 /\ 1:X6=1 /\ 2:X5=0 /\ 2:X6=1 /\ [PTE(x)]=(oa:PA(z))) \/ (1:X5=2 /\ 1:X6=1 /\ 2:X5=0 /\ 2:X6=2 /\ [PTE(x)]=(oa:PA(y))) \/ (1:X5=2 /\ 1:X6=1 /\ 2:X5=0 /\ 2:X6=2 /\ [PTE(x)]=(oa:PA(z))) \/ (1:X5=2 /\ 1:X6=1 /\ 2:X5=1 /\ 2:X6=0 /\ [PTE(x)]=(oa:PA(y))) \/ (1:X5=2 /\ 1:X6=1 /\ 2:X5=1 /\ 2:X6=0 /\ [PTE(x)]=(oa:PA(z))) \/ (1:X5=2 /\ 1:X6=1 /\ 2:X5=1 /\ 2:X6=1 /\ [PTE(x)]=(oa:PA(y))) \/ (1:X5=2 /\ 1:X6=1 /\ 2:X5=1 /\ 2:X6=1 /\ [PTE(x)]=(oa:PA(z))) \/ (1:X5=2 /\ 1:X6=1 /\ 2:X5=1 /\ 2:X6=2 /\ [PTE(x)]=(oa:PA(y))) \/ (1:X5=2 /\ 1:X6=1 /\ 2:X5=1 /\ 2:X6=2 /\ [PTE(x)]=(oa:PA(z))) \/ (1:X5=2 /\ 1:X6=1 /\ 2:X5=2 /\ 2:X6=0 /\ [PTE(x)]=(oa:PA(y))) \/ (1:X5=2 /\ 1:X6=1 /\ 2:X5=2 /\ 2:X6=0 /\ [PTE(x)]=(oa:PA(z))) \/ (1:X5=2 /\ 1:X6=1 /\ 2:X5=2 /\ 2:X6=1 /\ [PTE(x)]=(oa:PA(y))) \/ (1:X5=2 /\ 1:X6=1 /\ 2:X5=2 /\ 2:X6=1 /\ [PTE(x)]=(oa:PA(z))) \/ (1:X5=2 /\ 1:X6=1 /\ 2:X5=2 /\ 2:X6=2 /\ [PTE(x)]=(oa:PA(y))) \/ (1:X5=2 /\ 1:X6=1 /\ 2:X5=2 /\ 2:X6=2 /\ [PTE(x)]=(oa:PA(z))) \/ (1:X5=2 /\ 1:X6=2 /\ 2:X5=0 /\ 2:X6=1 /\ [PTE(x)]=(oa:PA(y))) \/ (1:X5=2 /\ 1:X6=2 /\ 2:X5=0 /\ 2:X6=1 /\ [PTE(x)]=(oa:PA(z))) \/ (1:X5=2 /\ 1:X6=2 /\ 2:X5=0 /\ 2:X6=2 /\ [PTE(x)]=(oa:PA(y))) \/ (1:X5=2 /\ 1:X6=2 /\ 2:X5=1 /\ 2:X6=0 /\ [PTE(x)]=(oa:PA(y))) \/ (1:X5=2 /\ 1:X6=2 /\ 2:X5=1 /\ 2:X6=0 /\ [PTE(x)]=(oa:PA(z))) \/ (1:X5=2 /\ 1:X6=2 /\ 2:X5=1 /\ 2:X6=2 /\ [PTE(x)]=(oa:PA(y))) \/ (1:X5=2 /\ 1:X6=2 /\ 2:X5=1 /\ 2:X6=2 /\ [PTE(x)]=(oa:PA(z))) \/ (1:X5=2 /\ 1:X6=2 /\ 2:X5=2 /\ 2:X6=0 /\ [PTE(x)]=(oa:PA(y))) \/ (1:X5=2 /\ 1:X6=2 /\ 2:X5=2 /\ 2:X6=0 /\ [PTE(x)]=(oa:PA(z))) \/ (1:X5=2 /\ 1:X6=2 /\ 2:X5=2 /\ 2:X6=1 /\ [PTE(x)]=(oa:PA(y))) \/ (1:X5=2 /\ 1:X6=2 /\ 2:X5=2 /\ 2:X6=1 /\ [PTE(x)]=(oa:PA(z)))