diff options
| -rw-r--r-- | c_emulator/riscv_platform.c | 15 | ||||
| -rw-r--r-- | c_emulator/riscv_platform.h | 4 | ||||
| -rw-r--r-- | c_emulator/riscv_platform_impl.c | 4 | ||||
| -rw-r--r-- | c_emulator/riscv_platform_impl.h | 4 | ||||
| -rw-r--r-- | c_emulator/riscv_sim.c | 27 | ||||
| -rw-r--r-- | handwritten_support/riscv_extras.lem | 4 | ||||
| -rw-r--r-- | handwritten_support/riscv_extras_sequential.lem | 4 | ||||
| -rw-r--r-- | model/riscv_csr_map.sail | 60 | ||||
| -rw-r--r-- | model/riscv_insts_zicsr.sail | 59 | ||||
| -rw-r--r-- | model/riscv_mem.sail | 4 | ||||
| -rw-r--r-- | model/riscv_platform.sail | 6 | ||||
| -rw-r--r-- | model/riscv_pmp_control.sail | 138 | ||||
| -rw-r--r-- | model/riscv_pmp_regs.sail | 186 | ||||
| -rw-r--r-- | model/riscv_sys_control.sail | 32 | ||||
| -rw-r--r-- | model/riscv_sys_regs.sail | 7 | ||||
| -rw-r--r-- | ocaml_emulator/platform.ml | 9 | ||||
| -rw-r--r-- | ocaml_emulator/riscv_ocaml_sim.ml | 9 |
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"); |