diff options
Diffstat (limited to 'riscv/riscv_mem.sail')
| -rw-r--r-- | riscv/riscv_mem.sail | 3 |
1 files changed, 1 insertions, 2 deletions
diff --git a/riscv/riscv_mem.sail b/riscv/riscv_mem.sail index 9ead3aeb..008c1642 100644 --- a/riscv/riscv_mem.sail +++ b/riscv/riscv_mem.sail @@ -92,6 +92,7 @@ function phys_mem_write(addr : xlenbits, width : atom('n), data: bits(8 * 'n)) - else MemException(E_SAMO_Access_Fault) } +// dispatches to MMIO regions or physical memory regions depending on physical memory map function checked_mem_write(addr : xlenbits, width : atom('n), data: bits(8 * 'n)) -> forall 'n, 'n > 0. MemoryOpResult(unit) = if within_mmio_writable(addr, width) then mmio_write(addr, width, data) @@ -133,8 +134,6 @@ function mem_write_value (addr, width, value, aq, rl, con) = { } } -val "speculate_conditional_success" : unit -> bool effect {exmem} - val MEM_fence_rw_rw = {ocaml: "skip", lem: "MEM_fence_rw_rw"} : unit -> unit effect {barr} val MEM_fence_r_rw = {ocaml: "skip", lem: "MEM_fence_r_rw"} : unit -> unit effect {barr} val MEM_fence_r_r = {ocaml: "skip", lem: "MEM_fence_r_r"} : unit -> unit effect {barr} |