RISCV ISA09+BIS
"Fence.w.wdWW Rfe Fri WsLeave RfBack DpAddrdR Fre"
Generator=diyone7 (version 7.47+3)
Prefetch=0:x=F,0:y=W,1:y=F,1:x=T
Com=Rf Fr Rf
Orig=Fence.w.wdWW Rfe Fri WsLeave RfBack DpAddrdR Fre
(* Variaton on MP+fence+fri-rfi-addr: add one write *)
{
0:x6=x; 0:x8=y;
1:x6=y; 1:x11=x;
2:x6=y;
}
P0 | P1 | P2 ;
ori x5,x0,1 | lw x5,0(x6) | ori x5,x0,3 ;
sw x5,0(x6) | ori x7,x0,2 | sw x5,0(x6) ;
fence w,w | sw x7,0(x6) | ;
ori x7,x0,1 | lw x8,0(x6) | ;
sw x7,0(x8) | andi x9,x8,128 | ;
| add x12,x11,x9 | ;
| lw x10,0(x12) | ;
locations [y;]
exists (1:x5=1 /\ 1:x10=0 /\ 1:x8=2)