diff options
| author | Brian Campbell | 2020-08-07 18:09:39 +0100 |
|---|---|---|
| committer | Brian Campbell | 2020-08-07 18:09:39 +0100 |
| commit | a4c44cef89eb7b252ac2e66a878b093ecfbbd99f (patch) | |
| tree | b456f4621d28919e19e9fd17cfe43d52f65aa390 /lib | |
| parent | 7f53a4db1d3c36524707761446a8167f69ddd357 (diff) | |
| parent | 82d6faf3596037b17a1b61665ec4f3e57cf95a61 (diff) | |
Merge branch 'monads' into sail2
Diffstat (limited to 'lib')
| -rw-r--r-- | lib/regfp.sail | 8 |
1 files changed, 8 insertions, 0 deletions
diff --git a/lib/regfp.sail b/lib/regfp.sail index 7e5c9153..d6af7cf7 100644 --- a/lib/regfp.sail +++ b/lib/regfp.sail @@ -175,6 +175,10 @@ val __read_mem = { ocaml: "Platform.read_mem", c: "platform_read_mem", _: "read_mem" } : forall 'n (constant 'addrsize : Int), 'n > 0 & 'addrsize in {32, 64}. (read_kind, int('addrsize), bits('addrsize), int('n)) -> bits(8 * 'n) effect {rmem} +val __read_memt + = { ocaml: "Platform.read_memt", c: "platform_read_memt", _: "read_memt" } + : forall 'n (constant 'addrsize : Int), 'n > 0 & 'addrsize in {32, 64}. + (read_kind, bits('addrsize), int('n)) -> (bits(8 * 'n), bit) effect {rmemt} val __write_mem_ea = { ocaml: "Platform.write_mem_ea", c: "platform_write_mem_ea", _: "write_mem_ea" } : forall 'n (constant 'addrsize : Int), 'n > 0 & 'addrsize in {32, 64}. @@ -183,6 +187,10 @@ val __write_mem = { ocaml: "Platform.write_mem", c: "platform_write_mem", _: "write_mem" } : forall 'n (constant 'addrsize : Int), 'n > 0 & 'addrsize in {32, 64}. (write_kind, int('addrsize), bits('addrsize), int('n), bits(8 * 'n)) -> bool effect {wmv} +val __write_memt + = { ocaml: "Platform.write_memt", c: "platform_write_memt", _: "write_memt" } + : forall 'n (constant 'addrsize : Int), 'n > 0 & 'addrsize in {32, 64}. + (write_kind, bits('addrsize), int('n), bits(8 * 'n), bit) -> bool effect {wmvt} val __excl_res = { ocaml: "Platform.excl_res", c: "platform_excl_res", _: "excl_result" } : unit -> bool effect {exmem} |