diff options
| author | Thomas Bauereiss <tb592@cl.cam.ac.uk> | 2019-10-07 16:00:56 +0100 |
|---|---|---|
| committer | Prashanth Mundkur <prashanth.mundkur@gmail.com> | 2019-10-09 22:04:15 -0700 |
| commit | 0e42c867fba498746405d2b878a12fd4d143c5d8 (patch) | |
| tree | 689e0ee412b6c91bcadb989148b72ad48b464a9b /model | |
| parent | a13c0a435804a9a8250054c2e9af2eacfa883164 (diff) | |
| download | sail-riscv-0e42c867fba498746405d2b878a12fd4d143c5d8.zip sail-riscv-0e42c867fba498746405d2b878a12fd4d143c5d8.tar.gz sail-riscv-0e42c867fba498746405d2b878a12fd4d143c5d8.tar.bz2 | |
Add {read,write}_ram for Coq
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) |