Skip to content

Commit

Permalink
addressed some comments
Browse files Browse the repository at this point in the history
  • Loading branch information
@HAMZA-AFZAL404
HAMZA-AFZAL404 committed Sep 16, 2024
1 parent e36958b commit 0245007
Show file tree
Hide file tree
Showing 6 changed files with 56 additions and 79 deletions.
12 changes: 6 additions & 6 deletions c_emulator/riscv_sim.c
View file
Original file line number Diff line number Diff line change
Expand Up @@ -59,7 +59,7 @@ enum {
OPT_ENABLE_ZICBOM,
OPT_ENABLE_ZICBOZ,
OPT_CACHE_BLOCK_SIZE,
OPT_ENABLE_ZJPM,
OPT_ENABLE_ZPM,
};

static bool do_dump_dts = false;
Expand Down Expand Up @@ -135,7 +135,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' },
{"ram-size", required_argument, 0, 'z' },
{"ram-size", required_argument, 0, 'z' },
{"disable-compressed", no_argument, 0, 'C' },
{"disable-writable-misa", no_argument, 0, 'I' },
{"disable-fdext", no_argument, 0, 'F' },
Expand All @@ -146,7 +146,7 @@ static struct option options[] = {
{"report-arch", no_argument, 0, 'a' },
{"test-signature", required_argument, 0, 'T' },
{"signature-granularity", required_argument, 0, 'g' },
{"enable-zpm", no_argument, 0, OPT_ENABLE_ZJPM },
{"enable-zpm", no_argument, 0, OPT_ENABLE_ZPM },
#ifdef RVFI_DII
{"rvfi-dii", required_argument, 0, 'r' },
#endif
Expand Down Expand Up @@ -290,7 +290,7 @@ static int process_args(int argc, char **argv)
"t:"
"T:"
"g:"
"h"
"h"
#ifdef RVFI_DII
"r:"
#endif
Expand Down Expand Up @@ -346,10 +346,10 @@ static int process_args(int argc, char **argv)
fprintf(stderr, "enabling N extension.\n");
rv_enable_next = true;
break;
case OPT_ENABLE_ZJPM:
case OPT_ENABLE_ZPM:
fprintf(stderr, "enabling pointer masking support.\n");
rv_enable_zpm = true;
break;
break;
case 'I':
fprintf(stderr, "disabling writable misa CSR.\n");
rv_enable_writable_misa = false;
Expand Down
2 changes: 1 addition & 1 deletion handwritten_support/riscv_extras.lem
View file
Original file line number Diff line number Diff line change
Expand Up @@ -259,4 +259,4 @@ val print_bits : string -> bitvector -> unit
let print_bits msg bs = print_endline (msg ^ (show_bitlist (bits_of bs)))

val print_dbg : string -> unit
let print_dbg msg = ()
let print_dbg msg = ()
10 changes: 5 additions & 5 deletions model/riscv_insts_aext.sail
View file
Original file line number Diff line number Diff line change
Expand Up @@ -113,7 +113,7 @@ mapping clause encdec = STORECON(aq, rl, rs2, rs1, size, rd)

/* NOTE: Currently, we only EA if address translation is successful. This may need revisiting. */
function clause execute (STORECON(aq, rl, rs2, rs1, width, rd)) = {
let pmm = is_pmm_active();
let pmm = is_pmm_active();
let width_bytes = size_bytes(width);

// This is checked during decoding.
Expand All @@ -134,7 +134,7 @@ function clause execute (STORECON(aq, rl, rs2, rs1, width, rd)) = {
match ext_data_get_addr(rs1, zeros(), Write(Data), width_bytes) {
Ext_DataAddr_Error(e) => { ext_handle_data_check_error(e); RETIRE_FAIL },
Ext_DataAddr_OK(vaddr) => {
let vaddr_ = transform_effective_address(vaddr, pmm);
let vaddr_ = transform_effective_address(vaddr, pmm);
if not(is_aligned(vaddr_, width))
then { handle_mem_exception(vaddr_, E_SAMO_Addr_Align()); RETIRE_FAIL }
else {
Expand Down Expand Up @@ -195,7 +195,7 @@ mapping clause encdec = AMO(op, aq, rl, rs2, rs1, size, rd)
/* NOTE: Currently, we only EA if address translation is successful.
This may need revisiting. */
function clause execute (AMO(op, aq, rl, rs2, rs1, width, rd)) = {
let pmm = is_pmm_active();
let pmm = is_pmm_active();
let 'width_bytes = size_bytes(width);

// This is checked during decoding.
Expand All @@ -207,7 +207,7 @@ function clause execute (AMO(op, aq, rl, rs2, rs1, width, rd)) = {
match ext_data_get_addr(rs1, zeros(), ReadWrite(Data, Data), width_bytes) {
Ext_DataAddr_Error(e) => { ext_handle_data_check_error(e); RETIRE_FAIL },
Ext_DataAddr_OK(vaddr) => {
let vaddr_ = transform_effective_address(vaddr, pmm);
let vaddr_ = transform_effective_address(vaddr, pmm);
if not(is_aligned(vaddr_, width))
then { handle_mem_exception(vaddr_, E_SAMO_Addr_Align()); RETIRE_FAIL }
else match translateAddr(vaddr_, ReadWrite(Data, Data)) {
Expand Down Expand Up @@ -261,4 +261,4 @@ mapping amo_mnemonic : amoop <-> string = {
}

mapping clause assembly = AMO(op, aq, rl, rs2, rs1, width, rd)
<-> amo_mnemonic(op) ^ "." ^ size_mnemonic(width) ^ maybe_aq(aq) ^ maybe_rl(rl) ^ spc() ^ reg_name(rd) ^ sep() ^ reg_name(rs2) ^ sep() ^ "(" ^ reg_name(rs1) ^ ")"
<-> amo_mnemonic(op) ^ "." ^ size_mnemonic(width) ^ maybe_aq(aq) ^ maybe_rl(rl) ^ spc() ^ reg_name(rd) ^ sep() ^ reg_name(rs2) ^ sep() ^ "(" ^ reg_name(rs1) ^ ")"
55 changes: 12 additions & 43 deletions model/riscv_insts_base.sail
View file
Original file line number Diff line number Diff line change
Expand Up @@ -320,57 +320,26 @@ function is_aligned(vaddr : xlenbits, width : word_width) -> bool =
function check_misaligned(vaddr : xlenbits, width : word_width) -> bool =
not(plat_enable_misaligned_access()) & not(is_aligned(vaddr, width))

function transform_VA (effective_address : xlenbits,pmlen : {7, 16}) -> xlenbits = {
let XLEN = sizeof(xlen);
let i = XLEN -(pmlen +1);
let effective_bit = effective_address[i..i];
let masked_bits = replicate_bits(effective_bit, pmlen);
let unmasked_bits = effective_address[i..0];
masked_bits @ unmasked_bits
function transform_VA (effective_address : xlenbits, pmlen : {7, 16}) -> xlenbits = {
sign_extend(effective_address[sizeof(xlen) - pmlen - 1 .. 0])
}

function transform_PA (effective_address : xlenbits,pmlen : {7, 16}) -> xlenbits = {
let XLEN = sizeof(xlen);
let i = XLEN -(pmlen +1);
let masked_bits = replicate_bits(0b0, pmlen);
let unmasked_bits = effective_address[i..0];
masked_bits @ unmasked_bits
function transform_PA (effective_address : xlenbits, pmlen : {7, 16}) -> xlenbits = {
zero_extend(effective_address[sizeof(xlen) - pmlen - 1 .. 0])
}

function transform_effective_address(vaddr : xlenbits, pmm : bool) -> xlenbits = {
if pmm then {
let pmm_bits = get_pmm();
let mode = translationMode(cur_privilege);
match (mode) {
(Sbare) => {
match (pmm_bits){
(0b10) => transform_PA (vaddr,7),
(0b11) => transform_PA (vaddr,16),
}
},
(Sv39) => {
match (pmm_bits){
(0b10) => transform_VA (vaddr,7),
(0b11) => transform_VA (vaddr,16),
}
},
(Sv48) => {
match (pmm_bits){
(0b10) => transform_VA (vaddr,7),
(0b11) => transform_VA (vaddr,16),
}
},
(Sv57) => {
match (pmm_bits){
(0b10) => transform_VA (vaddr,7),
(0b11) => transform_VA (vaddr,16),
}
},
match pmm_bits {
pmm_mode(Enabled7) => if mode == Sbare then transform_PA(vaddr, 7) else transform_VA(vaddr, 7),
pmm_mode(Enabled16) => if mode == Sbare then transform_PA(vaddr, 16) else transform_VA(vaddr, 16),
}
}
else {
vaddr //PMM is not active
}
}
else {
vaddr
}
}

function clause execute(LOAD(imm, rs1, rd, is_unsigned, width, aq, rl)) = {
Expand Down Expand Up @@ -790,4 +759,4 @@ function clause execute SFENCE_VMA(rs1, rs2) = {
}

mapping clause assembly = SFENCE_VMA(rs1, rs2)
<-> "sfence.vma" ^ spc() ^ reg_name(rs1) ^ sep() ^ reg_name(rs2)
<-> "sfence.vma" ^ spc() ^ reg_name(rs1) ^ sep() ^ reg_name(rs2)
14 changes: 7 additions & 7 deletions model/riscv_insts_vext_mem.sail
View file
Original file line number Diff line number Diff line change
Expand Up @@ -137,7 +137,7 @@ mapping clause encdec = VLSEGFFTYPE(nf, vm, rs1, width, vd) if extensionEnabled(

val process_vlsegff : forall 'f 'b 'n 'p, (0 < 'f & 'f <= 8) & ('b in {1, 2, 4, 8}) & ('n >= 0). (int('f), bits(1), regidx, int('b), regidx, int('p), int('n)) -> Retired
function process_vlsegff (nf, vm, vd, load_width_bytes, rs1, EMUL_pow, num_elem) = {
let pmm = is_pmm_active();
let pmm = is_pmm_active();
let EMUL_reg : int = if EMUL_pow <= 0 then 1 else 2 ^ (EMUL_pow);
let width_type : word_width = size_bytes(load_width_bytes);
let vm_val : vector('n, dec, bool) = read_vmask(num_elem, vm, 0b00000);
Expand All @@ -162,7 +162,7 @@ function process_vlsegff (nf, vm, vd, load_width_bytes, rs1, EMUL_pow, num_elem)
}
},
Ext_DataAddr_OK(vaddr) => {
let vaddr_ = transform_effective_address(vaddr, pmm) in
let vaddr_ = transform_effective_address(vaddr, pmm) in
if check_misaligned(vaddr_, width_type) then {
if i == 0 then { handle_mem_exception(vaddr_, E_Load_Addr_Align()); return RETIRE_FAIL }
else {
Expand Down Expand Up @@ -244,7 +244,7 @@ mapping clause encdec = VSSEGTYPE(nf, vm, rs1, width, vs3) if extensionEnabled(E

val process_vsseg : forall 'f 'b 'n 'p, (0 < 'f & 'f <= 8) & ('b in {1, 2, 4, 8}) & ('n >= 0). (int('f), bits(1), regidx, int('b), regidx, int('p), int('n)) -> Retired
function process_vsseg (nf, vm, vs3, load_width_bytes, rs1, EMUL_pow, num_elem) = {
let pmm = is_pmm_active();
let pmm = is_pmm_active();
let EMUL_reg : int = if EMUL_pow <= 0 then 1 else 2 ^ (EMUL_pow);
let width_type : word_width = size_bytes(load_width_bytes);
let vm_val : vector('n, dec, bool) = read_vmask(num_elem, vm, 0b00000);
Expand Down Expand Up @@ -457,7 +457,7 @@ mapping clause encdec = VLUXSEGTYPE(nf, vm, vs2, rs1, width, vd) if extensionEna
val process_vlxseg : forall 'f 'ib 'db 'ip 'dp 'n, (0 < 'f & 'f <= 8) & ('ib in {1, 2, 4, 8}) & ('db in {1, 2, 4, 8}) & ('n >= 0). (int('f), bits(1), regidx, int('ib), int('db), int('ip), int('dp), regidx, regidx, int('n), int) -> Retired
function process_vlxseg (nf, vm, vd, EEW_index_bytes, EEW_data_bytes, EMUL_index_pow, EMUL_data_pow, rs1, vs2, num_elem, mop) = {
let pmm = is_pmm_active();
let EMUL_reg : int = if EMUL_pow <= 0 then 1 else 2 ^ (EMUL_pow);
let EMUL_data_reg : int = if EMUL_data_pow <= 0 then 1 else 2 ^ (EMUL_data_pow);
let width_type : word_width = size_bytes(EEW_data_bytes);
let vm_val : vector('n, dec, bool) = read_vmask(num_elem, vm, 0b00000);
let vd_seg : vector('n, dec, bits('f * 'db * 8)) = read_vreg_seg(num_elem, EEW_data_bytes * 8, EMUL_data_pow, nf, vd);
Expand Down Expand Up @@ -551,7 +551,7 @@ mapping clause encdec = VSUXSEGTYPE(nf, vm, vs2, rs1, width, vs3) if extensionEn
val process_vsxseg : forall 'f 'ib 'db 'ip 'dp 'n, (0 < 'f & 'f <= 8) & ('ib in {1, 2, 4, 8}) & ('db in {1, 2, 4, 8}) & ('n >= 0). (int('f), bits(1), regidx, int('ib), int('db), int('ip), int('dp), regidx, regidx, int('n), int) -> Retired
function process_vsxseg (nf, vm, vs3, EEW_index_bytes, EEW_data_bytes, EMUL_index_pow, EMUL_data_pow, rs1, vs2, num_elem, mop) = {
let pmm = is_pmm_active();
let EMUL_reg : int = if EMUL_pow <= 0 then 1 else 2 ^ (EMUL_pow);
let EMUL_data_reg : int = if EMUL_data_pow <= 0 then 1 else 2 ^ (EMUL_data_pow);
let width_type : word_width = size_bytes(EEW_data_bytes);
let vm_val : vector('n, dec, bool) = read_vmask(num_elem, vm, 0b00000);
let vs3_seg : vector('n, dec, bits('f * 'db * 8)) = read_vreg_seg(num_elem, EEW_data_bytes * 8, EMUL_data_pow, nf, vs3);
Expand All @@ -567,7 +567,7 @@ function process_vsxseg (nf, vm, vs3, EEW_index_bytes, EEW_data_bytes, EMUL_inde
match ext_data_get_addr(rs1, to_bits(sizeof(xlen), elem_offset), Write(Data), EEW_data_bytes) {
Ext_DataAddr_Error(e) => { ext_handle_data_check_error(e); return RETIRE_FAIL },
Ext_DataAddr_OK(vaddr) =>
let vaddr_ = transform_effective_address(vaddr, pmm) in
let vaddr_ = transform_effective_address(vaddr, pmm) in
if check_misaligned(vaddr_, width_type)
then { handle_mem_exception(vaddr_, E_SAMO_Addr_Align()); return RETIRE_FAIL }
else match translateAddr(vaddr_, Write(Data)) {
Expand Down Expand Up @@ -840,7 +840,7 @@ mapping clause encdec = VMTYPE(rs1, vd_or_vs3, op) if extensionEnabled(Ext_V)

val process_vm : forall 'n 'l, ('n >= 0 & 'l >= 0). (regidx, regidx, int('n), int('l), vmlsop) -> Retired
function process_vm(vd_or_vs3, rs1, num_elem, evl, op) = {
let pmm = is_pmm_active();
let pmm = is_pmm_active();
let width_type : word_width = BYTE;
let start_element = get_start_element();
let vd_or_vs3_val : vector('n, dec, bits(8)) = read_vreg(num_elem, 8, 0, vd_or_vs3);
Expand Down
42 changes: 25 additions & 17 deletions model/riscv_sys_regs.sail
View file
Original file line number Diff line number Diff line change
Expand Up @@ -96,7 +96,7 @@ val sys_enable_next = pure {c: "sys_enable_next", ocaml: "Platform.enable_next",
supervisor mode is implemented and non-bare addressing modes are supported. */
val sys_enable_writable_fiom = pure {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 = pure {c: "sys_enable_pmm", ocaml: "Platform.enable_pmm", _: "sys_enable_pmm"} : unit -> bool
val sys_enable_zpm = pure {c: "sys_enable_zpm", ocaml: "Platform.enable_zpm", _: "sys_enable_zpm"} : unit -> bool
/* How many PMP entries are implemented. This must be 0, 16 or 64 (this is checked at runtime). */
val sys_pmp_count = pure {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 @@ -756,6 +756,21 @@ function read_seed_csr() -> xlenbits = {
/* Writes to the seed CSR are ignored */
function write_seed_csr () -> option(xlenbits) = None()

/* Pointer Masking Different modes */
enum PointerMaskingMode = {
Disabled, // Pointer Masking Disabled
Reserved, // Reserved Encoding for Pointer Masking
Enabled7, // Pointer Masking Enabled with PMM = 7
Enabled16, // Pointer Masking Enabled with PMM = 16
}

mapping pmm_mode : PointerMaskingMode <-> bits(2) = {
Disabled <-> 0b00,
Reserved <-> 0b01,
Enabled7 <-> 0b10,
Enabled16 <-> 0b11,
}

/* mseccfg is a XLEN-bit read/write register that controls */
/* security features */
bitfield MSeccfg : bits(64) = {
Expand Down Expand Up @@ -824,7 +839,7 @@ register senvcfg : SEnvcfg
function legalize_mseccfg(o : MSeccfg, v : bits(64)) -> MSeccfg = {
let v = Mk_MSeccfg(v);
// Update PMM field only if Pointer Masking is enabled and Written value is legal
let o = [o with PMM = if (sys_enable_zpm() & (sizeof(xlen) != 32) & (v[PMM] != 0b01)) then v[PMM] else o[PMM]];
let o = [o with PMM = if (sys_enable_zpm() & (sizeof(xlen) != 32) & (v[PMM] != pmm_mode(Reserved))) then v[PMM] else o[PMM]];
// Other extensions are not implemented yet so all other fields are read only zero.
o
}
Expand All @@ -833,7 +848,7 @@ function legalize_menvcfg(o : MEnvcfg, v : bits(64)) -> MEnvcfg = {
let v = Mk_MEnvcfg(v);
let o = [o with FIOM = 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 = [o with PMM = if (sys_enable_zpm() & (sizeof(xlen) != 32) & (v[PMM] != 0b01)) then v[PMM] else o[PMM]];
let o = [o with PMM = if (sys_enable_zpm() & (sizeof(xlen) != 32) & (v[PMM] != pmm_mode(Reserved))) then v[PMM] else o[PMM]];
// Other extensions are not implemented yet so all other fields are read only zero.
o
}
Expand All @@ -842,7 +857,7 @@ function legalize_senvcfg(o : SEnvcfg, v : bits(64)) -> SEnvcfg = {
let v = Mk_SEnvcfg(v);
let o = [o with FIOM = 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 = [o with PMM = if (sys_enable_zpm() & (sizeof(xlen) != 32) & (v[PMM] != 0b01)) then v[PMM] else o[PMM]];
let o = [o with PMM = if (sys_enable_zpm() & (sizeof(xlen) != 32) & (v[PMM] != pmm_mode(Reserved))) then v[PMM] else o[PMM]];
// Other extensions are not implemented yet so all other fields are read only zero.
o
}
Expand All @@ -858,16 +873,6 @@ function is_fiom_active() -> bool = {
}
}

// 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)),
}
}

/* vector csrs */
register vstart : bits(16) /* use the largest possible length of vstart */
register vxsat : bits(1)
Expand All @@ -886,13 +891,16 @@ bitfield Vtype : xlenbits = {
register vtype : Vtype

//Returns the PMM bits value depends on the Privilege mode
function get_pmm() -> bits(2) = {
function get_pmm() -> bits(2) =
match cur_privilege {
Machine => mseccfg[PMM],
Supervisor => menvcfg[PMM],
User => if extensionEnabled(Ext_S) then senvcfg[PMM] else menvcfg[PMM],
User => if extensionEnabled(Ext_S) then senvcfg[PMM] else menvcfg[PMM],
}
}

// 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 = get_pmm() != zeros(2)

/* the dynamic selected element width (SEW) */
/* this returns the power of 2 for SEW */
Expand Down

0 comments on commit 0245007

Please sign in to comment.