Improve PMP support

This implements a lot of missing functionality for PMPs.

* Support 64 PMPs as well as 0 and 16.
* Support read-only zero PMPs
* 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>

c_emulator/riscv_platform.c

@@ -47,6 +47,21 @@ 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_writable(unit u)
+{
+  return rv_pmp_writable;
+}
+
+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 +82,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;

c_emulator/riscv_platform.h

@@ -9,10 +9,13 @@ 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_writable(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);

c_emulator/riscv_platform_impl.c

@@ -3,7 +3,10 @@
 #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_writable = -1;
+uint64_t rv_pmp_grain = 0;
+
 bool rv_enable_zfinx = false;
 bool rv_enable_rvc = true;
 bool rv_enable_next = false;

c_emulator/riscv_platform_impl.h

@@ -8,7 +8,10 @@
 
 #define DEFAULT_RSTVEC 0x00001000
 
-extern bool rv_enable_pmp;
+extern uint64_t rv_pmp_count;
+extern uint64_t rv_pmp_writable;
+extern uint64_t rv_pmp_grain;
+
 extern bool rv_enable_zfinx;
 extern bool rv_enable_rvc;
 extern bool rv_enable_next;

c_emulator/riscv_sim.c

@@ -51,6 +51,9 @@ const char *RV32ISA = "RV32IMAC";
 
 #define OPT_TRACE_OUTPUT 1000
 #define OPT_ENABLE_WRITABLE_FIOM 1001
+#define OPT_PMP_COUNT 1002
+#define OPT_PMP_WRITABLE 1003
+#define OPT_PMP_GRAIN 1004
 
 static bool do_dump_dts = false;
 static bool do_show_times = false;
@@ -119,7 +122,9 @@ 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-writable",                required_argument, 0, OPT_PMP_WRITABLE        },
+    {"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 +241,9 @@ static int process_args(int argc, char **argv)
 {
   int c;
   uint64_t ram_size = 0;
+  uint64_t pmp_count = 0;
+  uint64_t pmp_writable = -1;
+  uint64_t pmp_grain = 0;
   while (true) {
     c = getopt_long(argc, argv,
                     "a"
@@ -281,9 +289,20 @@ 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);
+      rv_pmp_count = pmp_count;
+      break;
+    case OPT_PMP_WRITABLE:
+      pmp_writable = atol(optarg);
+      fprintf(stderr, "PMP writable: 0x%llx\n", pmp_writable);
+      rv_pmp_writable = pmp_writable;
+      break;
+    case OPT_PMP_GRAIN:
+      pmp_grain = atol(optarg);
+      fprintf(stderr, "PMP grain: %lld\n", pmp_grain);
+      rv_pmp_grain = pmp_grain;
       break;
     case 'C':
       fprintf(stderr, "disabling RVC compressed instructions.\n");

handwritten_support/0.11/riscv_extras.lem

@@ -123,10 +123,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`

handwritten_support/0.11/riscv_extras_sequential.lem

@@ -115,10 +115,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`

handwritten_support/riscv_extras.lem

@@ -197,10 +197,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`

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`

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"

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) },

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) {

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",