diff options
| author | Brian Campbell | 2020-11-19 18:09:15 +0000 |
|---|---|---|
| committer | Brian Campbell | 2020-11-19 18:09:15 +0000 |
| commit | 75c6d051de21b72089e4a10477d35b4c8a886266 (patch) | |
| tree | d8e9d51b550802b0a4f4f4fb6df229998040adcf | |
| parent | 3d526b799eeb699fab913994e0739959688e9963 (diff) | |
Add write tag primitive
| -rw-r--r-- | lib/regfp.sail | 4 |
1 files changed, 4 insertions, 0 deletions
diff --git a/lib/regfp.sail b/lib/regfp.sail index d6af7cf7..2c44797f 100644 --- a/lib/regfp.sail +++ b/lib/regfp.sail @@ -191,6 +191,10 @@ 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 __write_tag + = { ocaml: "Platform.write_tag", c: "platform_write_tag", _: "write_tag" } + : forall (constant 'addrsize : Int), 'addrsize in {32, 64}. + (write_kind, bits('addrsize), bit) -> bool effect {wmvt} val __excl_res = { ocaml: "Platform.excl_res", c: "platform_excl_res", _: "excl_result" } : unit -> bool effect {exmem} |
