Skip to content

Commit

Permalink
Improve PMP support
Browse files Browse the repository at this point in the history 
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 <[email protected]>
  • Loading branch information
@Timmmm @ben-fletcher-codasip
Timmmm and ben-fletcher-codasip committed Dec 6, 2023
1 parent 153f983 commit 78d7ce1
Show file tree
Hide file tree
Showing 19 changed files with 273 additions and 305 deletions.
15 changes: 10 additions & 5 deletions c_emulator/riscv_platform.c
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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;
Expand All @@ -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;
Expand Down
4 changes: 3 additions & 1 deletion c_emulator/riscv_platform.h
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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);
Expand Down
4 changes: 3 additions & 1 deletion c_emulator/riscv_platform_impl.c
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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;
Expand Down
4 changes: 3 additions & 1 deletion c_emulator/riscv_platform_impl.h
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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;
Expand Down
26 changes: 22 additions & 4 deletions c_emulator/riscv_sim.c
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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;
Expand Down Expand Up @@ -119,7 +121,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' },
Expand Down Expand Up @@ -236,6 +240,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"
Expand Down Expand Up @@ -281,9 +288,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");
Expand Down
4 changes: 0 additions & 4 deletions handwritten_support/0.11/riscv_extras.lem
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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`
Expand Down
4 changes: 0 additions & 4 deletions handwritten_support/0.11/riscv_extras_sequential.lem
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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`
Expand Down
4 changes: 0 additions & 4 deletions handwritten_support/riscv_extras.lem
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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`
Expand Down
4 changes: 0 additions & 4 deletions handwritten_support/riscv_extras_sequential.lem
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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`
Expand Down
60 changes: 60 additions & 0 deletions model/riscv_csr_map.sail
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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"
Expand All @@ -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"
Expand Down
59 changes: 17 additions & 42 deletions model/riscv_insts_zicsr.sail
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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],
Expand Down Expand Up @@ -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) },
Expand Down
4 changes: 2 additions & 2 deletions model/riscv_mem.sail
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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) {
Expand Down Expand Up @@ -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) {
Expand Down
6 changes: 0 additions & 6 deletions model/riscv_platform.sail
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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",
Expand Down
Loading

0 comments on commit 78d7ce1

Please sign in to comment.