diff options
| author | Prashanth Mundkur <prashanth.mundkur@gmail.com> | 2019-06-24 16:55:18 -0700 |
|---|---|---|
| committer | Prashanth Mundkur <prashanth.mundkur@gmail.com> | 2019-06-24 18:11:18 -0700 |
| commit | bbb65b3c3422d02989015a6135cf36107f10ad95 (patch) | |
| tree | 98f7f7bc49e5a9779428eb6a38727e8913bb3b7b /handwritten_support | |
| parent | 295175dd4d510cb416bdc4ef17c2ca96d84ed04e (diff) | |
| download | sail-riscv-bbb65b3c3422d02989015a6135cf36107f10ad95.zip sail-riscv-bbb65b3c3422d02989015a6135cf36107f10ad95.tar.gz sail-riscv-bbb65b3c3422d02989015a6135cf36107f10ad95.tar.bz2 | |
Add PMP checks to physical memory accesses.
- unify AccessType and ReadType since they were essentially redundant,
making it easier to implement PMP checks for ReadWrite/atomic accesses.
- add command line options to enable PMP in the platform
- also fix the matching for the case when all entries are off
Diffstat (limited to 'handwritten_support')
| -rw-r--r-- | handwritten_support/riscv_extras.lem | 4 | ||||
| -rw-r--r-- | handwritten_support/riscv_extras_sequential.lem | 4 |
2 files changed, 8 insertions, 0 deletions
diff --git a/handwritten_support/riscv_extras.lem b/handwritten_support/riscv_extras.lem index 66b5d94..da6106d 100644 --- a/handwritten_support/riscv_extras.lem +++ b/handwritten_support/riscv_extras.lem @@ -111,6 +111,10 @@ val plat_enable_misaligned_access : unit -> bool let plat_enable_misaligned_access () = false declare ocaml target_rep function plat_enable_misaligned_access = `Platform.enable_misaligned_access` +val plat_enable_pmp : unit -> bool +let plat_enable_pmp () = false +declare ocaml target_rep function plat_enable_pmp = `Platform.enable_pmp` + val plat_mtval_has_illegal_inst_bits : unit -> bool let plat_mtval_has_illegal_inst_bits () = false declare ocaml target_rep function plat_mtval_has_illegal_inst_bits = `Platform.mtval_has_illegal_inst_bits` diff --git a/handwritten_support/riscv_extras_sequential.lem b/handwritten_support/riscv_extras_sequential.lem index 604911a..7715614 100644 --- a/handwritten_support/riscv_extras_sequential.lem +++ b/handwritten_support/riscv_extras_sequential.lem @@ -107,6 +107,10 @@ val plat_enable_misaligned_access : unit -> bool let plat_enable_misaligned_access () = false declare ocaml target_rep function plat_enable_misaligned_access = `Platform.enable_misaligned_access` +val plat_enable_pmp : unit -> bool +let plat_enable_pmp () = false +declare ocaml target_rep function plat_enable_pmp = `Platform.enable_pmp` + val plat_mtval_has_illegal_inst_bits : unit -> bool let plat_mtval_has_illegal_inst_bits () = false declare ocaml target_rep function plat_mtval_has_illegal_inst_bits = `Platform.mtval_has_illegal_inst_bits` |