diff options
| author | Jon French <jf451@cam.ac.uk> | 2019-03-12 12:07:33 +0000 |
|---|---|---|
| committer | Jon French <jf451@cam.ac.uk> | 2019-03-12 14:02:19 +0000 |
| commit | 68a69d4ea5357c698da1f007fce6215c6e58e1f7 (patch) | |
| tree | 5e31ed5fad64218cbf1b1ba27a220b436e99fd8d /model/riscv_sys_control.sail | |
| parent | eab254dedc3f72d5ab1b6bbcae69cfebf15988dc (diff) | |
| download | sail-riscv-68a69d4ea5357c698da1f007fce6215c6e58e1f7.zip sail-riscv-68a69d4ea5357c698da1f007fce6215c6e58e1f7.tar.gz sail-riscv-68a69d4ea5357c698da1f007fce6215c6e58e1f7.tar.bz2 | |
riscv_platform.sail: use externs for platform values even in interpreter
Diffstat (limited to 'model/riscv_sys_control.sail')
| -rw-r--r-- | model/riscv_sys_control.sail | 10 |
1 files changed, 4 insertions, 6 deletions
diff --git a/model/riscv_sys_control.sail b/model/riscv_sys_control.sail index 3bdaadd..df84733 100644 --- a/model/riscv_sys_control.sail +++ b/model/riscv_sys_control.sail @@ -99,13 +99,11 @@ function check_CSR(csr : csreg, p : Privilege, isWrite : bool) -> bool = * where cancellation can be performed. */ -val speculate_conditional = {ocaml: "Platform.speculate_conditional", c: "speculate_conditional", lem: "speculate_conditional_success"} : unit -> bool effect {exmem} +val speculate_conditional = {ocaml: "Platform.speculate_conditional", interpreter: "excl_res", c: "speculate_conditional", lem: "speculate_conditional_success"} : unit -> bool effect {exmem} -val load_reservation = {ocaml: "Platform.load_reservation", c: "load_reservation", lem: "load_reservation"} : xlenbits -> unit - -val match_reservation = {ocaml: "Platform.match_reservation", lem: "match_reservation", c: "match_reservation"} : xlenbits -> bool - -val cancel_reservation = {ocaml: "Platform.cancel_reservation", c: "cancel_reservation", lem: "cancel_reservation"} : unit -> unit +val load_reservation = {ocaml: "Platform.load_reservation", interpreter: "Platform.load_reservation", c: "load_reservation", lem: "load_reservation"} : xlenbits -> unit +val match_reservation = {ocaml: "Platform.match_reservation", interpreter: "Platform.match_reservation", lem: "match_reservation", c: "match_reservation"} : xlenbits -> bool +val cancel_reservation = {ocaml: "Platform.cancel_reservation", interpreter: "Platform.cancel_reservation", c: "cancel_reservation", lem: "cancel_reservation"} : unit -> unit /* Exception delegation: given an exception and the privilege at which * it occured, returns the privilege at which it should be handled. |