Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

Improve PMP support #350

Merged
merged 1 commit into from
Feb 5, 2024
Merged

Improve PMP support #350

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
15 changes: 10 additions & 5 deletions c_emulator/riscv_platform.c
View file
Open in desktop
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
Open in desktop
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
Open in desktop
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
Open in desktop
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
27 changes: 23 additions & 4 deletions c_emulator/riscv_sim.c
View file
Open in desktop
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,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' },
Expand Down Expand Up @@ -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"
Expand Down Expand Up @@ -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':
Timmmm marked this conversation as resolved.
Show resolved Hide resolved
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;
Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Do we need to handle invalid optarg here?

Copy link
Collaborator Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Ah yes the Sail assumes it is <=64 so we need to check that here. I'll add that.

Copy link
Collaborator Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Done. I added a check for pmp_grain too.

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");
Expand Down
4 changes: 0 additions & 4 deletions handwritten_support/riscv_extras.lem
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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`
Expand Down
4 changes: 0 additions & 4 deletions handwritten_support/riscv_extras_sequential.lem
View file
Open in desktop
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
Open in desktop
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
Open in desktop
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)),
Timmmm marked this conversation as resolved.
Show resolved Hide resolved
// 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
Open in desktop
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
Open in desktop
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
Loading