diff options
Diffstat (limited to 'model')
| -rw-r--r-- | model/prelude_mem.sail | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/model/prelude_mem.sail b/model/prelude_mem.sail index 6cc768c..85d141b 100644 --- a/model/prelude_mem.sail +++ b/model/prelude_mem.sail @@ -19,7 +19,7 @@ capabilities and SIMD / vector instructions will also need more. */ type max_mem_access : Int = 16 -val write_ram = {lem: "write_ram"} : forall 'n, 0 < 'n <= max_mem_access . (write_kind, xlenbits, atom('n), bits(8 * 'n), mem_meta) -> bool effect {wmv, wmvt} +val write_ram = {lem: "write_ram", coq: "write_ram"} : forall 'n, 0 < 'n <= max_mem_access . (write_kind, xlenbits, atom('n), bits(8 * 'n), mem_meta) -> bool effect {wmv, wmvt} function write_ram(wk, addr, width, data, meta) = { /* Write out metadata only if the value write succeeds. * It is assumed for now that this write always succeeds; @@ -37,7 +37,7 @@ val write_ram_ea : forall 'n, 0 < 'n <= max_mem_access . (write_kind, xlenbits, function write_ram_ea(wk, addr, width) = __write_mem_ea(wk, sizeof(xlen), addr, width) -val read_ram = {lem: "read_ram"} : forall 'n, 0 < 'n <= max_mem_access . (read_kind, xlenbits, atom('n), bool) -> (bits(8 * 'n), mem_meta) effect {rmem, rmemt} +val read_ram = {lem: "read_ram", coq: "read_ram"} : forall 'n, 0 < 'n <= max_mem_access . (read_kind, xlenbits, atom('n), bool) -> (bits(8 * 'n), mem_meta) effect {rmem, rmemt} function read_ram(rk, addr, width, read_meta) = let meta = if read_meta then __ReadRAM_Meta(addr, width) else default_meta in (__read_mem(rk, sizeof(xlen), addr, width), meta) |