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>

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;

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

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;

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;

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

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`

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