diff options
| author | Robert Norton | 2018-07-12 15:54:11 +0100 |
|---|---|---|
| committer | Robert Norton | 2018-07-12 15:54:15 +0100 |
| commit | 79ecf8b83b06a6bd1330e1f243826cbe951a9e7d (patch) | |
| tree | 5d3b76bdc57d48af47a37bc5580f2d88d1997c2a /mips/prelude.sail | |
| parent | 8195ac7e4d851e9901bfaae92997ea51914c09b2 (diff) | |
update arm and mips models for new type of write_ram builtin. Also fix c and interpreter implementations of same.
Diffstat (limited to 'mips/prelude.sail')
| -rw-r--r-- | mips/prelude.sail | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/mips/prelude.sail b/mips/prelude.sail index 037819bc..85060dda 100644 --- a/mips/prelude.sail +++ b/mips/prelude.sail @@ -125,10 +125,10 @@ overload min = {min_atom, min_nat, min_int} overload max = {max_atom, max_nat, max_int} val __WriteRAM = "write_ram" : forall 'n 'm. - (atom('m), atom('n), bits('m), bits('m), bits(8 * 'n)) -> unit effect {wmv} + (atom('m), atom('n), bits('m), bits('m), bits(8 * 'n)) -> bool effect {wmv} val __MIPS_write : forall 'n. (bits(64), atom('n), bits(8 * 'n)) -> unit effect {wmv} -function __MIPS_write (addr, width, data) = __WriteRAM(64, width, 0x0000_0000_0000_0000, addr, data) +function __MIPS_write (addr, width, data) = let _ = __WriteRAM(64, width, 0x0000_0000_0000_0000, addr, data) in () val __ReadRAM = "read_ram" : forall 'n 'm, 'n >= 0. (atom('m), atom('n), bits('m), bits('m)) -> bits(8 * 'n) effect {rmem} |
