diff options
| author | Prashanth Mundkur <prashanth.mundkur@gmail.com> | 2019-04-01 09:07:15 -0700 |
|---|---|---|
| committer | Prashanth Mundkur <prashanth.mundkur@gmail.com> | 2019-04-01 09:07:15 -0700 |
| commit | 9f30ffdb88b744c09370829ef73d1f293b62f76d (patch) | |
| tree | 801b5bec67dbeb3fb818e9c7c2d22cc1277b1ed9 /handwritten_support/riscv_extras.lem | |
| parent | 483e1e4044b5f3e35da5b6102c39f0534483ba36 (diff) | |
| download | sail-riscv-9f30ffdb88b744c09370829ef73d1f293b62f76d.zip sail-riscv-9f30ffdb88b744c09370829ef73d1f293b62f76d.tar.gz sail-riscv-9f30ffdb88b744c09370829ef73d1f293b62f76d.tar.bz2 | |
Add missed lem definitions for sys misa/rvcflags.
Diffstat (limited to 'handwritten_support/riscv_extras.lem')
| -rw-r--r-- | handwritten_support/riscv_extras.lem | 8 |
1 files changed, 8 insertions, 0 deletions
diff --git a/handwritten_support/riscv_extras.lem b/handwritten_support/riscv_extras.lem index ed572be..738c9c6 100644 --- a/handwritten_support/riscv_extras.lem +++ b/handwritten_support/riscv_extras.lem @@ -71,6 +71,14 @@ let speculate_conditional_success () = excl_result () let match_reservation _ = true let cancel_reservation () = () +val sys_enable_writable_misa : unit -> bool +let sys_enable_writable_misa () = true +declare ocaml target_rep function sys_enable_writable_misa = `Platform.enable_writable_misa` + +val sys_enable_rvc : unit -> bool +let sys_enable_rvc () = true +declare ocaml target_rep function sys_enable_rvc = `Platform.enable_rvc` + val plat_ram_base : forall 'a. Size 'a => unit -> bitvector 'a let plat_ram_base () = wordFromInteger 0 declare ocaml target_rep function plat_ram_base = `Platform.dram_base` |