Test MP+Data-XX-Addr

RISCV MP+Data-XX-Addr
(*
Attempt to detect wether LR and SC are systematically in ppo or not.
This may reveal an unique reserved address register.
At the moment, none, thus in LR x;SC x; LR y; SC y; There is no ppo
in teh middle. Allow
*)

{
0:x6=x; 0:x8=y;
1:x6=y; 1:x8=z; 1:x11=a; 1:x16=x;
}
 P0          | P1                  ;
 ori x5,x0,1 | lw x5,0(x6)         ;
 sw x5,0(x6) | xor x7,x5,x5        ;
 fence w,w   | ori x7,x7,1         ;
 ori x7,x0,1 | lr.w x9,0(x8)       ;
 sw x7,0(x8) | sc.w x10,x7,0(x8)   ;
             | ori x12,x0,1        ;
             | lr.w x13,0(x11)     ;
             | sc.w x14,x12,0(x11) ;
             | andi x17,x13,2      ;
             | add x18,x16,x17     ;
             | lw x15,0(x18)       ;
exists
(a=1 /\ z=1 /\ 1:x14=0 /\ 1:x10=0 /\ 1:x5=1 /\ 1:x15=0)