aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
-rw-r--r--c_emulator/riscv_platform.c15
-rw-r--r--c_emulator/riscv_platform.h4
-rw-r--r--c_emulator/riscv_platform_impl.c4
-rw-r--r--c_emulator/riscv_platform_impl.h4
-rw-r--r--c_emulator/riscv_sim.c27
-rw-r--r--handwritten_support/riscv_extras.lem4
-rw-r--r--handwritten_support/riscv_extras_sequential.lem4
-rw-r--r--model/riscv_csr_map.sail60
-rw-r--r--model/riscv_insts_zicsr.sail59
-rw-r--r--model/riscv_mem.sail4
-rw-r--r--model/riscv_platform.sail6
-rw-r--r--model/riscv_pmp_control.sail138
-rw-r--r--model/riscv_pmp_regs.sail186
-rw-r--r--model/riscv_sys_control.sail32
-rw-r--r--model/riscv_sys_regs.sail7
-rw-r--r--ocaml_emulator/platform.ml9
-rw-r--r--ocaml_emulator/riscv_ocaml_sim.ml9
17 files changed, 275 insertions, 297 deletions
diff --git a/c_emulator/riscv_platform.c b/c_emulator/riscv_platform.c
index fbd63fa..253da35 100644
--- a/c_emulator/riscv_platform.c
+++ b/c_emulator/riscv_platform.c
@@ -47,6 +47,16 @@ bool sys_enable_vext(unit u)
return rv_enable_vext;
}
+uint64_t sys_pmp_count(unit u)
+{
+ return rv_pmp_count;
+}
+
+uint64_t sys_pmp_grain(unit u)
+{
+ return rv_pmp_grain;
+}
+
bool sys_enable_writable_misa(unit u)
{
return rv_enable_writable_misa;
@@ -67,11 +77,6 @@ bool plat_mtval_has_illegal_inst_bits(unit u)
return rv_mtval_has_illegal_inst_bits;
}
-bool plat_enable_pmp(unit u)
-{
- return rv_enable_pmp;
-}
-
mach_bits plat_ram_base(unit u)
{
return rv_ram_base;
diff --git a/c_emulator/riscv_platform.h b/c_emulator/riscv_platform.h
index 4b6541f..38fac2f 100644
--- a/c_emulator/riscv_platform.h
+++ b/c_emulator/riscv_platform.h
@@ -9,10 +9,12 @@ bool sys_enable_writable_misa(unit);
bool sys_enable_writable_fiom(unit);
bool sys_enable_vext(unit);
+uint64_t sys_pmp_count(unit);
+uint64_t sys_pmp_grain(unit);
+
bool plat_enable_dirty_update(unit);
bool plat_enable_misaligned_access(unit);
bool plat_mtval_has_illegal_inst_bits(unit);
-bool plat_enable_pmp(unit);
mach_bits plat_ram_base(unit);
mach_bits plat_ram_size(unit);
diff --git a/c_emulator/riscv_platform_impl.c b/c_emulator/riscv_platform_impl.c
index 15ff8ad..c2ae256 100644
--- a/c_emulator/riscv_platform_impl.c
+++ b/c_emulator/riscv_platform_impl.c
@@ -3,7 +3,9 @@
#include <stdio.h>
/* Settings of the platform implementation, with common defaults. */
-bool rv_enable_pmp = false;
+uint64_t rv_pmp_count = 0;
+uint64_t rv_pmp_grain = 0;
+
bool rv_enable_zfinx = false;
bool rv_enable_rvc = true;
bool rv_enable_next = false;
diff --git a/c_emulator/riscv_platform_impl.h b/c_emulator/riscv_platform_impl.h
index e5c562a..e3e4a96 100644
--- a/c_emulator/riscv_platform_impl.h
+++ b/c_emulator/riscv_platform_impl.h
@@ -8,7 +8,9 @@
#define DEFAULT_RSTVEC 0x00001000
-extern bool rv_enable_pmp;
+extern uint64_t rv_pmp_count;
+extern uint64_t rv_pmp_grain;
+
extern bool rv_enable_zfinx;
extern bool rv_enable_rvc;
extern bool rv_enable_next;
diff --git a/c_emulator/riscv_sim.c b/c_emulator/riscv_sim.c
index 13d1653..f3c6343 100644
--- a/c_emulator/riscv_sim.c
+++ b/c_emulator/riscv_sim.c
@@ -51,6 +51,8 @@ const char *RV32ISA = "RV32IMAC";
#define OPT_TRACE_OUTPUT 1000
#define OPT_ENABLE_WRITABLE_FIOM 1001
+#define OPT_PMP_COUNT 1002
+#define OPT_PMP_GRAIN 1003
static bool do_dump_dts = false;
static bool do_show_times = false;
@@ -119,7 +121,8 @@ char *sailcov_file = NULL;
static struct option options[] = {
{"enable-dirty-update", no_argument, 0, 'd' },
{"enable-misaligned", no_argument, 0, 'm' },
- {"enable-pmp", no_argument, 0, 'P' },
+ {"pmp-count", required_argument, 0, OPT_PMP_COUNT },
+ {"pmp-grain", required_argument, 0, OPT_PMP_GRAIN },
{"enable-next", no_argument, 0, 'N' },
{"ram-size", required_argument, 0, 'z' },
{"disable-compressed", no_argument, 0, 'C' },
@@ -236,6 +239,8 @@ static int process_args(int argc, char **argv)
{
int c;
uint64_t ram_size = 0;
+ uint64_t pmp_count = 0;
+ uint64_t pmp_grain = 0;
while (true) {
c = getopt_long(argc, argv,
"a"
@@ -281,9 +286,23 @@ static int process_args(int argc, char **argv)
fprintf(stderr, "enabling misaligned access.\n");
rv_enable_misaligned = true;
break;
- case 'P':
- fprintf(stderr, "enabling PMP support.\n");
- rv_enable_pmp = true;
+ case OPT_PMP_COUNT:
+ pmp_count = atol(optarg);
+ fprintf(stderr, "PMP count: %lld\n", pmp_count);
+ if (pmp_count != 0 && pmp_count != 16 && pmp_count != 64) {
+ fprintf(stderr, "invalid PMP count: must be 0, 16 or 64");
+ exit(1);
+ }
+ rv_pmp_count = pmp_count;
+ break;
+ case OPT_PMP_GRAIN:
+ pmp_grain = atol(optarg);
+ fprintf(stderr, "PMP grain: %lld\n", pmp_grain);
+ if (pmp_grain >= 64) {
+ fprintf(stderr, "invalid PMP grain: must less than 64");
+ exit(1);
+ }
+ rv_pmp_grain = pmp_grain;
break;
case 'C':
fprintf(stderr, "disabling RVC compressed instructions.\n");
diff --git a/handwritten_support/riscv_extras.lem b/handwritten_support/riscv_extras.lem
index bc04c2d..27e8ee5 100644
--- a/handwritten_support/riscv_extras.lem
+++ b/handwritten_support/riscv_extras.lem
@@ -201,10 +201,6 @@ 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 102d082..d113908 100644
--- a/handwritten_support/riscv_extras_sequential.lem
+++ b/handwritten_support/riscv_extras_sequential.lem
@@ -189,10 +189,6 @@ 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/model/riscv_csr_map.sail b/model/riscv_csr_map.sail
index da68556..dcc8651 100644
--- a/model/riscv_csr_map.sail
+++ b/model/riscv_csr_map.sail
@@ -138,6 +138,18 @@ mapping clause csr_name_map = 0x3A0 <-> "pmpcfg0"
mapping clause csr_name_map = 0x3A1 <-> "pmpcfg1"
mapping clause csr_name_map = 0x3A2 <-> "pmpcfg2"
mapping clause csr_name_map = 0x3A3 <-> "pmpcfg3"
+mapping clause csr_name_map = 0x3A4 <-> "pmpcfg4"
+mapping clause csr_name_map = 0x3A5 <-> "pmpcfg5"
+mapping clause csr_name_map = 0x3A6 <-> "pmpcfg6"
+mapping clause csr_name_map = 0x3A7 <-> "pmpcfg7"
+mapping clause csr_name_map = 0x3A8 <-> "pmpcfg8"
+mapping clause csr_name_map = 0x3A9 <-> "pmpcfg9"
+mapping clause csr_name_map = 0x3AA <-> "pmpcfg10"
+mapping clause csr_name_map = 0x3AB <-> "pmpcfg11"
+mapping clause csr_name_map = 0x3AC <-> "pmpcfg12"
+mapping clause csr_name_map = 0x3AD <-> "pmpcfg13"
+mapping clause csr_name_map = 0x3AE <-> "pmpcfg14"
+mapping clause csr_name_map = 0x3AF <-> "pmpcfg15"
mapping clause csr_name_map = 0x3B0 <-> "pmpaddr0"
mapping clause csr_name_map = 0x3B1 <-> "pmpaddr1"
mapping clause csr_name_map = 0x3B2 <-> "pmpaddr2"
@@ -154,6 +166,54 @@ mapping clause csr_name_map = 0x3BC <-> "pmpaddr12"
mapping clause csr_name_map = 0x3BD <-> "pmpaddr13"
mapping clause csr_name_map = 0x3BE <-> "pmpaddr14"
mapping clause csr_name_map = 0x3BF <-> "pmpaddr15"
+mapping clause csr_name_map = 0x3C0 <-> "pmpaddr16"
+mapping clause csr_name_map = 0x3C1 <-> "pmpaddr17"
+mapping clause csr_name_map = 0x3C2 <-> "pmpaddr18"
+mapping clause csr_name_map = 0x3C3 <-> "pmpaddr19"
+mapping clause csr_name_map = 0x3C4 <-> "pmpaddr20"
+mapping clause csr_name_map = 0x3C5 <-> "pmpaddr21"
+mapping clause csr_name_map = 0x3C6 <-> "pmpaddr22"
+mapping clause csr_name_map = 0x3C7 <-> "pmpaddr23"
+mapping clause csr_name_map = 0x3C8 <-> "pmpaddr24"
+mapping clause csr_name_map = 0x3C9 <-> "pmpaddr25"
+mapping clause csr_name_map = 0x3CA <-> "pmpaddr26"
+mapping clause csr_name_map = 0x3CB <-> "pmpaddr27"
+mapping clause csr_name_map = 0x3CC <-> "pmpaddr28"
+mapping clause csr_name_map = 0x3CD <-> "pmpaddr29"
+mapping clause csr_name_map = 0x3CE <-> "pmpaddr30"
+mapping clause csr_name_map = 0x3CF <-> "pmpaddr31"
+mapping clause csr_name_map = 0x3D0 <-> "pmpaddr32"
+mapping clause csr_name_map = 0x3D1 <-> "pmpaddr33"
+mapping clause csr_name_map = 0x3D2 <-> "pmpaddr34"
+mapping clause csr_name_map = 0x3D3 <-> "pmpaddr35"
+mapping clause csr_name_map = 0x3D4 <-> "pmpaddr36"
+mapping clause csr_name_map = 0x3D5 <-> "pmpaddr37"
+mapping clause csr_name_map = 0x3D6 <-> "pmpaddr38"
+mapping clause csr_name_map = 0x3D7 <-> "pmpaddr39"
+mapping clause csr_name_map = 0x3D8 <-> "pmpaddr40"
+mapping clause csr_name_map = 0x3D9 <-> "pmpaddr41"
+mapping clause csr_name_map = 0x3DA <-> "pmpaddr42"
+mapping clause csr_name_map = 0x3DB <-> "pmpaddr43"
+mapping clause csr_name_map = 0x3DC <-> "pmpaddr44"
+mapping clause csr_name_map = 0x3DD <-> "pmpaddr45"
+mapping clause csr_name_map = 0x3DE <-> "pmpaddr46"
+mapping clause csr_name_map = 0x3DF <-> "pmpaddr47"
+mapping clause csr_name_map = 0x3E0 <-> "pmpaddr48"
+mapping clause csr_name_map = 0x3E1 <-> "pmpaddr49"
+mapping clause csr_name_map = 0x3E2 <-> "pmpaddr50"
+mapping clause csr_name_map = 0x3E3 <-> "pmpaddr51"
+mapping clause csr_name_map = 0x3E4 <-> "pmpaddr52"
+mapping clause csr_name_map = 0x3E5 <-> "pmpaddr53"
+mapping clause csr_name_map = 0x3E6 <-> "pmpaddr54"
+mapping clause csr_name_map = 0x3E7 <-> "pmpaddr55"
+mapping clause csr_name_map = 0x3E8 <-> "pmpaddr56"
+mapping clause csr_name_map = 0x3E9 <-> "pmpaddr57"
+mapping clause csr_name_map = 0x3EA <-> "pmpaddr58"
+mapping clause csr_name_map = 0x3EB <-> "pmpaddr59"
+mapping clause csr_name_map = 0x3EC <-> "pmpaddr60"
+mapping clause csr_name_map = 0x3ED <-> "pmpaddr61"
+mapping clause csr_name_map = 0x3EE <-> "pmpaddr62"
+mapping clause csr_name_map = 0x3EF <-> "pmpaddr63"
/* machine counters/timers */
mapping clause csr_name_map = 0xB00 <-> "mcycle"
mapping clause csr_name_map = 0xB02 <-> "minstret"
diff --git a/model/riscv_insts_zicsr.sail b/model/riscv_insts_zicsr.sail
index 4be297a..6aa512e 100644
--- a/model/riscv_insts_zicsr.sail
+++ b/model/riscv_insts_zicsr.sail
@@ -109,27 +109,13 @@ function readCSR csr : csreg -> xlenbits = {
(0x343, _) => mtval,
(0x344, _) => mip.bits,
- (0x3A0, _) => pmpReadCfgReg(0), // pmpcfg0
- (0x3A1, 32) => pmpReadCfgReg(1), // pmpcfg1
- (0x3A2, _) => pmpReadCfgReg(2), // pmpcfg2
- (0x3A3, 32) => pmpReadCfgReg(3), // pmpcfg3
-
- (0x3B0, _) => pmpaddr0,
- (0x3B1, _) => pmpaddr1,
- (0x3B2, _) => pmpaddr2,
- (0x3B3, _) => pmpaddr3,
- (0x3B4, _) => pmpaddr4,
- (0x3B5, _) => pmpaddr5,
- (0x3B6, _) => pmpaddr6,
- (0x3B7, _) => pmpaddr7,
- (0x3B8, _) => pmpaddr8,
- (0x3B9, _) => pmpaddr9,
- (0x3BA, _) => pmpaddr10,
- (0x3BB, _) => pmpaddr11,
- (0x3BC, _) => pmpaddr12,
- (0x3BD, _) => pmpaddr13,
- (0x3BE, _) => pmpaddr14,
- (0x3BF, _) => pmpaddr15,
+ // pmpcfgN
+ (0x3A @ idx : bits(4), _) if idx[0] == bitzero | sizeof(xlen) == 32 => pmpReadCfgReg(unsigned(idx)),
+ // pmpaddrN. Unfortunately the PMP index does not nicely align with the CSR index bits.
+ (0x3B @ idx : bits(4), _) => pmpReadAddrReg(unsigned(0b00 @ idx)),
+ (0x3C @ idx : bits(4), _) => pmpReadAddrReg(unsigned(0b01 @ idx)),
+ (0x3D @ idx : bits(4), _) => pmpReadAddrReg(unsigned(0b10 @ idx)),
+ (0x3E @ idx : bits(4), _) => pmpReadAddrReg(unsigned(0b11 @ idx)),
/* machine mode counters */
(0xB00, _) => mcycle[(sizeof(xlen) - 1) .. 0],
@@ -209,28 +195,17 @@ function writeCSR (csr : csreg, value : xlenbits) -> unit = {
(0x343, _) => { mtval = value; Some(mtval) },
(0x344, _) => { mip = legalize_mip(mip, value); Some(mip.bits) },
- // Note: Some(value) returned below is not the legalized value due to locked entries
- (0x3A0, _) => { pmpWriteCfgReg(0, value); Some(pmpReadCfgReg(0)) }, // pmpcfg0
- (0x3A1, 32) => { pmpWriteCfgReg(1, value); Some(pmpReadCfgReg(1)) }, // pmpcfg1
- (0x3A2, _) => { pmpWriteCfgReg(2, value); Some(pmpReadCfgReg(2)) }, // pmpcfg2
- (0x3A3, 32) => { pmpWriteCfgReg(3, value); Some(pmpReadCfgReg(3)) }, // pmpcfg3
+ // pmpcfgN
+ (0x3A @ idx : bits(4), _) if idx[0] == bitzero | sizeof(xlen) == 32 => {
+ let idx = unsigned(idx);
+ pmpWriteCfgReg(idx, value); Some(pmpReadCfgReg(idx))
+ },
- (0x3B0, _) => { pmpaddr0 = pmpWriteAddr(pmpLocked(pmp0cfg), pmpTORLocked(pmp1cfg), pmpaddr0, value); Some(pmpaddr0) },
- (0x3B1, _) => { pmpaddr1 = pmpWriteAddr(pmpLocked(pmp1cfg), pmpTORLocked(pmp2cfg), pmpaddr1, value); Some(pmpaddr1) },
- (0x3B2, _) => { pmpaddr2 = pmpWriteAddr(pmpLocked(pmp2cfg), pmpTORLocked(pmp3cfg), pmpaddr2, value); Some(pmpaddr2) },
- (0x3B3, _) => { pmpaddr3 = pmpWriteAddr(pmpLocked(pmp3cfg), pmpTORLocked(pmp4cfg), pmpaddr3, value); Some(pmpaddr3) },
- (0x3B4, _) => { pmpaddr4 = pmpWriteAddr(pmpLocked(pmp4cfg), pmpTORLocked(pmp5cfg), pmpaddr4, value); Some(pmpaddr4) },
- (0x3B5, _) => { pmpaddr5 = pmpWriteAddr(pmpLocked(pmp5cfg), pmpTORLocked(pmp6cfg), pmpaddr5, value); Some(pmpaddr5) },
- (0x3B6, _) => { pmpaddr6 = pmpWriteAddr(pmpLocked(pmp6cfg), pmpTORLocked(pmp7cfg), pmpaddr6, value); Some(pmpaddr6) },
- (0x3B7, _) => { pmpaddr7 = pmpWriteAddr(pmpLocked(pmp7cfg), pmpTORLocked(pmp8cfg), pmpaddr7, value); Some(pmpaddr7) },
- (0x3B8, _) => { pmpaddr8 = pmpWriteAddr(pmpLocked(pmp8cfg), pmpTORLocked(pmp9cfg), pmpaddr8, value); Some(pmpaddr8) },
- (0x3B9, _) => { pmpaddr9 = pmpWriteAddr(pmpLocked(pmp9cfg), pmpTORLocked(pmp10cfg), pmpaddr9, value); Some(pmpaddr9) },
- (0x3BA, _) => { pmpaddr10 = pmpWriteAddr(pmpLocked(pmp10cfg), pmpTORLocked(pmp11cfg), pmpaddr10, value); Some(pmpaddr10) },
- (0x3BB, _) => { pmpaddr11 = pmpWriteAddr(pmpLocked(pmp11cfg), pmpTORLocked(pmp12cfg), pmpaddr11, value); Some(pmpaddr11) },
- (0x3BC, _) => { pmpaddr12 = pmpWriteAddr(pmpLocked(pmp12cfg), pmpTORLocked(pmp13cfg), pmpaddr12, value); Some(pmpaddr12) },
- (0x3BD, _) => { pmpaddr13 = pmpWriteAddr(pmpLocked(pmp13cfg), pmpTORLocked(pmp14cfg), pmpaddr13, value); Some(pmpaddr13) },
- (0x3BE, _) => { pmpaddr14 = pmpWriteAddr(pmpLocked(pmp14cfg), pmpTORLocked(pmp15cfg), pmpaddr14, value); Some(pmpaddr14) },
- (0x3BF, _) => { pmpaddr15 = pmpWriteAddr(pmpLocked(pmp15cfg), false, pmpaddr15, value); Some(pmpaddr15) },
+ // pmpaddrN. Unfortunately the PMP index does not nicely align with the CSR index bits.
+ (0x3B @ idx : bits(4), _) => { let idx = unsigned(0b00 @ idx); pmpWriteAddrReg(idx, value); Some(pmpReadAddrReg(idx)) },
+ (0x3C @ idx : bits(4), _) => { let idx = unsigned(0b01 @ idx); pmpWriteAddrReg(idx, value); Some(pmpReadAddrReg(idx)) },
+ (0x3D @ idx : bits(4), _) => { let idx = unsigned(0b10 @ idx); pmpWriteAddrReg(idx, value); Some(pmpReadAddrReg(idx)) },
+ (0x3E @ idx : bits(4), _) => { let idx = unsigned(0b11 @ idx); pmpWriteAddrReg(idx, value); Some(pmpReadAddrReg(idx)) },
/* machine mode counters */
(0xB00, _) => { mcycle[(sizeof(xlen) - 1) .. 0] = value; Some(value) },
diff --git a/model/riscv_mem.sail b/model/riscv_mem.sail
index 2df6192..5224938 100644
--- a/model/riscv_mem.sail
+++ b/model/riscv_mem.sail
@@ -144,7 +144,7 @@ function checked_mem_read forall 'n, 0 < 'n <= max_mem_access . (t : AccessType(
/* PMP checks if enabled */
function pmp_mem_read forall 'n, 0 < 'n <= max_mem_access . (t : AccessType(ext_access_type), p : Privilege, paddr : xlenbits, width : atom('n), aq : bool, rl : bool, res: bool, meta : bool) -> MemoryOpResult((bits(8 * 'n), mem_meta)) =
- if not(plat_enable_pmp())
+ if sys_pmp_count() == 0
then checked_mem_read(t, paddr, width, aq, rl, res, meta)
else {
match pmpCheck(paddr, width, t, p) {
@@ -272,7 +272,7 @@ function checked_mem_write forall 'n, 0 < 'n <= max_mem_access . (wk : write_kin
/* PMP checks if enabled */
function pmp_mem_write forall 'n, 0 < 'n <= max_mem_access . (wk: write_kind, paddr : xlenbits, width : atom('n), data: bits(8 * 'n), typ: AccessType(ext_access_type), priv: Privilege, meta: mem_meta) -> MemoryOpResult(bool) =
- if not(plat_enable_pmp())
+ if sys_pmp_count() == 0
then checked_mem_write(wk, paddr, width, data, meta)
else {
match pmpCheck(paddr, width, typ, priv) {
diff --git a/model/riscv_platform.sail b/model/riscv_platform.sail
index f9637fe..15b0d4c 100644
--- a/model/riscv_platform.sail
+++ b/model/riscv_platform.sail
@@ -92,12 +92,6 @@ val elf_entry = {
val plat_ram_base = {c: "plat_ram_base", ocaml: "Platform.dram_base", interpreter: "Platform.dram_base", lem: "plat_ram_base"} : unit -> xlenbits
val plat_ram_size = {c: "plat_ram_size", ocaml: "Platform.dram_size", interpreter: "Platform.dram_size", lem: "plat_ram_size"} : unit -> xlenbits
-/* whether the platform supports PMP configurations */
-val plat_enable_pmp = {ocaml: "Platform.enable_pmp",
- interpreter: "Platform.enable_pmp",
- c: "plat_enable_pmp",
- lem: "plat_enable_pmp"} : unit -> bool
-
/* whether the MMU should update dirty bits in PTEs */
val plat_enable_dirty_update = {ocaml: "Platform.enable_dirty_update",
interpreter: "Platform.enable_dirty_update",
diff --git a/model/riscv_pmp_control.sail b/model/riscv_pmp_control.sail
index e95dfa1..b2da8d8 100644
--- a/model/riscv_pmp_control.sail
+++ b/model/riscv_pmp_control.sail
@@ -70,7 +70,6 @@
/* address ranges */
-// TODO: handle PMP grain > 4 (i.e. G > 0).
// TODO: handle the 34-bit paddr32 on RV32
/* [min, max) of the matching range. */
@@ -80,14 +79,21 @@ function pmpAddrRange(cfg: Pmpcfg_ent, pmpaddr: xlenbits, prev_pmpaddr: xlenbits
match pmpAddrMatchType_of_bits(cfg[A]) {
OFF => None(),
TOR => { Some ((prev_pmpaddr << 2, pmpaddr << 2)) },
- NA4 => { // TODO: I find the spec unclear for entries marked NA4 and G = 1.
- // (for G >= 2, it is the same as NAPOT). In particular, it affects
- // whether pmpaddr[0] is always read as 0.
+ NA4 => {
+ // NA4 is not selectable when the PMP grain G >= 1. See pmpWriteCfg().
+ assert(sys_pmp_grain() < 1, "NA4 cannot be selected when PMP grain G >= 1.");
let lo = pmpaddr << 2;
Some((lo, lo + 4))
},
- NAPOT => { let mask = pmpaddr ^ (pmpaddr + 1); // generate 1s in signifying bits
+ NAPOT => {
+ // Example pmpaddr: 0b00010101111
+ // ^--- last 0 dictates region size & alignment
+ let mask = pmpaddr ^ (pmpaddr + 1);
+ // pmpaddr + 1: 0b00010110000
+ // mask: 0b00000011111
+ // ~mask: 0b11111100000
let lo = pmpaddr & (~ (mask));
+ // mask + 1: 0b00000100000
let len = mask + 1;
Some((lo << 2, (lo + len) << 2))
}
@@ -152,104 +158,38 @@ function pmpMatchEntry(addr: xlenbits, width: xlenbits, acc: AccessType(ext_acce
/* priority checks */
+function accessToFault(acc : AccessType(ext_access_type)) -> ExceptionType =
+ match acc {
+ Read(_) => E_Load_Access_Fault(),
+ Write(_) => E_SAMO_Access_Fault(),
+ ReadWrite(_) => E_SAMO_Access_Fault(),
+ Execute() => E_Fetch_Access_Fault(),
+ }
+
function pmpCheck forall 'n, 'n > 0. (addr: xlenbits, width: atom('n), acc: AccessType(ext_access_type), priv: Privilege)
-> option(ExceptionType) = {
let width : xlenbits = to_bits(sizeof(xlen), width);
- let check : bool =
- match pmpMatchEntry(addr, width, acc, priv, pmp0cfg, pmpaddr0, zeros()) {
- PMP_Success => true,
- PMP_Fail => false,
- PMP_Continue =>
- match pmpMatchEntry(addr, width, acc, priv, pmp1cfg, pmpaddr1, pmpaddr0) {
- PMP_Success => true,
- PMP_Fail => false,
- PMP_Continue =>
- match pmpMatchEntry(addr, width, acc, priv, pmp2cfg, pmpaddr2, pmpaddr1) {
- PMP_Success => true,
- PMP_Fail => false,
- PMP_Continue =>
- match pmpMatchEntry(addr, width, acc, priv, pmp3cfg, pmpaddr3, pmpaddr2) {
- PMP_Success => true,
- PMP_Fail => false,
- PMP_Continue =>
- match pmpMatchEntry(addr, width, acc, priv, pmp4cfg, pmpaddr4, pmpaddr3) {
- PMP_Success => true,
- PMP_Fail => false,
- PMP_Continue =>
- match pmpMatchEntry(addr, width, acc, priv, pmp5cfg, pmpaddr5, pmpaddr4) {
- PMP_Success => true,
- PMP_Fail => false,
- PMP_Continue =>
- match pmpMatchEntry(addr, width, acc, priv, pmp6cfg, pmpaddr6, pmpaddr5) {
- PMP_Success => true,
- PMP_Fail => false,
- PMP_Continue =>
- match pmpMatchEntry(addr, width, acc, priv, pmp7cfg, pmpaddr7, pmpaddr6) {
- PMP_Success => true,
- PMP_Fail => false,
- PMP_Continue =>
- match pmpMatchEntry(addr, width, acc, priv, pmp8cfg, pmpaddr8, pmpaddr7) {
- PMP_Success => true,
- PMP_Fail => false,
- PMP_Continue =>
- match pmpMatchEntry(addr, width, acc, priv, pmp9cfg, pmpaddr9, pmpaddr8) {
- PMP_Success => true,
- PMP_Fail => false,
- PMP_Continue =>
- match pmpMatchEntry(addr, width, acc, priv, pmp10cfg, pmpaddr10, pmpaddr9) {
- PMP_Success => true,
- PMP_Fail => false,
- PMP_Continue =>
- match pmpMatchEntry(addr, width, acc, priv, pmp11cfg, pmpaddr11, pmpaddr10) {
- PMP_Success => true,
- PMP_Fail => false,
- PMP_Continue =>
- match pmpMatchEntry(addr, width, acc, priv, pmp12cfg, pmpaddr12, pmpaddr11) {
- PMP_Success => true,
- PMP_Fail => false,
- PMP_Continue =>
- match pmpMatchEntry(addr, width, acc, priv, pmp13cfg, pmpaddr13, pmpaddr12) {
- PMP_Success => true,
- PMP_Fail => false,
- PMP_Continue =>
- match pmpMatchEntry(addr, width, acc, priv, pmp14cfg, pmpaddr14, pmpaddr13) {
- PMP_Success => true,
- PMP_Fail => false,
- PMP_Continue =>
- match pmpMatchEntry(addr, width, acc, priv, pmp15cfg, pmpaddr15, pmpaddr14) {
- PMP_Success => true,
- PMP_Fail => false,
- PMP_Continue => match priv {
- Machine => true,
- _ => false
- }
- }}}}}}}}}}}}}}}};
-
- if check
- then None()
- else match acc {
- Read(_) => Some(E_Load_Access_Fault()),
- Write(_) => Some(E_SAMO_Access_Fault()),
- ReadWrite(_) => Some(E_SAMO_Access_Fault()),
- Execute() => Some(E_Fetch_Access_Fault())
- }
+
+ foreach (i from 0 to 63) {
+ let prev_pmpaddr = (if i > 0 then pmpReadAddrReg(i - 1) else zeros());
+ match pmpMatchEntry(addr, width, acc, priv, pmpcfg_n[i], pmpReadAddrReg(i), prev_pmpaddr) {
+ PMP_Success => { return None(); },
+ PMP_Fail => { return Some(accessToFault(acc)); },
+ PMP_Continue => (),
+ }
+ };
+ if priv == Machine then None() else Some(accessToFault(acc))
}
function init_pmp() -> unit = {
- pmp0cfg = update_A(pmp0cfg, pmpAddrMatchType_to_bits(OFF));
- pmp1cfg = update_A(pmp1cfg, pmpAddrMatchType_to_bits(OFF));
- pmp2cfg = update_A(pmp2cfg, pmpAddrMatchType_to_bits(OFF));
- pmp3cfg = update_A(pmp3cfg, pmpAddrMatchType_to_bits(OFF));
- pmp4cfg = update_A(pmp4cfg, pmpAddrMatchType_to_bits(OFF));
- pmp5cfg = update_A(pmp5cfg, pmpAddrMatchType_to_bits(OFF));
- pmp6cfg = update_A(pmp6cfg, pmpAddrMatchType_to_bits(OFF));
- pmp7cfg = update_A(pmp7cfg, pmpAddrMatchType_to_bits(OFF));
- pmp8cfg = update_A(pmp8cfg, pmpAddrMatchType_to_bits(OFF));
- pmp9cfg = update_A(pmp9cfg, pmpAddrMatchType_to_bits(OFF));
- pmp10cfg = update_A(pmp10cfg, pmpAddrMatchType_to_bits(OFF));
- pmp11cfg = update_A(pmp11cfg, pmpAddrMatchType_to_bits(OFF));
- pmp12cfg = update_A(pmp12cfg, pmpAddrMatchType_to_bits(OFF));
- pmp13cfg = update_A(pmp13cfg, pmpAddrMatchType_to_bits(OFF));
- pmp14cfg = update_A(pmp14cfg, pmpAddrMatchType_to_bits(OFF));
- pmp15cfg = update_A(pmp15cfg, pmpAddrMatchType_to_bits(OFF))
+ assert(
+ sys_pmp_count() == 0 | sys_pmp_count() == 16 | sys_pmp_count() == 64,
+ "sys_pmp_count() must be 0, 16, or 64"
+ );
+
+ foreach (i from 0 to 63) {
+ // On reset the PMP register's A and L bits are set to 0 unless the plaform
+ // mandates a different value.
+ pmpcfg_n[i] = [pmpcfg_n[i] with A = pmpAddrMatchType_to_bits(OFF), L = 0b0];
+ };
}
diff --git a/model/riscv_pmp_regs.sail b/model/riscv_pmp_regs.sail
index 04ab309..5f931af 100644
--- a/model/riscv_pmp_regs.sail
+++ b/model/riscv_pmp_regs.sail
@@ -102,59 +102,52 @@ bitfield Pmpcfg_ent : bits(8) = {
R : 0 /* read */
}
-register pmp0cfg : Pmpcfg_ent
-register pmp1cfg : Pmpcfg_ent
-register pmp2cfg : Pmpcfg_ent
-register pmp3cfg : Pmpcfg_ent
-register pmp4cfg : Pmpcfg_ent
-register pmp5cfg : Pmpcfg_ent
-register pmp6cfg : Pmpcfg_ent
-register pmp7cfg : Pmpcfg_ent
-register pmp8cfg : Pmpcfg_ent
-register pmp9cfg : Pmpcfg_ent
-register pmp10cfg : Pmpcfg_ent
-register pmp11cfg : Pmpcfg_ent
-register pmp12cfg : Pmpcfg_ent
-register pmp13cfg : Pmpcfg_ent
-register pmp14cfg : Pmpcfg_ent
-register pmp15cfg : Pmpcfg_ent
-
-/* PMP address configuration */
-
-register pmpaddr0 : xlenbits
-register pmpaddr1 : xlenbits
-register pmpaddr2 : xlenbits
-register pmpaddr3 : xlenbits
-register pmpaddr4 : xlenbits
-register pmpaddr5 : xlenbits
-register pmpaddr6 : xlenbits
-register pmpaddr7 : xlenbits
-register pmpaddr8 : xlenbits
-register pmpaddr9 : xlenbits
-register pmpaddr10 : xlenbits
-register pmpaddr11 : xlenbits
-register pmpaddr12 : xlenbits
-register pmpaddr13 : xlenbits
-register pmpaddr14 : xlenbits
-register pmpaddr15 : xlenbits
+register pmpcfg_n : vector(64, dec, Pmpcfg_ent)
+register pmpaddr_n : vector(64, dec, xlenbits)
/* Packing and unpacking pmpcfg regs for xlen-width accesses */
-val pmpReadCfgReg : forall 'n, 0 <= 'n < 4 . (atom('n)) -> xlenbits
-function pmpReadCfgReg(n) = {
- if sizeof(xlen) == 32
- then match n {
- 0 => append(pmp3cfg.bits, append(pmp2cfg.bits, append(pmp1cfg.bits, pmp0cfg.bits))),
- 1 => append(pmp7cfg.bits, append(pmp6cfg.bits, append(pmp5cfg.bits, pmp4cfg.bits))),
- 2 => append(pmp11cfg.bits, append(pmp10cfg.bits, append(pmp9cfg.bits, pmp8cfg.bits))),
- 3 => append(pmp15cfg.bits, append(pmp14cfg.bits, append(pmp13cfg.bits, pmp12cfg.bits))),
- _ => internal_error(__FILE__, __LINE__, "Unexpected pmp config reg read")
- }
- else match n { // sizeof(xlen) >= 64
- 0 => append(pmp7cfg.bits, append(pmp6cfg.bits, append(pmp5cfg.bits, append(pmp4cfg.bits, append(pmp3cfg.bits, append(pmp2cfg.bits, append(pmp1cfg.bits, pmp0cfg.bits))))))),
- 2 => append(pmp15cfg.bits, append(pmp14cfg.bits, append(pmp13cfg.bits, append(pmp12cfg.bits, append(pmp11cfg.bits, append(pmp10cfg.bits, append(pmp9cfg.bits, pmp8cfg.bits))))))),
- _ => internal_error(__FILE__, __LINE__, "Unexpected pmp config reg read")
- }
+function pmpReadCfgReg(n : range(0, 15)) -> xlenbits = {
+ if sizeof(xlen) == 32
+ then {
+ pmpcfg_n[n*4 + 3].bits @
+ pmpcfg_n[n*4 + 2].bits @
+ pmpcfg_n[n*4 + 1].bits @
+ pmpcfg_n[n*4 + 0].bits
+ }
+ else {
+ assert(n % 2 == 0, "Unexpected pmp config reg read");
+ pmpcfg_n[n*4 + 7].bits @
+ pmpcfg_n[n*4 + 6].bits @
+ pmpcfg_n[n*4 + 5].bits @
+ pmpcfg_n[n*4 + 4].bits @
+ pmpcfg_n[n*4 + 3].bits @
+ pmpcfg_n[n*4 + 2].bits @
+ pmpcfg_n[n*4 + 1].bits @
+ pmpcfg_n[n*4 + 0].bits
+ }
+}
+
+function pmpReadAddrReg(n : range(0, 63)) -> xlenbits = {
+ let G = sys_pmp_grain();
+ let match_type = pmpcfg_n[n].A();
+ let addr = pmpaddr_n[n];
+
+ match match_type[1] {
+ bitone if G >= 2 => {
+ // [G-2..0] read as all ones to form mask, therefore we need G-1 bits.
+ let mask : xlenbits = zero_extend(ones(min(G - 1, sizeof(xlen))));
+ addr | mask
+ },
+
+ bitzero if G >= 1 => {
+ // [G-1..0] read as all zeros to form mask, therefore we need G bits.
+ let mask : xlenbits = zero_extend(ones(min(G , sizeof(xlen))));
+ addr & ~(mask)
+ },
+
+ _ => addr,
+ }
}
/* Helpers to handle locked entries */
@@ -164,61 +157,54 @@ function pmpLocked(cfg: Pmpcfg_ent) -> bool =
function pmpTORLocked(cfg: Pmpcfg_ent) -> bool =
(cfg[L] == 0b1) & (pmpAddrMatchType_of_bits(cfg[A]) == TOR)
-function pmpWriteCfg(cfg: Pmpcfg_ent, v: bits(8)) -> Pmpcfg_ent =
+function pmpWriteCfg(n: range(0, 63), cfg: Pmpcfg_ent, v: bits(8)) -> Pmpcfg_ent =
if pmpLocked(cfg) then cfg
- else Mk_Pmpcfg_ent(v & 0x9f) // Bits 5 and 6 are zero.
+ else {
+ // Bits 5 and 6 are zero.
+ let cfg = Mk_Pmpcfg_ent(v & 0x9f);
+
+ // "The R, W, and X fields form a collective WARL field for which the combinations with R=0 and W=1 are reserved."
+ // In this implementation if R=0 and W=1 then R, W and X are all set to 0.
+ // This is the least risky option from a security perspective.
+ let cfg = if cfg.W() == 0b1 & cfg.R() == 0b0 then [cfg with X = 0b0, W = 0b0, R = 0b0] else cfg;
+
+ // "When G >= 1, the NA4 mode is not selectable."
+ // In this implementation we set it to OFF if NA4 is selected.
+ // This is the least risky option from a security perspective.
+ let cfg = if sys_pmp_grain() >= 1 & pmpAddrMatchType_of_bits(cfg.A()) == NA4
+ then [cfg with A = pmpAddrMatchType_to_bits(OFF)]
+ else cfg;
+
+ cfg
+ }
-val pmpWriteCfgReg : forall 'n, 0 <= 'n < 4 . (atom('n), xlenbits) -> unit
-function pmpWriteCfgReg(n, v) = {
- if sizeof(xlen) == 32
- then match n {
- 0 => { pmp0cfg = pmpWriteCfg(pmp0cfg, v[7 ..0]);
- pmp1cfg = pmpWriteCfg(pmp1cfg, v[15..8]);
- pmp2cfg = pmpWriteCfg(pmp2cfg, v[23..16]);
- pmp3cfg = pmpWriteCfg(pmp3cfg, v[31..24]);
- },
- 1 => { pmp4cfg = pmpWriteCfg(pmp4cfg, v[7 ..0]);
- pmp5cfg = pmpWriteCfg(pmp5cfg, v[15..8]);
- pmp6cfg = pmpWriteCfg(pmp6cfg, v[23..16]);
- pmp7cfg = pmpWriteCfg(pmp7cfg, v[31..24]);
- },
- 2 => { pmp8cfg = pmpWriteCfg(pmp8cfg, v[7 ..0]);
- pmp9cfg = pmpWriteCfg(pmp9cfg, v[15..8]);
- pmp10cfg = pmpWriteCfg(pmp10cfg, v[23..16]);
- pmp11cfg = pmpWriteCfg(pmp11cfg, v[31..24]);
- },
- 3 => { pmp12cfg = pmpWriteCfg(pmp12cfg, v[7 ..0]);
- pmp13cfg = pmpWriteCfg(pmp13cfg, v[15..8]);
- pmp14cfg = pmpWriteCfg(pmp14cfg, v[23..16]);
- pmp15cfg = pmpWriteCfg(pmp15cfg, v[31..24]);
- },
- _ => internal_error(__FILE__, __LINE__, "Unexpected pmp config reg write")
- }
- else if sizeof(xlen) >= 64
- then match n {
- 0 => { pmp0cfg = pmpWriteCfg(pmp0cfg, v[7 ..0]);
- pmp1cfg = pmpWriteCfg(pmp1cfg, v[15..8]);
- pmp2cfg = pmpWriteCfg(pmp2cfg, v[23..16]);
- pmp3cfg = pmpWriteCfg(pmp3cfg, v[31..24]);
- pmp4cfg = pmpWriteCfg(pmp4cfg, v[39..32]);
- pmp5cfg = pmpWriteCfg(pmp5cfg, v[47..40]);
- pmp6cfg = pmpWriteCfg(pmp6cfg, v[55..48]);
- pmp7cfg = pmpWriteCfg(pmp7cfg, v[63..56])
- },
- 2 => { pmp8cfg = pmpWriteCfg(pmp8cfg, v[7 ..0]);
- pmp9cfg = pmpWriteCfg(pmp9cfg, v[15..8]);
- pmp10cfg = pmpWriteCfg(pmp10cfg, v[23..16]);
- pmp11cfg = pmpWriteCfg(pmp11cfg, v[31..24]);
- pmp12cfg = pmpWriteCfg(pmp12cfg, v[39..32]);
- pmp13cfg = pmpWriteCfg(pmp13cfg, v[47..40]);
- pmp14cfg = pmpWriteCfg(pmp14cfg, v[55..48]);
- pmp15cfg = pmpWriteCfg(pmp15cfg, v[63..56])
- },
- _ => internal_error(__FILE__, __LINE__, "Unexpected pmp config reg write")
- }
+function pmpWriteCfgReg(n : range(0, 15), v : xlenbits) -> unit = {
+ if sizeof(xlen) == 32
+ then {
+ foreach (i from 0 to 3) {
+ let idx = n*4 + i;
+ pmpcfg_n[idx] = pmpWriteCfg(idx, pmpcfg_n[idx], v[8*i+7 .. 8*i]);
+ }
+ }
+ else {
+ assert(n % 2 == 0, "Unexpected pmp config reg write");
+ foreach (i from 0 to 7) {
+ let idx = n*4 + i;
+ pmpcfg_n[idx] = pmpWriteCfg(idx, pmpcfg_n[idx], v[8*i+7 .. 8*i]);
+ }
+ }
}
function pmpWriteAddr(locked: bool, tor_locked: bool, reg: xlenbits, v: xlenbits) -> xlenbits =
if sizeof(xlen) == 32
then { if (locked | tor_locked) then reg else v }
else { if (locked | tor_locked) then reg else zero_extend(v[53..0]) }
+
+function pmpWriteAddrReg(n : range(0, 63), v : xlenbits) -> unit = {
+ pmpaddr_n[n] = pmpWriteAddr(
+ pmpLocked(pmpcfg_n[n]),
+ if n + 1 < 64 then pmpTORLocked(pmpcfg_n[n + 1]) else false,
+ pmpaddr_n[n],
+ v,
+ );
+}
diff --git a/model/riscv_sys_control.sail b/model/riscv_sys_control.sail
index 94e8a4c..4dfe365 100644
--- a/model/riscv_sys_control.sail
+++ b/model/riscv_sys_control.sail
@@ -102,29 +102,14 @@ function is_CSR_defined (csr : csreg, p : Privilege) -> bool =
0x343 => p == Machine, // mtval
0x344 => p == Machine, // mip
- 0x3A0 => p == Machine, // pmpcfg0
- 0x3A1 => p == Machine & (sizeof(xlen) == 32), // pmpcfg1
- 0x3A2 => p == Machine, // pmpcfg2
- 0x3A3 => p == Machine & (sizeof(xlen) == 32), // pmpcfg3
-
- 0x3B0 => p == Machine, // pmpaddr0
- 0x3B1 => p == Machine, // pmpaddr1
- 0x3B2 => p == Machine, // pmpaddr2
- 0x3B3 => p == Machine, // pmpaddr3
- 0x3B4 => p == Machine, // pmpaddr4
- 0x3B5 => p == Machine, // pmpaddr5
- 0x3B6 => p == Machine, // pmpaddr6
- 0x3B7 => p == Machine, // pmpaddr7
- 0x3B8 => p == Machine, // pmpaddr8
- 0x3B9 => p == Machine, // pmpaddr9
- 0x3BA => p == Machine, // pmpaddrA
- 0x3BB => p == Machine, // pmpaddrB
- 0x3BC => p == Machine, // pmpaddrC
- 0x3BD => p == Machine, // pmpaddrD
- 0x3BE => p == Machine, // pmpaddrE
- 0x3BF => p == Machine, // pmpaddrF
-
- /* counters */
+ // pmpcfgN
+ 0x3A @ idx : bits(4) => p == Machine & sys_pmp_count() > unsigned(idx) & (idx[0] == bitzero | sizeof(xlen) == 32),
+
+ // pmpaddrN. Unfortunately the PMP index does not nicely align with the CSR index bits.
+ 0x3B @ idx : bits(4) => p == Machine & sys_pmp_count() > unsigned(0b00 @ idx),
+ 0x3C @ idx : bits(4) => p == Machine & sys_pmp_count() > unsigned(0b01 @ idx),
+ 0x3D @ idx : bits(4) => p == Machine & sys_pmp_count() > unsigned(0b10 @ idx),
+ 0x3E @ idx : bits(4) => p == Machine & sys_pmp_count() > unsigned(0b11 @ idx),
0xB00 => p == Machine, // mcycle
0xB02 => p == Machine, // minstret
@@ -623,6 +608,7 @@ function init_sys() -> unit = {
vtype[vsew] = 0b000;
vtype[vlmul] = 0b000;
+ // PMP's L and A fields are set to 0 on reset.
init_pmp();
// log compatibility with spike
diff --git a/model/riscv_sys_regs.sail b/model/riscv_sys_regs.sail
index fac0c97..c98584b 100644
--- a/model/riscv_sys_regs.sail
+++ b/model/riscv_sys_regs.sail
@@ -153,6 +153,13 @@ val sys_enable_next = {c: "sys_enable_next", ocaml: "Platform.enable_next", _: "
/* Whether FIOM bit of menvcfg/senvcfg is enabled. It must be enabled if
supervisor mode is implemented and non-bare addressing modes are supported. */
val sys_enable_writable_fiom = {c: "sys_enable_writable_fiom", ocaml: "Platform.enable_writable_fiom", _: "sys_enable_writable_fiom"} : unit -> bool
+
+/* How many PMP entries are implemented. This must be 0, 16 or 64 (this is checked at runtime). */
+val sys_pmp_count = {c: "sys_pmp_count", ocaml: "Platform.pmp_count", _: "sys_pmp_count"} : unit -> range(0, 64)
+/* G parameter that specifies the PMP grain size. The grain size is 2^(G+2), e.g.
+ G=0 -> 4 bytes, G=10 -> 4096 bytes. */
+val sys_pmp_grain = {c: "sys_pmp_grain", ocaml: "Platform.pmp_grain", _: "sys_pmp_grain"} : unit -> range(0, 63)
+
/* whether misa.v was enabled at boot */
val sys_enable_vext = {c: "sys_enable_vext", ocaml: "Platform.enable_vext", _: "sys_enable_vext"} : unit -> bool
diff --git a/ocaml_emulator/platform.ml b/ocaml_emulator/platform.ml
index e4dbfeb..a8bde44 100644
--- a/ocaml_emulator/platform.ml
+++ b/ocaml_emulator/platform.ml
@@ -10,9 +10,13 @@ let config_enable_writable_misa = ref true
let config_enable_dirty_update = ref false
let config_enable_misaligned_access = ref false
let config_mtval_has_illegal_inst_bits = ref false
-let config_enable_pmp = ref false
let config_enable_writable_fiom = ref true
let config_enable_vext = ref true
+let config_pmp_count = ref Big_int.zero
+let config_pmp_grain = ref Big_int.zero
+
+let set_config_pmp_count x = config_pmp_count := Big_int.of_int x
+let set_config_pmp_grain x = config_pmp_grain := Big_int.of_int x
let platform_arch = ref P.RV64
@@ -84,9 +88,10 @@ let enable_vext () = !config_enable_vext
let enable_dirty_update () = !config_enable_dirty_update
let enable_misaligned_access () = !config_enable_misaligned_access
let mtval_has_illegal_inst_bits () = !config_mtval_has_illegal_inst_bits
-let enable_pmp () = !config_enable_pmp
let enable_zfinx () = false
let enable_writable_fiom () = !config_enable_writable_fiom
+let pmp_count () = !config_pmp_count
+let pmp_grain () = !config_pmp_grain
let rom_base () = arch_bits_of_int64 P.rom_base
let rom_size () = arch_bits_of_int !rom_size_ref
diff --git a/ocaml_emulator/riscv_ocaml_sim.ml b/ocaml_emulator/riscv_ocaml_sim.ml
index c151d69..03887b7 100644
--- a/ocaml_emulator/riscv_ocaml_sim.ml
+++ b/ocaml_emulator/riscv_ocaml_sim.ml
@@ -41,9 +41,12 @@ let options = Arg.align ([("-dump-dts",
("-enable-misaligned-access",
Arg.Set P.config_enable_misaligned_access,
" enable misaligned accesses without M-mode traps");
- ("-enable-pmp",
- Arg.Set P.config_enable_pmp,
- " enable PMP support");
+ ("-pmp-count",
+ Arg.Int P.set_config_pmp_count,
+ " number of supported PMPs (0, 16, 64)");
+ ("-pmp-grain",
+ Arg.Int P.set_config_pmp_grain,
+ " exponent of granularity of PMP addresses (G in the spec)");
("-enable-next",
Arg.Set P.config_enable_next,
" enable N extension");