fixed the RISC-V fences (3 types: "rw,rw"/"r,rw"/"rw,w")

1 files changed, 6 insertions, 3 deletions

diff --git a/risc-v/riscv_extras_embed_sequential.lem b/risc-v/riscv_extras_embed_sequential.lem
index 7fb62161..f6709ff7 100644
--- a/risc-v/riscv_extras_embed_sequential.lem
+++ b/risc-v/riscv_extras_embed_sequential.lem
@@ -23,10 +23,13 @@ val MEMval_conditional     : (vector bitU * integer * vector bitU) -> M bitU
 let MEMval (_,_,v)                   = write_mem_val v >>= fun _ -> return ()
 let MEMval_conditional (_,_,v)       = write_mem_val v >>= fun b -> return (if b then B1 else B0)
 
-val MEM_sync  : unit -> M unit
-
-let MEM_sync () = barrier Barrier_MIPS_SYNC
+val MEM_fence_rw_rw : unit -> M unit
+val MEM_fence_r_rw  : unit -> M unit
+val MEM_fence_rw_w  : unit -> M unit
 
+let MEM_fence_rw_rw () = barrier Barrier_RISCV_rw_rw
+let MEM_fence_r_rw  () = barrier Barrier_RISCV_r_rw
+let MEM_fence_rw_w  () = barrier Barrier_RISCV_rw_w
 
 let duplicate (bit,len) =
   let bits = repeat [bit] len in