Test ISA10+BIS

“RDW’, that is “Read Different Writes”, Forbid.

RISCV ISA10+BIS

(* Variation on ISA V2.3 fig. 1.10, RDW *)
{
  int x; int y; int z;
  0:s0=x; 0:s1=y;
  1:s0=x; 1:s1=y; 1:s2=z;
  2:s2=z;
  
}

 P0            | P1           | P2          ;
 li t1,1       | lw a0,0(s1)  | li t1,1     ;
 sw t1,0(s0)   | xor t2,a0,a0 | sw t1,0(s2) ;
 fence w,w     | add s3,s2,t2 |             ;
 sw t1,0(s1)   | lw a1,0(s3)  |             ;
               | lw a2,0(s2)  |             ;
               | xor t3,a2,a2 |             ;
               | add s0,s0,t3 |             ;
               | lw a3,0(s0)  |             ;

~exists (1:a0=1 /\ 1:a3 = 0 /\ 1:a1 = 0 /\ 1:a2 = 1)