Test PPOLDSTLD01

RISCV PPOLDSTLD01
"Fence.w.wdWW Rfe DpDatadW Rfi DpAddrdR Fre"
(*
 Test for ppo rule ld->st->ld, or (addr|data);rfi
  Forbid
*)
{
0:x6=x; 0:x8=y;
1:x6=y; 1:x8=z; 1:x12=x;
}
 P0          | P1              ;
 ori x5,x0,1 | lw x5,0(x6)     ;
 sw x5,0(x6) | andi x7,x5,128  ;
 fence w,w   | ori x7,x7,1     ;
 ori x7,x0,1 | sw x7,0(x8)     ;
 sw x7,0(x8) | lw x9,0(x8)     ;
             | andi x10,x9,128 ;
             | add x13,x12,x10 ;
             | lw x11,0(x13)   ;
exists
(1:x5=1 /\ 1:x9=1 /\ 1:x11=0)