Test F2V

AArch64 F2V
{
[PTE(x)]=(valid:0);
0:X1=(oa:PA(x),valid:1);
0:X2=PTE(x); 0:X3=x;
1:X3=x
}

P0                 | P1               ;
   STR  X1,[X2]    |    MOV  W4,#1    ;
   DSB  ISH        |    STR  W4, [X3] ; (* new permissions *)
   LSR  X9,X3,#12  | L0:STR  W4, [X3] ; (* old permissions *)
   TLBI VAAE1IS,X9 |                  ;
   DSB  ISH        |                  ;
   LDR  W7,[X3]    |                  ;
exists (0:X7=0 /\ fault(P1:L0,x,MMU:Translation))