diff options
Diffstat (limited to 'risc-v/riscv_extras_embed.lem')
| -rw-r--r-- | risc-v/riscv_extras_embed.lem | 8 |
1 files changed, 6 insertions, 2 deletions
diff --git a/risc-v/riscv_extras_embed.lem b/risc-v/riscv_extras_embed.lem index cbc8bd0d..1146d1cd 100644 --- a/risc-v/riscv_extras_embed.lem +++ b/risc-v/riscv_extras_embed.lem @@ -22,9 +22,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 +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_sync () = barrier Barrier_Isync +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 |