Test ISA-S-DEP-DATA-SUCCESS

RISCV ISA-S-DEP-DATA-SUCCESS

(* Data+Success dependency on P1, variation on an idea by D. Lustig,Forbid *)
{
1:s0=x; 1:s1=y; 1:s2=z;
0:s0=x; 0:s1=y;
}

 P0          | P1                ;
 li t1,1     | lw a0,0(s0)       ;
 sw t1,0(s1) | lr.w a1,0(s2)     ;
 fence w,w   | sc.w a1,a0,0(s2)  ; 
 sw t1,0(s0) | andi t2,a1,64     ;
             | addi t2,t2,2      ;
             | sw t2,0(s1)       ;
locations [1:a1;]
~exists 1:a0=1 /\ y=1