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.

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

Pmm support #452

Closed
wants to merge 5 commits into from
Closed
Show file tree
Hide file tree
Changes from 1 commit
Commits
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
5 changes: 5 additions & 0 deletions c_emulator/riscv_platform.c
Original file line number Diff line number Diff line change
Expand Up @@ -42,6 +42,11 @@ bool sys_enable_writable_fiom(unit u)
return rv_enable_writable_fiom;
}

bool sys_enable_pmm(unit u)
{
return rv_enable_pmm;
}

bool sys_enable_vext(unit u)
{
return rv_enable_vext;
Expand Down
1 change: 1 addition & 0 deletions c_emulator/riscv_platform.h
Original file line number Diff line number Diff line change
Expand Up @@ -7,6 +7,7 @@ bool sys_enable_fdext(unit);
bool sys_enable_zfinx(unit);
bool sys_enable_writable_misa(unit);
bool sys_enable_writable_fiom(unit);
bool sys_enable_pmm(unit);
bool sys_enable_vext(unit);

uint64_t sys_pmp_count(unit);
Expand Down
1 change: 1 addition & 0 deletions c_emulator/riscv_platform_impl.c
Original file line number Diff line number Diff line change
Expand Up @@ -17,6 +17,7 @@ bool rv_enable_dirty_update = false;
bool rv_enable_misaligned = false;
bool rv_mtval_has_illegal_inst_bits = false;
bool rv_enable_writable_fiom = true;
bool rv_enable_pmm = false;

uint64_t rv_ram_base = UINT64_C(0x80000000);
uint64_t rv_ram_size = UINT64_C(0x4000000);
Expand Down
1 change: 1 addition & 0 deletions c_emulator/riscv_platform_impl.h
Original file line number Diff line number Diff line change
Expand Up @@ -21,6 +21,7 @@ extern bool rv_enable_dirty_update;
extern bool rv_enable_misaligned;
extern bool rv_mtval_has_illegal_inst_bits;
extern bool rv_enable_writable_fiom;
extern bool rv_enable_pmm;

Choose a reason for hiding this comment

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

Nit: Here and throughout the PR, pmm is used to refer to pointer masking. I think "pm" or "zpm" would be a better naming (PMM stands for "pointer masking mode", which is only referring to the bits used to configure pointer masking).

Copy link
Author

Choose a reason for hiding this comment

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

That’s a great suggestion. I will proceed with changing it to "zpm".


extern uint64_t rv_ram_base;
extern uint64_t rv_ram_size;
Expand Down
6 changes: 6 additions & 0 deletions c_emulator/riscv_sim.c
Original file line number Diff line number Diff line change
Expand Up @@ -124,6 +124,7 @@ static struct option options[] = {
{"pmp-count", required_argument, 0, OPT_PMP_COUNT },
{"pmp-grain", required_argument, 0, OPT_PMP_GRAIN },
{"enable-next", no_argument, 0, 'N' },
{"enable-pmm", no_argument, 0, 'M' },
{"ram-size", required_argument, 0, 'z' },
{"disable-compressed", no_argument, 0, 'C' },
{"disable-writable-misa", no_argument, 0, 'I' },
Expand Down Expand Up @@ -249,6 +250,7 @@ static int process_args(int argc, char **argv)
"P"
"C"
"N"
"M"
"I"
"F"
"W"
Expand Down Expand Up @@ -312,6 +314,10 @@ static int process_args(int argc, char **argv)
fprintf(stderr, "enabling N extension.\n");
rv_enable_next = true;
break;
case 'M':
fprintf(stderr, "enabling pointer masking support.\n");
rv_enable_pmm = true;
break;
case 'I':
fprintf(stderr, "disabling writable misa CSR.\n");
rv_enable_writable_misa = false;
Expand Down
4 changes: 4 additions & 0 deletions handwritten_support/riscv_extras.lem
Original file line number Diff line number Diff line change
Expand Up @@ -169,6 +169,10 @@ val sys_enable_writable_fiom : unit -> bool
let sys_enable_writable_fiom () = true
declare ocaml target_rep function sys_enable_writable_fiom = `Platform.enable_writable_fiom`

val sys_enable_pmm : unit -> bool
let sys_enable_pmm () = false
declare ocaml target_rep function sys_enable_pmm = `Platform.enable_pmm`

val plat_ram_base : unit -> bitvector
let plat_ram_base () = []
declare ocaml target_rep function plat_ram_base = `Platform.dram_base`
Expand Down
1 change: 1 addition & 0 deletions handwritten_support/riscv_extras.v
Original file line number Diff line number Diff line change
Expand Up @@ -201,6 +201,7 @@ Axiom sys_enable_fdext : unit -> bool.
Axiom sys_enable_next : unit -> bool.
Axiom sys_enable_zfinx : unit -> bool.
Axiom sys_enable_writable_fiom : unit -> bool.
Axiom sys_enable_pmm : unit -> bool.

(* The constraint solver can do this itself, but a Coq bug puts
anonymous_subproof into the term instead of an actual subproof. *)
Expand Down
4 changes: 4 additions & 0 deletions handwritten_support/riscv_extras_sequential.lem
Original file line number Diff line number Diff line change
Expand Up @@ -157,6 +157,10 @@ val sys_enable_writable_fiom : unit -> bool
let sys_enable_writable_fiom () = true
declare ocaml target_rep function sys_enable_writable_fiom = `Platform.enable_writable_fiom`

val sys_enable_pmm : unit -> bool
let sys_enable_pmm () = false
declare ocaml target_rep function sys_enable_pmm = `Platform.enable_pmm`

val plat_ram_base : forall 'a. Size 'a => unit -> bitvector 'a
let plat_ram_base () = wordFromInteger 0
declare ocaml target_rep function plat_ram_base = `Platform.dram_base`
Expand Down
79 changes: 66 additions & 13 deletions model/riscv_insts_base.sail
Original file line number Diff line number Diff line change
Expand Up @@ -321,28 +321,79 @@ function check_misaligned(vaddr : xlenbits, width : word_width) -> bool =
WORD => vaddr[0] == bitone | vaddr[1] == bitone,
DOUBLE => vaddr[0] == bitone | vaddr[1] == bitone | vaddr[2] == bitone
}
function transform_VA (effective_address : xlenbits,PMLEN :int) -> xlenbits = {
assert(PMLEN >= 0, "PMLEN out of range");
assert(PMLEN <= 63, "PMLEN out of range");
let XLEN = sizeof(xlen);
let i = XLEN -(PMLEN +1);
let effective_bit = effective_address[i..i];
let NVBITS = replicate_bits(effective_bit, PMLEN);

Choose a reason for hiding this comment

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

Nit: This naming isn't quite accurate – NVBITS/VBITS is independent of pointer masking. I think what these variables describe are masked_bits/unmasked_bits.

Copy link
Author

Choose a reason for hiding this comment

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

I have modified the variable names as suggested.

let VBITS = effective_address[i..0];
NVBITS @ VBITS
}

function transform_PA (effective_address : xlenbits,PMLEN :int) -> xlenbits = {
assert(PMLEN >= 0, "PMLEN out of range");
assert(PMLEN <= 63, "PMLEN out of range");
let XLEN = sizeof(xlen);
let i = XLEN -(PMLEN + 1);
let NVBITS = replicate_bits(0b0, PMLEN);
let VBITS = effective_address[i..0];
NVBITS @ VBITS
}

function transform_effective_address(vaddr : xlenbits, pmm : bool) -> xlenbits = {

Choose a reason for hiding this comment

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

For misaligned addresses, will this be applied to each byte of the address or just the initial address? (the spec mandates the former.)

Copy link
Author

Choose a reason for hiding this comment

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

Currently, the misaligned extension is not integrated into the Sail model. Therefore, I am applying Pointer Masking only to the initial address. However, once the integration is complete, we will need to apply Pointer Masking to each byte of the address.

if pmm then {
let pmm_bits : bits(2) = get_pmm();
let mode : SATPMode = translationMode(cur_privilege);
match (mode) {
(Sbare) => {
match (pmm_bits){
(0b10) => transform_PA (vaddr,7),
(0b11) => transform_PA (vaddr,16),
}
},
(Sv48) => {

Choose a reason for hiding this comment

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

How will Sv39 be handled? Also, does the current code cover 2-stage address translation?

Copy link
Author

Choose a reason for hiding this comment

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

At present, the sail model does not support Hyper Visor, and therefore, it does not cover the 2-stage address translation Yet. However, I am implementing the PM for Sv39 mode.

match (pmm_bits){
(0b10) => transform_VA (vaddr,7),
(0b11) => transform_VA (vaddr,16),
}
},
(Sv57) => {
match (pmm_bits){
(0b10) => transform_VA (vaddr,7),
}
},
}
}
else {
vaddr //PMM is not active
}
}

function clause execute(LOAD(imm, rs1, rd, is_unsigned, width, aq, rl)) = {
let pmm = is_pmm_active();
let offset : xlenbits = sign_extend(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) {
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)) {
TR_Failure(e, _) => { handle_mem_exception(vaddr, e); RETIRE_FAIL },
let vaddr_ = transform_effective_address(vaddr, pmm) in
if check_misaligned(vaddr_, width)
then { handle_mem_exception(vaddr_, E_Load_Addr_Align()); RETIRE_FAIL }
else match translateAddr(vaddr_, Read(Data)) {
TR_Failure(e, _) => { handle_mem_exception(vaddr_, e); RETIRE_FAIL },
TR_Address(paddr, _) =>
match (width) {
BYTE =>
process_load(rd, vaddr, mem_read(Read(Data), paddr, 1, aq, rl, false), is_unsigned),
process_load(rd, vaddr_, mem_read(Read(Data), paddr, 1, aq, rl, false), is_unsigned),
HALF =>
process_load(rd, vaddr, mem_read(Read(Data), paddr, 2, aq, rl, false), is_unsigned),
process_load(rd, vaddr_, mem_read(Read(Data), paddr, 2, aq, rl, false), is_unsigned),
WORD =>
process_load(rd, vaddr, mem_read(Read(Data), paddr, 4, aq, rl, false), is_unsigned),
process_load(rd, vaddr_, mem_read(Read(Data), paddr, 4, aq, rl, false), is_unsigned),
DOUBLE if sizeof(xlen) >= 64 =>
process_load(rd, vaddr, mem_read(Read(Data), paddr, 8, aq, rl, false), is_unsigned),
process_load(rd, vaddr_, mem_read(Read(Data), paddr, 8, aq, rl, false), is_unsigned),
_ => report_invalid_width(__FILE__, __LINE__, width, "load")
}
}
Expand Down Expand Up @@ -379,16 +430,18 @@ mapping clause encdec = STORE(imm7 @ imm5, rs2, rs1, size, false, false)
/* NOTE: Currently, we only EA if address translation is successful.
This may need revisiting. */
function clause execute (STORE(imm, rs2, rs1, width, aq, rl)) = {
let pmm = is_pmm_active();
let offset : xlenbits = sign_extend(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) {
Ext_DataAddr_Error(e) => { ext_handle_data_check_error(e); RETIRE_FAIL },
Ext_DataAddr_OK(vaddr) =>
let vaddr_ = transform_effective_address(vaddr, pmm) in
if check_misaligned(vaddr, width)
then { handle_mem_exception(vaddr, E_SAMO_Addr_Align()); RETIRE_FAIL }
else match translateAddr(vaddr, Write(Data)) {
TR_Failure(e, _) => { handle_mem_exception(vaddr, e); RETIRE_FAIL },
then { handle_mem_exception(vaddr_, E_SAMO_Addr_Align()); RETIRE_FAIL }
else match translateAddr(vaddr_, Write(Data)) {
TR_Failure(e, _) => { handle_mem_exception(vaddr_, e); RETIRE_FAIL },
TR_Address(paddr, _) => {
let eares : MemoryOpResult(unit) = match width {
BYTE => mem_write_ea(paddr, 1, aq, rl, false),
Expand All @@ -397,7 +450,7 @@ function clause execute (STORE(imm, rs2, rs1, width, aq, rl)) = {
DOUBLE => mem_write_ea(paddr, 8, aq, rl, false)
};
match (eares) {
MemException(e) => { handle_mem_exception(vaddr, e); RETIRE_FAIL },
MemException(e) => { handle_mem_exception(vaddr_, e); RETIRE_FAIL },
MemValue(_) => {
let rs2_val = X(rs2);
let res : MemoryOpResult(bool) = match (width) {
Expand All @@ -411,7 +464,7 @@ function clause execute (STORE(imm, rs2, rs1, width, aq, rl)) = {
match (res) {
MemValue(true) => RETIRE_SUCCESS,
MemValue(false) => internal_error(__FILE__, __LINE__, "store got false from mem_write_value"),
MemException(e) => { handle_mem_exception(vaddr, e); RETIRE_FAIL }
MemException(e) => { handle_mem_exception(vaddr_, e); RETIRE_FAIL }
}
}
}
Expand Down
32 changes: 18 additions & 14 deletions model/riscv_insts_fext.sail
Original file line number Diff line number Diff line change
Expand Up @@ -312,26 +312,28 @@ function process_fload16(rd, addr, value) =
}

function clause execute(LOAD_FP(imm, rs1, rd, width)) = {
let pmm = is_pmm_active();
let offset : xlenbits = sign_extend(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) {
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 }
let vaddr_ = transform_effective_address(vaddr, pmm) in
if check_misaligned(vaddr_, width)
then { handle_mem_exception(vaddr_, E_Load_Addr_Align()); RETIRE_FAIL }
else match translateAddr(vaddr, Read(Data)) {
TR_Failure(e, _) => { handle_mem_exception(vaddr, e); RETIRE_FAIL },
TR_Failure(e, _) => { handle_mem_exception(vaddr_, e); RETIRE_FAIL },
TR_Address(addr, _) => {
let (aq, rl, res) = (false, false, false);
match (width) {
BYTE => { handle_illegal(); RETIRE_FAIL },
HALF =>
process_fload16(rd, vaddr, mem_read(Read(Data), addr, 2, aq, rl, res)),
process_fload16(rd, vaddr_, mem_read(Read(Data), addr, 2, aq, rl, res)),
WORD =>
process_fload32(rd, vaddr, mem_read(Read(Data), addr, 4, aq, rl, res)),
process_fload32(rd, vaddr_, mem_read(Read(Data), addr, 4, aq, rl, res)),
DOUBLE if sizeof(flen) >= 64 =>
process_fload64(rd, vaddr, mem_read(Read(Data), addr, 8, aq, rl, res)),
process_fload64(rd, vaddr_, mem_read(Read(Data), addr, 8, aq, rl, res)),
_ => report_invalid_width(__FILE__, __LINE__, width, "floating point load"),
}
}
Expand Down Expand Up @@ -377,17 +379,19 @@ function process_fstore(vaddr, value) =
}

function clause execute (STORE_FP(imm, rs2, rs1, width)) = {
let pmm = is_pmm_active();
let offset : xlenbits = sign_extend(imm);
let (aq, rl, con) = (false, false, false);
/* Get the address, X(rs1) + offset.
Some extensions perform additional checks on address validity. */
match ext_data_get_addr(rs1, offset, Write(Data), 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)) {
TR_Failure(e, _) => { handle_mem_exception(vaddr, e); RETIRE_FAIL },
let vaddr_ = transform_effective_address(vaddr, pmm) in
if check_misaligned(vaddr_, width)
then { handle_mem_exception(vaddr_, E_SAMO_Addr_Align()); RETIRE_FAIL }
else match translateAddr(vaddr_, Write(Data)) {
TR_Failure(e, _) => { handle_mem_exception(vaddr_, e); RETIRE_FAIL },
TR_Address(addr, _) => {
let eares : MemoryOpResult(unit) = match width {
BYTE => MemValue () /* bogus placeholder for illegal size */,
Expand All @@ -396,15 +400,15 @@ function clause execute (STORE_FP(imm, rs2, rs1, width)) = {
DOUBLE => mem_write_ea(addr, 8, aq, rl, false)
};
match (eares) {
MemException(e) => { handle_mem_exception(vaddr, e); RETIRE_FAIL },
MemException(e) => { handle_mem_exception(vaddr_, e); RETIRE_FAIL },
MemValue(_) => {
let rs2_val = F(rs2);
match (width) {
BYTE => { handle_illegal(); RETIRE_FAIL },
HALF => process_fstore (vaddr, mem_write_value(addr, 2, rs2_val[15..0], aq, rl, con)),
WORD => process_fstore (vaddr, mem_write_value(addr, 4, rs2_val[31..0], aq, rl, con)),
HALF => process_fstore (vaddr_, mem_write_value(addr, 2, rs2_val[15..0], aq, rl, con)),
WORD => process_fstore (vaddr_, mem_write_value(addr, 4, rs2_val[31..0], aq, rl, con)),
DOUBLE if sizeof(flen) >= 64 =>
process_fstore (vaddr, mem_write_value(addr, 8, rs2_val, aq, rl, con)),
process_fstore (vaddr_, mem_write_value(addr, 8, rs2_val, aq, rl, con)),
_ => report_invalid_width(__FILE__, __LINE__, width, "floating point store"),
};
}
Expand Down
33 changes: 30 additions & 3 deletions model/riscv_sys_regs.sail
Original file line number Diff line number Diff line change
Expand Up @@ -91,7 +91,8 @@ 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

/* whether the PME extension was enabled at boot */
val sys_enable_pmm = {c: "sys_enable_pmm", ocaml: "Platform.enable_pmm", _: "sys_enable_pmm"} : 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.
Expand Down Expand Up @@ -807,7 +808,11 @@ bitfield Envcfg : bits(64) = {
// Page Based Memory Types Extension
PBMTE : 62,
// Reserved WPRI bits.
wpri_1 : 61 .. 8,
wpri_2 : 61 .. 34,
// PMM bits of Pointer Masking Extension
PMM : 33 .. 32,
// Reserved WPRI bits.
wpri_1 : 31 .. 8,
// Cache Block Zero instruction Enable
CBZE : 7,
// Cache Block Clean and Flush instruction Enable
Expand All @@ -825,7 +830,9 @@ register senvcfg : Envcfg

function legalize_envcfg(o : Envcfg, v : bits(64)) -> Envcfg = {
let v = Mk_Envcfg(v);
let o = [o with FIOM = if sys_enable_writable_fiom() then v[FIOM] else 0b0];
let o = update_FIOM(o, if sys_enable_writable_fiom() then v.FIOM() else 0b0);
// Update PMM field only if Pointer Masking is enabled and Written value is legal
let o = update_PMM(o, if (sys_enable_pmm() & (sizeof(xlen) != 32) & (v.PMM() != 0b01)) then v.PMM() else o.PMM());
// Other extensions are not implemented yet so all other fields are read only zero.
o
}
Expand All @@ -840,6 +847,26 @@ function is_fiom_active() -> bool = {
User => (menvcfg[FIOM] | senvcfg[FIOM]) == 0b1,
}
}

// Return whether or not PMM is currently active, based on the current
// privilege and the menvcfg,senvcfg and mseccfg settings.
function is_pmm_active() -> bool = {
match cur_privilege {
Machine => (mseccfg.PMM() == 0b11 | mseccfg.PMM() == 0b10),
Supervisor => (menvcfg.PMM() == 0b11 | menvcfg.PMM() == 0b10),
User => ((menvcfg.PMM() == 0b11 | menvcfg.PMM() == 0b10) | (senvcfg.PMM() == 0b11 | senvcfg.PMM() == 0b10)),
}
}

//Returns the PMM bits value depends on the Privilege mode
function get_pmm() -> bits(2) = {
match cur_privilege {
Machine => mseccfg.PMM(),
Supervisor => menvcfg.PMM(),
User => senvcfg.PMM(),

Choose a reason for hiding this comment

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

I think this is only the case if the system has all of these privilege modes. For example, if a system does not have a supervisor mode, then menvcfg controls the user mode pointer masking.

Copy link
Author

Choose a reason for hiding this comment

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

I have updated the logic here as mentioned.

}
}

/* vector csrs */
register vstart : bits(16) /* use the largest possible length of vstart */
register vxsat : bits(1)
Expand Down
2 changes: 2 additions & 0 deletions ocaml_emulator/platform.ml
Original file line number Diff line number Diff line change
Expand Up @@ -14,6 +14,7 @@ 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 config_enable_pmm = ref false

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
Expand Down Expand Up @@ -90,6 +91,7 @@ let enable_misaligned_access () = !config_enable_misaligned_access
let mtval_has_illegal_inst_bits () = !config_mtval_has_illegal_inst_bits
let enable_zfinx () = false
let enable_writable_fiom () = !config_enable_writable_fiom
let enable_pmm () = !config_enable_pmm
let pmp_count () = !config_pmp_count
let pmp_grain () = !config_pmp_grain

Expand Down
3 changes: 3 additions & 0 deletions ocaml_emulator/riscv_ocaml_sim.ml
Original file line number Diff line number Diff line change
Expand Up @@ -50,6 +50,9 @@ let options = Arg.align ([("-dump-dts",
("-enable-next",
Arg.Set P.config_enable_next,
" enable N extension");
("-enable-pmm",
Arg.Set P.config_enable_pmm,
" enable PMM support");
("-mtval-has-illegal-inst-bits",
Arg.Set P.config_mtval_has_illegal_inst_bits,
" mtval stores instruction bits on an illegal instruction exception");
Expand Down