aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--c_emulator/riscv_platform.c3
-rw-r--r--c_emulator/riscv_platform.h1
-rw-r--r--c_emulator/riscv_platform_impl.c1
-rw-r--r--c_emulator/riscv_platform_impl.h1
-rw-r--r--c_emulator/riscv_sim.c5
-rw-r--r--handwritten_support/riscv_extras.lem4
-rw-r--r--handwritten_support/riscv_extras_sequential.lem4
-rw-r--r--model/riscv_addr_checks.sail2
-rw-r--r--model/riscv_fetch.sail8
-rw-r--r--model/riscv_insts_aext.sail21
-rw-r--r--model/riscv_insts_base.sail18
-rw-r--r--model/riscv_mem.sail42
-rw-r--r--model/riscv_platform.sail6
-rw-r--r--model/riscv_pmp_control.sail28
-rw-r--r--model/riscv_pmp_regs.sail10
-rw-r--r--model/riscv_sys_control.sail2
-rw-r--r--model/riscv_types.sail9
-rw-r--r--model/riscv_vmem_rv32.sail10
-rw-r--r--model/riscv_vmem_rv64.sail10
-rw-r--r--model/riscv_vmem_sv32.sail2
-rw-r--r--model/riscv_vmem_sv39.sail2
-rw-r--r--model/riscv_vmem_sv48.sail2
-rw-r--r--ocaml_emulator/platform.ml2
-rw-r--r--ocaml_emulator/riscv_ocaml_sim.ml3
24 files changed, 135 insertions, 61 deletions
diff --git a/c_emulator/riscv_platform.c b/c_emulator/riscv_platform.c
index dcc5766..c88f688 100644
--- a/c_emulator/riscv_platform.c
+++ b/c_emulator/riscv_platform.c
@@ -23,6 +23,9 @@ bool plat_enable_misaligned_access(unit u)
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 31f2807..85cf3fd 100644
--- a/c_emulator/riscv_platform.h
+++ b/c_emulator/riscv_platform.h
@@ -7,6 +7,7 @@ bool sys_enable_writable_misa(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 5894fc9..695384c 100644
--- a/c_emulator/riscv_platform_impl.c
+++ b/c_emulator/riscv_platform_impl.c
@@ -3,6 +3,7 @@
#include <stdio.h>
/* Settings of the platform implementation, with common defaults. */
+bool rv_enable_pmp = false;
bool rv_enable_rvc = true;
bool rv_enable_writable_misa = true;
diff --git a/c_emulator/riscv_platform_impl.h b/c_emulator/riscv_platform_impl.h
index cf3bc30..60b9181 100644
--- a/c_emulator/riscv_platform_impl.h
+++ b/c_emulator/riscv_platform_impl.h
@@ -7,6 +7,7 @@
#define DEFAULT_RSTVEC 0x00001000
+extern bool rv_enable_pmp;
extern bool rv_enable_rvc;
extern bool rv_enable_writable_misa;
extern bool rv_enable_dirty_update;
diff --git a/c_emulator/riscv_sim.c b/c_emulator/riscv_sim.c
index d9a1c23..af0df02 100644
--- a/c_emulator/riscv_sim.c
+++ b/c_emulator/riscv_sim.c
@@ -75,6 +75,7 @@ int total_insns = 0;
static struct option options[] = {
{"enable-dirty-update", no_argument, 0, 'd'},
{"enable-misaligned", no_argument, 0, 'm'},
+ {"enable-pmp", no_argument, 0, 'P'},
{"ram-size", required_argument, 0, 'z'},
{"disable-compressed", no_argument, 0, 'C'},
{"disable-writable-misa", no_argument, 0, 'I'},
@@ -185,6 +186,10 @@ char *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;
+ break;
case 'C':
fprintf(stderr, "disabling RVC compressed instructions.\n");
rv_enable_rvc = false;
diff --git a/handwritten_support/riscv_extras.lem b/handwritten_support/riscv_extras.lem
index 66b5d94..da6106d 100644
--- a/handwritten_support/riscv_extras.lem
+++ b/handwritten_support/riscv_extras.lem
@@ -111,6 +111,10 @@ 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 604911a..7715614 100644
--- a/handwritten_support/riscv_extras_sequential.lem
+++ b/handwritten_support/riscv_extras_sequential.lem
@@ -107,6 +107,10 @@ 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_addr_checks.sail b/model/riscv_addr_checks.sail
index 28e688d..06e20f9 100644
--- a/model/riscv_addr_checks.sail
+++ b/model/riscv_addr_checks.sail
@@ -46,7 +46,7 @@ type ext_data_addr_error = unit
/* Default data addr is just base register + immediate offset (may be zero).
Extensions might override and add additional checks. */
-function ext_data_get_addr(base : regidx, offset : xlenbits, acc : AccessType, rt : ReadType, width : word_width)
+function ext_data_get_addr(base : regidx, offset : xlenbits, acc : AccessType, width : word_width)
-> Ext_DataAddr_Check(ext_data_addr_error) =
let addr = X(base) + offset in
Ext_DataAddr_OK(addr)
diff --git a/model/riscv_fetch.sail b/model/riscv_fetch.sail
index b076b95..ae8748c 100644
--- a/model/riscv_fetch.sail
+++ b/model/riscv_fetch.sail
@@ -14,14 +14,14 @@ function fetch() -> FetchResult =
Ext_FetchAddr_OK(use_pc) => {
if (use_pc[0] != 0b0 | (use_pc[1] != 0b0 & (~ (haveRVC()))))
then F_Error(E_Fetch_Addr_Align, PC)
- else match translateAddr(use_pc, Execute, Instruction) {
+ else match translateAddr(use_pc, Execute) {
TR_Failure(e) => F_Error(e, PC),
TR_Address(ppclo) => {
/* split instruction fetch into 16-bit granules to handle RVC, as
* well as to generate precise fault addresses in any fetch
* exceptions.
*/
- match mem_read(Instruction, ppclo, 2, false, false, false) {
+ match mem_read(Execute, ppclo, 2, false, false, false) {
MemException(e) => F_Error(E_Fetch_Access_Fault, PC),
MemValue(ilo) => {
if isRVC(ilo)
@@ -32,10 +32,10 @@ function fetch() -> FetchResult =
match ext_fetch_check_pc(PC, PC_hi) {
Ext_FetchAddr_Error(e) => F_Ext_Error(e),
Ext_FetchAddr_OK(use_pc_hi) => {
- match translateAddr(use_pc_hi, Execute, Instruction) {
+ match translateAddr(use_pc_hi, Execute) {
TR_Failure(e) => F_Error(e, PC_hi),
TR_Address(ppchi) => {
- match mem_read(Instruction, ppchi, 2, false, false, false) {
+ match mem_read(Execute, ppchi, 2, false, false, false) {
MemException(e) => F_Error(E_Fetch_Access_Fault, PC_hi),
MemValue(ihi) => F_Base(append(ihi, ilo))
}
diff --git a/model/riscv_insts_aext.sail b/model/riscv_insts_aext.sail
index 91346ee..cd2f069 100644
--- a/model/riscv_insts_aext.sail
+++ b/model/riscv_insts_aext.sail
@@ -44,7 +44,7 @@ function clause execute(LOADRES(aq, rl, rs1, width, rd)) = {
/* Get the address, X(rs1) (no offset).
* Extensions might perform additional checks on address validity.
*/
- match ext_data_get_addr(rs1, zeros(), Read, Data, width) {
+ match ext_data_get_addr(rs1, zeros(), Read, width) {
Ext_DataAddr_Error(e) => { ext_handle_data_check_error(e); RETIRE_FAIL },
Ext_DataAddr_OK(vaddr) => {
let aligned : bool =
@@ -62,12 +62,12 @@ function clause execute(LOADRES(aq, rl, rs1, width, rd)) = {
*/
if (~ (aligned))
then { handle_mem_exception(vaddr, E_Load_Addr_Align); RETIRE_FAIL }
- else match translateAddr(vaddr, Read, Data) {
+ else match translateAddr(vaddr, Read) {
TR_Failure(e) => { handle_mem_exception(vaddr, e); RETIRE_FAIL },
TR_Address(addr) =>
match (width, sizeof(xlen)) {
- (WORD, _) => process_loadres(rd, vaddr, mem_read(Data, addr, 4, aq, rl, true), false),
- (DOUBLE, 64) => process_loadres(rd, vaddr, mem_read(Data, addr, 8, aq, rl, true), false),
+ (WORD, _) => process_loadres(rd, vaddr, mem_read(Read, addr, 4, aq, rl, true), false),
+ (DOUBLE, 64) => process_loadres(rd, vaddr, mem_read(Read, addr, 8, aq, rl, true), false),
_ => internal_error("LOADRES expected WORD or DOUBLE")
}
}
@@ -103,7 +103,7 @@ function clause execute (STORECON(aq, rl, rs2, rs1, width, rd)) = {
/* Get the address, X(rs1) (no offset).
* Extensions might perform additional checks on address validity.
*/
- match ext_data_get_addr(rs1, zeros(), Read, Data, width) {
+ match ext_data_get_addr(rs1, zeros(), Write, width) {
Ext_DataAddr_Error(e) => { ext_handle_data_check_error(e); RETIRE_FAIL },
Ext_DataAddr_OK(vaddr) => {
let aligned : bool =
@@ -123,7 +123,8 @@ function clause execute (STORECON(aq, rl, rs2, rs1, width, rd)) = {
/* cannot happen in rmem */
X(rd) = EXTZ(0b1); cancel_reservation(); RETIRE_SUCCESS
} else {
- match translateAddr(vaddr, Write, Data) {
+ match translateAddr(vaddr, Write) { /* Write and ReadWrite are equivalent here:
+ * both result in a SAMO exception */
TR_Failure(e) => { handle_mem_exception(vaddr, e); RETIRE_FAIL },
TR_Address(addr) => {
let eares : MemoryOpResult(unit) = match (width, sizeof(xlen)) {
@@ -188,10 +189,10 @@ function clause execute (AMO(op, aq, rl, rs2, rs1, width, rd)) = {
/* Get the address, X(rs1) (no offset).
* Some extensions perform additional checks on address validity.
*/
- match ext_data_get_addr(rs1, zeros(), Read, Data, width) {
+ match ext_data_get_addr(rs1, zeros(), ReadWrite, width) {
Ext_DataAddr_Error(e) => { ext_handle_data_check_error(e); RETIRE_FAIL },
Ext_DataAddr_OK(vaddr) => {
- match translateAddr(vaddr, ReadWrite, Data) {
+ match translateAddr(vaddr, ReadWrite) {
TR_Failure(e) => { handle_mem_exception(vaddr, e); RETIRE_FAIL },
TR_Address(addr) => {
let eares : MemoryOpResult(unit) = match (width, sizeof(xlen)) {
@@ -204,8 +205,8 @@ function clause execute (AMO(op, aq, rl, rs2, rs1, width, rd)) = {
MemException(e) => { handle_mem_exception(addr, e); RETIRE_FAIL },
MemValue(_) => {
let rval : MemoryOpResult(xlenbits) = match (width, sizeof(xlen)) {
- (WORD, _) => extend_value(false, mem_read(Data, addr, 4, aq, aq & rl, true)),
- (DOUBLE, 64) => extend_value(false, mem_read(Data, addr, 8, aq, aq & rl, true)),
+ (WORD, _) => extend_value(false, mem_read(ReadWrite, addr, 4, aq, aq & rl, true)),
+ (DOUBLE, 64) => extend_value(false, mem_read(ReadWrite, addr, 8, aq, aq & rl, true)),
_ => internal_error ("AMO expected WORD or DOUBLE")
};
match (rval) {
diff --git a/model/riscv_insts_base.sail b/model/riscv_insts_base.sail
index acfd1db..14a626e 100644
--- a/model/riscv_insts_base.sail
+++ b/model/riscv_insts_base.sail
@@ -287,7 +287,7 @@ mapping clause assembly = RTYPE(rs2, rs1, rd, op)
/* ****************************************************************** */
union clause ast = LOAD : (bits(12), regidx, regidx, bool, word_width, bool, bool)
-/* unsigned loads are only present for widths strictly less than xlen,
+/* unsigned loads are only present for widths strictly less than xlen,
signed loads also present for widths equal to xlen */
mapping clause encdec = LOAD(imm, rs1, rd, is_unsigned, size, false, false) if (word_width_bytes(size) < sizeof(xlen_bytes)) | (not_bool(is_unsigned) & word_width_bytes(size) <= sizeof(xlen_bytes))
<-> imm @ rs1 @ bool_bits(is_unsigned) @ size_bits(size) @ rd @ 0b0000011 if (word_width_bytes(size) < sizeof(xlen_bytes)) | (not_bool(is_unsigned) & word_width_bytes(size) <= sizeof(xlen_bytes))
@@ -318,23 +318,23 @@ function clause execute(LOAD(imm, rs1, rd, is_unsigned, width, aq, rl)) = {
let offset : xlenbits = EXTS(imm);
/* Get the address, X(rs1) + offset.
Some extensions perform additional checks on address validity. */
- match ext_data_get_addr(rs1, offset, Read, Data, width) {
+ match ext_data_get_addr(rs1, offset, Read, width) {
Ext_DataAddr_Error(e) => { ext_handle_data_check_error(e); RETIRE_FAIL },
Ext_DataAddr_OK(vaddr) =>
if check_misaligned(vaddr, width)
then { handle_mem_exception(vaddr, E_Load_Addr_Align); RETIRE_FAIL }
- else match translateAddr(vaddr, Read, Data) {
+ else match translateAddr(vaddr, Read) {
TR_Failure(e) => { handle_mem_exception(vaddr, e); RETIRE_FAIL },
TR_Address(addr) =>
match (width, sizeof(xlen)) {
(BYTE, _) =>
- process_load(rd, vaddr, mem_read(Data, addr, 1, aq, rl, false), is_unsigned),
+ process_load(rd, vaddr, mem_read(Read, addr, 1, aq, rl, false), is_unsigned),
(HALF, _) =>
- process_load(rd, vaddr, mem_read(Data, addr, 2, aq, rl, false), is_unsigned),
+ process_load(rd, vaddr, mem_read(Read, addr, 2, aq, rl, false), is_unsigned),
(WORD, _) =>
- process_load(rd, vaddr, mem_read(Data, addr, 4, aq, rl, false), is_unsigned),
+ process_load(rd, vaddr, mem_read(Read, addr, 4, aq, rl, false), is_unsigned),
(DOUBLE, 64) =>
- process_load(rd, vaddr, mem_read(Data, addr, 8, aq, rl, false), is_unsigned)
+ process_load(rd, vaddr, mem_read(Read, addr, 8, aq, rl, false), is_unsigned)
}
}
}
@@ -373,12 +373,12 @@ function clause execute (STORE(imm, rs2, rs1, width, aq, rl)) = {
let offset : xlenbits = EXTS(imm);
/* Get the address, X(rs1) + offset.
Some extensions perform additional checks on address validity. */
- match ext_data_get_addr(rs1, offset, Write, Data, width) {
+ match ext_data_get_addr(rs1, offset, Write, width) {
Ext_DataAddr_Error(e) => { ext_handle_data_check_error(e); RETIRE_FAIL },
Ext_DataAddr_OK(vaddr) =>
if check_misaligned(vaddr, width)
then { handle_mem_exception(vaddr, E_SAMO_Addr_Align); RETIRE_FAIL }
- else match translateAddr(vaddr, Write, Data) {
+ else match translateAddr(vaddr, Write) {
TR_Failure(e) => { handle_mem_exception(vaddr, e); RETIRE_FAIL },
TR_Address(addr) => {
let eares : MemoryOpResult(unit) = match width {
diff --git a/model/riscv_mem.sail b/model/riscv_mem.sail
index 5fa9a3c..ee9db4e 100644
--- a/model/riscv_mem.sail
+++ b/model/riscv_mem.sail
@@ -8,7 +8,7 @@ function is_aligned_addr forall 'n. (addr : xlenbits, width : atom('n)) -> bool
unsigned(addr) % width == 0
// only used for actual memory regions, to avoid MMIO effects
-function phys_mem_read forall 'n, 'n > 0. (t : ReadType, addr : xlenbits, width : atom('n), aq : bool, rl: bool, res : bool) -> MemoryOpResult(bits(8 * 'n)) = {
+function phys_mem_read forall 'n, 'n > 0. (t : AccessType, addr : xlenbits, width : atom('n), aq : bool, rl: bool, res : bool) -> MemoryOpResult(bits(8 * 'n)) = {
let result = (match (aq, rl, res) {
(false, false, false) => Some(read_ram(Read_plain, addr, width)),
(true, false, false) => Some(read_ram(Read_RISCV_acquire, addr, width)),
@@ -20,21 +20,31 @@ function phys_mem_read forall 'n, 'n > 0. (t : ReadType, addr : xlenbits, width
(false, true, true) => None()
}) : option(bits(8 * 'n));
match (t, result) {
- (Instruction, None()) => MemException(E_Fetch_Access_Fault),
- (Data, None()) => MemException(E_Load_Access_Fault),
- (_, Some(v)) => { print_mem("mem[" ^ t ^ "," ^ BitStr(addr) ^ "] -> " ^ BitStr(v));
- MemValue(v) }
+ (Execute, None()) => MemException(E_Fetch_Access_Fault),
+ (Read, None()) => MemException(E_Load_Access_Fault),
+ (_, None()) => MemException(E_SAMO_Access_Fault),
+ (_, Some(v)) => { print_mem("mem[" ^ t ^ "," ^ BitStr(addr) ^ "] -> " ^ BitStr(v));
+ MemValue(v) }
}
}
-function checked_mem_read forall 'n, 'n > 0. (t : ReadType, addr : xlenbits, width : atom('n), aq : bool, rl : bool, res: bool) -> MemoryOpResult(bits(8 * 'n)) =
- /* treat MMIO regions as not executable for now. TODO: this should actually come from PMP/PMA. */
- if t == Data & within_mmio_readable(addr, width)
+function checked_mem_read forall 'n, 'n > 0. (t : AccessType, addr : xlenbits, width : atom('n), aq : bool, rl : bool, res: bool) -> MemoryOpResult(bits(8 * 'n)) =
+ if within_mmio_readable(addr, width)
then mmio_read(addr, width)
else if within_phys_mem(addr, width)
then phys_mem_read(t, addr, width, aq, rl, res)
else MemException(E_Load_Access_Fault)
+function pmp_mem_read forall 'n, 'n > 0. (t : AccessType, addr : xlenbits, width : atom('n), aq : bool, rl : bool, res: bool) -> MemoryOpResult(bits(8 * 'n)) =
+ if (~ (plat_enable_pmp ()))
+ then checked_mem_read(t, addr, width, aq, rl, res)
+ else {
+ match pmpCheck(addr, width, t, effectivePrivilege(mstatus, cur_privilege)) {
+ None() => checked_mem_read(t, addr, width, aq, rl, res),
+ Some(e) => MemException(e)
+ }
+ }
+
/* Atomic accesses can be done to MMIO regions, e.g. in kernel access to device registers. */
$ifdef RVFI_DII
@@ -56,9 +66,9 @@ $endif
/* NOTE: The rreg effect is due to MMIO. */
$ifdef RVFI_DII
-val mem_read : forall 'n, 'n > 0. (ReadType, xlenbits, atom('n), bool, bool, bool) -> MemoryOpResult(bits(8 * 'n)) effect {wreg, rmem, rreg, escape}
+val mem_read : forall 'n, 'n > 0. (AccessType, xlenbits, atom('n), bool, bool, bool) -> MemoryOpResult(bits(8 * 'n)) effect {wreg, rmem, rreg, escape}
$else
-val mem_read : forall 'n, 'n > 0. (ReadType, xlenbits, atom('n), bool, bool, bool) -> MemoryOpResult(bits(8 * 'n)) effect {rmem, rreg, escape}
+val mem_read : forall 'n, 'n > 0. (AccessType, xlenbits, atom('n), bool, bool, bool) -> MemoryOpResult(bits(8 * 'n)) effect {rmem, rreg, escape}
$endif
function mem_read (typ, addr, width, aq, rl, res) = {
@@ -68,7 +78,7 @@ function mem_read (typ, addr, width, aq, rl, res) = {
else match (aq, rl, res) {
(false, true, false) => throw(Error_not_implemented("load.rl")),
(false, true, true) => throw(Error_not_implemented("lr.rl")),
- (_, _, _) => checked_mem_read(typ, addr, width, aq, rl, res)
+ (_, _, _) => pmp_mem_read(typ, addr, width, aq, rl, res)
};
rvfi_read(addr, width, result);
result
@@ -130,6 +140,14 @@ function checked_mem_write forall 'n, 'n > 0. (addr : xlenbits, width : atom('n)
then phys_mem_write(addr, width, data, meta, aq, rl, con)
else MemException(E_SAMO_Access_Fault)
+function pmp_mem_write forall 'n, 'n > 0. (addr : xlenbits, width : atom('n), data: bits(8 * 'n), meta: mem_meta, aq : bool, rl : bool, con : bool) -> MemoryOpResult(bool) =
+ if (~ (plat_enable_pmp ()))
+ then checked_mem_write(addr, width, data, meta, aq, rl, con)
+ else match pmpCheck(addr, width, Write, effectivePrivilege(mstatus, cur_privilege)) {
+ None() => checked_mem_write(addr, width, data, meta, aq, rl, con),
+ Some(e) => MemException(e)
+ }
+
/* Atomic accesses can be done to MMIO regions, e.g. in kernel access to device registers. */
/* Memory write with a default metadata value */
@@ -141,7 +159,7 @@ function mem_write_value (addr, width, value, aq, rl, con) = {
else match (aq, rl, con) {
(true, false, false) => throw(Error_not_implemented("store.aq")),
(true, false, true) => throw(Error_not_implemented("sc.aq")),
- (_, _, _) => checked_mem_write(addr, width, value, default_meta, aq, rl, con)
+ (_, _, _) => pmp_mem_write(addr, width, value, default_meta, aq, rl, con)
}
}
diff --git a/model/riscv_platform.sail b/model/riscv_platform.sail
index 87fa425..d440489 100644
--- a/model/riscv_platform.sail
+++ b/model/riscv_platform.sail
@@ -22,6 +22,12 @@ 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 4260888..4c65f7d 100644
--- a/model/riscv_pmp_control.sail
+++ b/model/riscv_pmp_control.sail
@@ -82,9 +82,9 @@ function pmpMatchEntry(addr: xlenbits, width: xlenbits, acc: AccessType, priv: P
/* priority checks */
-function pmpCheck(addr: xlenbits, width: xlenbits, acc: AccessType, priv: Privilege,
- ent: Pmpcfg_ent, pmpaddr: xlenbits, prev_pmpaddr: xlenbits)
+function pmpCheck forall 'n, 'n > 0. (addr: xlenbits, width: atom('n), acc: AccessType, 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,
@@ -149,7 +149,10 @@ function pmpCheck(addr: xlenbits, width: xlenbits, acc: AccessType, priv: Privil
match pmpMatchEntry(addr, width, acc, priv, pmp15cfg, pmpaddr15, pmpaddr14) {
PMP_Success => true,
PMP_Fail => false,
- PMP_Continue => false
+ PMP_Continue => match priv {
+ Machine => true,
+ _ => false
+ }
}}}}}}}}}}}}}}}};
if check
@@ -161,3 +164,22 @@ function pmpCheck(addr: xlenbits, width: xlenbits, acc: AccessType, priv: Privil
Execute => Some(E_Fetch_Access_Fault)
}
}
+
+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))
+}
diff --git a/model/riscv_pmp_regs.sail b/model/riscv_pmp_regs.sail
index 5d1ee40..b2c5bfb 100644
--- a/model/riscv_pmp_regs.sail
+++ b/model/riscv_pmp_regs.sail
@@ -12,6 +12,16 @@ function pmpAddrMatchType_of_bits(bs) = {
}
}
+val cast pmpAddrMatchType_to_bits : PmpAddrMatchType -> bits(2)
+function pmpAddrMatchType_to_bits(bs) = {
+ match bs {
+ OFF => 0b00,
+ TOR => 0b01,
+ NA4 => 0b10,
+ NAPOT => 0b11
+ }
+}
+
bitfield Pmpcfg_ent : bits(8) = {
L : 7, /* locking */
A : 4 .. 3, /* address match type, encoded as above */
diff --git a/model/riscv_sys_control.sail b/model/riscv_sys_control.sail
index e866986..27c2566 100644
--- a/model/riscv_sys_control.sail
+++ b/model/riscv_sys_control.sail
@@ -444,6 +444,8 @@ function init_sys() -> unit = {
minstret = EXTZ(0b0);
minstret_written = false;
+ init_pmp();
+
// log compatibility with spike
print_reg("CSR mstatus <- " ^ BitStr(mstatus.bits()) ^ " (input: " ^ BitStr(EXTZ(0b0) : xlenbits) ^ ")")
}
diff --git a/model/riscv_types.sail b/model/riscv_types.sail
index 1cb595e..ef8d011 100644
--- a/model/riscv_types.sail
+++ b/model/riscv_types.sail
@@ -106,15 +106,6 @@ function accessType_to_str (a) =
Execute => "X"
}
-enum ReadType = {Instruction, Data}
-
-val cast readType_to_str : ReadType -> string
-function readType_to_str (r) =
- match (r) {
- Instruction => "I",
- Data => "D"
- }
-
enum word_width = {BYTE, HALF, WORD, DOUBLE}
/* architectural interrupt definitions */
diff --git a/model/riscv_vmem_rv32.sail b/model/riscv_vmem_rv32.sail
index d0fac76..5b640b1 100644
--- a/model/riscv_vmem_rv32.sail
+++ b/model/riscv_vmem_rv32.sail
@@ -26,11 +26,11 @@ function translationMode(priv) = {
/* Top-level address translation dispatcher */
-val translateAddr : (xlenbits, AccessType, ReadType) -> TR_Result(xlenbits, ExceptionType) effect {escape, rmem, rreg, wmv, wmvt, wreg}
-function translateAddr(vAddr, ac, rt) = {
- let effPriv : Privilege = match rt {
- Instruction => cur_privilege,
- Data => effectivePrivilege(mstatus, cur_privilege)
+val translateAddr : (xlenbits, AccessType) -> TR_Result(xlenbits, ExceptionType) effect {escape, rmem, rreg, wmv, wmvt, wreg}
+function translateAddr(vAddr, ac) = {
+ let effPriv : Privilege = match ac {
+ Execute => cur_privilege,
+ _ => effectivePrivilege(mstatus, cur_privilege)
};
let mxr : bool = mstatus.MXR() == true;
let do_sum : bool = mstatus.SUM() == true;
diff --git a/model/riscv_vmem_rv64.sail b/model/riscv_vmem_rv64.sail
index cb2d1e5..e3cca0b 100644
--- a/model/riscv_vmem_rv64.sail
+++ b/model/riscv_vmem_rv64.sail
@@ -33,11 +33,11 @@ function translationMode(priv) = {
/* Top-level address translation dispatcher */
-val translateAddr : (xlenbits, AccessType, ReadType) -> TR_Result(xlenbits, ExceptionType) effect {escape, rmem, rreg, wmv, wmvt, wreg}
-function translateAddr(vAddr, ac, rt) = {
- let effPriv : Privilege = match rt {
- Instruction => cur_privilege,
- Data => effectivePrivilege(mstatus, cur_privilege)
+val translateAddr : (xlenbits, AccessType) -> TR_Result(xlenbits, ExceptionType) effect {escape, rmem, rreg, wmv, wmvt, wreg}
+function translateAddr(vAddr, ac) = {
+ let effPriv : Privilege = match ac {
+ Execute => cur_privilege,
+ _ => effectivePrivilege(mstatus, cur_privilege)
};
let mxr : bool = mstatus.MXR() == true;
let do_sum : bool = mstatus.SUM() == true;
diff --git a/model/riscv_vmem_sv32.sail b/model/riscv_vmem_sv32.sail
index 21fa68a..49d7ec1 100644
--- a/model/riscv_vmem_sv32.sail
+++ b/model/riscv_vmem_sv32.sail
@@ -12,7 +12,7 @@ function walk32(vaddr, ac, priv, mxr, do_sum, ptb, level, global) = {
let pt_ofs : paddr32 = shiftl(EXTZ(shiftr(va.VPNi(), (level * SV32_LEVEL_BITS))[(SV32_LEVEL_BITS - 1) .. 0]),
PTE32_LOG_SIZE);
let pte_addr = ptb + pt_ofs;
- match (mem_read(Data, to_phys_addr(pte_addr), 4, false, false, false)) {
+ match (mem_read(ac, to_phys_addr(pte_addr), 4, false, false, false)) {
MemException(_) => {
/* print("walk32(vaddr=" ^ BitStr(vaddr) ^ " level=" ^ string_of_int(level)
^ " pt_base=" ^ BitStr(to_phys_addr(ptb))
diff --git a/model/riscv_vmem_sv39.sail b/model/riscv_vmem_sv39.sail
index d68190f..a575a07 100644
--- a/model/riscv_vmem_sv39.sail
+++ b/model/riscv_vmem_sv39.sail
@@ -6,7 +6,7 @@ function walk39(vaddr, ac, priv, mxr, do_sum, ptb, level, global) = {
let pt_ofs : paddr64 = shiftl(EXTZ(shiftr(va.VPNi(), (level * SV39_LEVEL_BITS))[(SV39_LEVEL_BITS - 1) .. 0]),
PTE39_LOG_SIZE);
let pte_addr = ptb + pt_ofs;
- match (mem_read(Data, EXTZ(pte_addr), 8, false, false, false)) {
+ match (mem_read(ac, EXTZ(pte_addr), 8, false, false, false)) {
MemException(_) => {
/* print("walk39(vaddr=" ^ BitStr(vaddr) ^ " level=" ^ string_of_int(level)
^ " pt_base=" ^ BitStr(ptb)
diff --git a/model/riscv_vmem_sv48.sail b/model/riscv_vmem_sv48.sail
index 162097d..a898ac7 100644
--- a/model/riscv_vmem_sv48.sail
+++ b/model/riscv_vmem_sv48.sail
@@ -6,7 +6,7 @@ function walk48(vaddr, ac, priv, mxr, do_sum, ptb, level, global) = {
let pt_ofs : paddr64 = shiftl(EXTZ(shiftr(va.VPNi(), (level * SV48_LEVEL_BITS))[(SV48_LEVEL_BITS - 1) .. 0]),
PTE48_LOG_SIZE);
let pte_addr = ptb + pt_ofs;
- match (mem_read(Data, EXTZ(pte_addr), 8, false, false, false)) {
+ match (mem_read(ac, EXTZ(pte_addr), 8, false, false, false)) {
MemException(_) => {
/* print("walk48(vaddr=" ^ BitStr(vaddr) ^ " level=" ^ string_of_int(level)
^ " pt_base=" ^ BitStr(ptb)
diff --git a/ocaml_emulator/platform.ml b/ocaml_emulator/platform.ml
index 11abaf1..f4a8a3c 100644
--- a/ocaml_emulator/platform.ml
+++ b/ocaml_emulator/platform.ml
@@ -9,6 +9,7 @@ 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 platform_arch = ref P.RV64
@@ -72,6 +73,7 @@ let enable_rvc () = !config_enable_rvc
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 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 5f5c716..f827ad5 100644
--- a/ocaml_emulator/riscv_ocaml_sim.ml
+++ b/ocaml_emulator/riscv_ocaml_sim.ml
@@ -37,6 +37,9 @@ 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");
("-mtval-has-illegal-inst-bits",
Arg.Set P.config_mtval_has_illegal_inst_bits,
" mtval stores instruction bits on an illegal instruction exception");
generated by cgit v1.1 at 2024-10-20 06:15:21 +0000