Test RDWI

Run RDWI in model, using armmem

ARM RDWI ()
"is RR to same location in ppo?, internal write variation"
Prefetch=1:z=T
{
P1:R6=x; P1:R7=y; P1:R8=z;
P0:R7=y; P0:R8=z;
}
P0           |P1             ;
mov R1,1     |ldr R1,R7      ;
str R1,R8    |and R9,R1,0    ;
dmb          |ldr R3,[R9,R6] ;
mov R2,2     |mov R10,1      ;
str R2,R7    |str R10,R6     ;
             |ldr R4,R6      ;
             |and R10,R4,0   ;
             |ldr R2,[R10,R8];

exists (P1:R1=2 /\ P1:R2=0 /\ P1:R3=0 /\ P1:R4=1)