Test FK

AArch64 FK
(* FC + data *)
{
0:X1=(oa:PA(x),valid:1);
0:X2=PTE(x);
[PTE(x)]=(valid:0);
0:X4=x; 0:X6=y;
1:X4=x; 1:X6=y;
}

  P0             |  P1          ;
 STR X1,[X2]     | LDR  W1,[X6] ;
 DSB ISH         | ORR W3,W1,#1 ;
 LSR X8,X4,#12   |L0:           ;
 TLBI VAAE1IS,X8 | STR W3,[X4]  ;  
 DSB ISH         |              ;
 MOV W3,#1       |              ;
 STR W3,[X6]     |              ; 
exists (1:X1=1 /\ fault(P1:L0,x,MMU:Translation))