Improve PMP support

This implements a lot of missing functionality for PMPs.

* Support 64 PMPs as well as 0 and 16.
* Support setting PMP grain
* Return correct address bits on read (some read as 0 or 1 depending on the grain and match type)
* Unlock PMPs on reset
* Implement pmpcfg WARL legalisation

Co-authored-by: Ben Fletcher <benjamin.fletcher@codasip.com>

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");