Test FL

AArch64 FL
(* FC + ctrl *)
{
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         | CBZ W1,L1    ;
 LSR X8,X4,#12   | MOV W3,#1    ;
 TLBI VAAE1IS,X8 |L0:           ;
 DSB ISH         | STR W3,[X4]  ;  
 MOV W3,#1       |L1:           ;
 STR W3,[X6]     |              ; 
exists (1:X1=1 /\ fault(P1:L0,x,MMU:Translation))