diff options
Diffstat (limited to 'lib/regfp.sail')
| -rw-r--r-- | lib/regfp.sail | 8 |
1 files changed, 5 insertions, 3 deletions
diff --git a/lib/regfp.sail b/lib/regfp.sail index 90af9b44..ce361cd6 100644 --- a/lib/regfp.sail +++ b/lib/regfp.sail @@ -116,13 +116,13 @@ union instruction_kind = { val __read_mem = { ocaml: "Platform.read_mem", c: "platform_read_mem", _: "read_mem" } - : forall 'n, 'n > 0. (read_kind, bits(64), int('n)) -> bits(8 * 'n) effect {rmem} + : forall 'n 'addrsize, 'n > 0 & 'addrsize in {32, 64}. (read_kind, int('addrsize), bits('addrsize), int('n)) -> bits(8 * 'n) effect {rmem} val __write_mem_ea = { ocaml: "Platform.write_mem_ea", c: "platform_write_mem_ea", _: "write_mem_ea" } - : forall 'n, 'n > 0. (write_kind, bits(64), int('n)) -> unit effect {eamem} + : forall 'n 'addrsize, 'n > 0 & 'addrsize in {32, 64}. (write_kind, int('addrsize), bits('addrsize), int('n)) -> unit effect {eamem} val __write_mem = { ocaml: "Platform.write_mem", c: "platform_write_mem", _: "write_mem" } - : forall 'n, 'n > 0. (write_kind, bits(64), int('n), bits(8 * 'n)) -> bool effect {wmv} + : forall 'n 'addrsize, 'n > 0 & 'addrsize in {32, 64}. (write_kind, int('addrsize), bits('addrsize), int('n), bits(8 * 'n)) -> bool effect {wmv} val __excl_res = { ocaml: "Platform.excl_res", c: "platform_excl_res", _: "excl_res" } : unit -> bool effect {exmem} @@ -131,10 +131,12 @@ val __barrier : barrier_kind -> unit effect {barr} +/* val __write : forall 'n, 'n > 0. (write_kind, bits(64), int('n), bits(8 * 'n)) -> bool effect {eamem,wmv} function __write (wk, addr, len, value) = { __write_mem_ea(wk, addr, len); __write_mem(wk, addr, len, value) } +*/ $endif |