Test F1c+Fatal

AArch64 F1c+Fatal
Variant=Fatal
{
[PTE(x)] = (db:0);
0:X1=(oa:PA(x),db:1);
0:X2=PTE(x); 0:X3=x; 0:X8=y;
1:X3=x; 1:X8=y;
}

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