From 75d7b42f391c4e44486e9dc3112ce64bf4514f83 Mon Sep 17 00:00:00 2001 From: Ved Shanbhogue Date: Sat, 20 Jan 2024 15:40:22 -0600 Subject: [PATCH] Add Svnapot and Svpbmt extensions --- c_emulator/riscv_platform.c | 10 +++++++ c_emulator/riscv_platform.h | 2 ++ c_emulator/riscv_platform_impl.c | 2 ++ c_emulator/riscv_platform_impl.h | 2 ++ c_emulator/riscv_sim.c | 12 +++++++++ model/riscv_fetch.sail | 4 +-- model/riscv_fetch_rvfi.sail | 4 +-- model/riscv_insts_aext.sail | 8 +++--- model/riscv_insts_base.sail | 9 +++---- model/riscv_insts_fext.sail | 4 +-- model/riscv_insts_vext_mem.sail | 26 +++++++++--------- model/riscv_sys_regs.sail | 17 +++++++++++- model/riscv_vmem.sail | 40 ++++++++++++++++------------ model/riscv_vmem_pte.sail | 44 ++++++++++++++++++++++++++----- ocaml_emulator/platform.ml | 5 +++- ocaml_emulator/riscv_ocaml_sim.ml | 8 +++++- 16 files changed, 142 insertions(+), 55 deletions(-) diff --git a/c_emulator/riscv_platform.c b/c_emulator/riscv_platform.c index 644cb1e8d..037b1b9d3 100644 --- a/c_emulator/riscv_platform.c +++ b/c_emulator/riscv_platform.c @@ -92,6 +92,16 @@ bool plat_mtval_has_illegal_inst_bits(unit u) return rv_mtval_has_illegal_inst_bits; } +bool sys_enable_svnapot(unit u) +{ + return rv_enable_svnapot; +} + +bool sys_enable_svpbmt(unit u) +{ + return rv_enable_svpbmt; +} + 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 450a64eba..37d4e3950 100644 --- a/c_emulator/riscv_platform.h +++ b/c_emulator/riscv_platform.h @@ -11,6 +11,8 @@ bool sys_enable_writable_misa(unit); bool sys_enable_writable_fiom(unit); bool sys_enable_vext(unit); bool sys_enable_bext(unit); +bool sys_enable_svnapot(unit); +bool sys_enable_svpbmt(unit); uint64_t sys_pmp_count(unit); uint64_t sys_pmp_grain(unit); diff --git a/c_emulator/riscv_platform_impl.c b/c_emulator/riscv_platform_impl.c index cad634ef2..43fa9c3fa 100644 --- a/c_emulator/riscv_platform_impl.c +++ b/c_emulator/riscv_platform_impl.c @@ -20,6 +20,8 @@ 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_svnapot = false; +bool rv_enable_svpbmt = false; uint64_t rv_ram_base = UINT64_C(0x80000000); uint64_t rv_ram_size = UINT64_C(0x4000000); diff --git a/c_emulator/riscv_platform_impl.h b/c_emulator/riscv_platform_impl.h index 111090d39..1fd3c8edd 100644 --- a/c_emulator/riscv_platform_impl.h +++ b/c_emulator/riscv_platform_impl.h @@ -24,6 +24,8 @@ 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_svnapot; +extern bool rv_enable_svpbmt; extern uint64_t rv_ram_base; extern uint64_t rv_ram_size; diff --git a/c_emulator/riscv_sim.c b/c_emulator/riscv_sim.c index 913543144..18638e7bd 100644 --- a/c_emulator/riscv_sim.c +++ b/c_emulator/riscv_sim.c @@ -56,6 +56,8 @@ enum { OPT_PMP_GRAIN, OPT_ENABLE_SVINVAL, OPT_ENABLE_ZCB, + OPT_ENABLE_SVNAPOT, + OPT_ENABLE_SVPBMT, }; static bool do_dump_dts = false; @@ -154,6 +156,8 @@ static struct option options[] = { #ifdef SAILCOV {"sailcov-file", required_argument, 0, 'c' }, #endif + {"enable-svnapot", no_argument, 0, OPT_ENABLE_SVNAPOT }, + {"enable-svpbmt", no_argument, 0, OPT_ENABLE_SVPBMT }, {0, 0, 0, 0 } }; @@ -415,6 +419,14 @@ static int process_args(int argc, char **argv) trace_log_path = optarg; fprintf(stderr, "using %s for trace output.\n", trace_log_path); break; + case OPT_ENABLE_SVNAPOT: + fprintf(stderr, "enabling Svnapot extension.\n"); + rv_enable_svnapot = true; + break; + case OPT_ENABLE_SVPBMT: + fprintf(stderr, "enabling Svpbmt extension.\n"); + rv_enable_svpbmt = true; + break; case '?': print_usage(argv[0], 1); break; diff --git a/model/riscv_fetch.sail b/model/riscv_fetch.sail index 6fd66917d..4bcb0a966 100644 --- a/model/riscv_fetch.sail +++ b/model/riscv_fetch.sail @@ -23,7 +23,7 @@ function fetch() -> FetchResult = then F_Error(E_Fetch_Addr_Align(), PC) else match translateAddr(use_pc, Execute()) { TR_Failure(e, _) => F_Error(e, PC), - TR_Address(ppclo, _) => { + 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. @@ -41,7 +41,7 @@ function fetch() -> FetchResult = Ext_FetchAddr_OK(use_pc_hi) => { match translateAddr(use_pc_hi, Execute()) { TR_Failure(e, _) => F_Error(e, PC_hi), - TR_Address(ppchi, _) => { + TR_Address(ppchi, _, _) => { match mem_read(Execute(), ppchi, 2, false, false, false) { MemException(e) => F_Error(e, PC_hi), MemValue(ihi) => F_Base(append(ihi, ilo)) diff --git a/model/riscv_fetch_rvfi.sail b/model/riscv_fetch_rvfi.sail index d25237572..6b0dcf514 100644 --- a/model/riscv_fetch_rvfi.sail +++ b/model/riscv_fetch_rvfi.sail @@ -21,7 +21,7 @@ function fetch() -> FetchResult = { then F_Error(E_Fetch_Addr_Align(), PC) else match translateAddr(use_pc, Execute()) { TR_Failure(e, _) => F_Error(e, PC), - TR_Address(_, _) => { + TR_Address(_, _, _) => { let i = rvfi_instruction[rvfi_insn]; rvfi_inst_data->rvfi_insn() = zero_extend(i); if (i[1 .. 0] != 0b11) @@ -34,7 +34,7 @@ function fetch() -> FetchResult = { Ext_FetchAddr_OK(use_pc_hi) => match translateAddr(use_pc_hi, Execute()) { TR_Failure(e, _) => F_Error(e, PC), - TR_Address(_, _) => F_Base(i) + TR_Address(_, _, _) => F_Base(i) } } } diff --git a/model/riscv_insts_aext.sail b/model/riscv_insts_aext.sail index 3bf44b8f5..55833bb55 100644 --- a/model/riscv_insts_aext.sail +++ b/model/riscv_insts_aext.sail @@ -72,11 +72,11 @@ function clause execute(LOADRES(aq, rl, rs1, width, rd)) = { 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(addr, _) => + TR_Address(addr, _, _) => match mem_read(Read(Data), addr, width_bytes, aq, aq & rl, true) { MemValue(result) => { load_reservation(vaddr); X(rd) = sign_extend(result); RETIRE_SUCCESS }, MemException(e) => { handle_mem_exception(vaddr, e); RETIRE_FAIL } - }, + } } } } @@ -123,7 +123,7 @@ function clause execute (STORECON(aq, rl, rs2, rs1, width, rd)) = { match translateAddr(vaddr, Write(Data)) { /* 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, _) => { + TR_Address(addr, _, _) => { let eares = mem_write_ea(addr, width_bytes, aq & rl, rl, true); match (eares) { MemException(e) => { handle_mem_exception(vaddr, e); RETIRE_FAIL }, @@ -184,7 +184,7 @@ function clause execute (AMO(op, aq, rl, rs2, rs1, width, rd)) = { then { handle_mem_exception(vaddr, E_SAMO_Addr_Align()); RETIRE_FAIL } else match translateAddr(vaddr, ReadWrite(Data, Data)) { TR_Failure(e, _) => { handle_mem_exception(vaddr, e); RETIRE_FAIL }, - TR_Address(addr, _) => { + TR_Address(addr, _, _) => { let eares = mem_write_ea(addr, width_bytes, aq & rl, rl, true); let rs2_val = X(rs2)[width_bytes * 8 - 1 .. 0]; match (eares) { diff --git a/model/riscv_insts_base.sail b/model/riscv_insts_base.sail index 26915f22c..7ff755831 100644 --- a/model/riscv_insts_base.sail +++ b/model/riscv_insts_base.sail @@ -331,14 +331,13 @@ function clause execute(LOAD(imm, rs1, rd, is_unsigned, width, aq, rl)) = { 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, _) => - + TR_Address(paddr, _, _) => match mem_read(Read(Data), paddr, width_bytes, aq, rl, false) { MemValue(result) => { X(rd) = extend_value(is_unsigned, result); RETIRE_SUCCESS }, MemException(e) => { handle_mem_exception(vaddr, e); RETIRE_FAIL }, - }, + } } - }, + } } } @@ -387,7 +386,7 @@ function clause execute (STORE(imm, rs2, rs1, width, aq, rl)) = { 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, _) => { + TR_Address(paddr, _, _) => { let eares = mem_write_ea(paddr, width_bytes, aq, rl, false); match (eares) { MemException(e) => { handle_mem_exception(vaddr, e); RETIRE_FAIL }, diff --git a/model/riscv_insts_fext.sail b/model/riscv_insts_fext.sail index 5c89e9188..41eb92640 100644 --- a/model/riscv_insts_fext.sail +++ b/model/riscv_insts_fext.sail @@ -322,7 +322,7 @@ function clause execute(LOAD_FP(imm, rs1, rd, 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(addr, _) => { + TR_Address(addr, _, _) => { let (aq, rl, res) = (false, false, false); match (width) { BYTE => { handle_illegal(); RETIRE_FAIL }, @@ -388,7 +388,7 @@ function clause execute (STORE_FP(imm, rs2, rs1, 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, _) => { + TR_Address(addr, _, _) => { let eares : MemoryOpResult(unit) = match width { BYTE => MemValue () /* bogus placeholder for illegal size */, HALF => mem_write_ea(addr, 2, aq, rl, false), diff --git a/model/riscv_insts_vext_mem.sail b/model/riscv_insts_vext_mem.sail index 4da82e18f..91df902e9 100644 --- a/model/riscv_insts_vext_mem.sail +++ b/model/riscv_insts_vext_mem.sail @@ -88,7 +88,7 @@ function process_vlseg (nf, vm, vd, load_width_bytes, rs1, EMUL_pow, num_elem) = then { handle_mem_exception(vaddr, E_Load_Addr_Align()); return RETIRE_FAIL } else match translateAddr(vaddr, Read(Data)) { TR_Failure(e, _) => { handle_mem_exception(vaddr, e); return RETIRE_FAIL }, - TR_Address(paddr, _) => { + TR_Address(paddr, _, _) => { match mem_read(Read(Data), paddr, load_width_bytes, false, false, false) { MemValue(elem) => write_single_element(load_width_bytes * 8, i, vd + to_bits(5, j * EMUL_reg), elem), MemException(e) => { handle_mem_exception(vaddr, e); return RETIRE_FAIL } @@ -175,7 +175,7 @@ function process_vlsegff (nf, vm, vd, load_width_bytes, rs1, EMUL_pow, num_elem) trimmed = true } }, - TR_Address(paddr, _) => { + TR_Address(paddr, _, _) => { match mem_read(Read(Data), paddr, load_width_bytes, false, false, false) { MemValue(elem) => write_single_element(load_width_bytes * 8, i, vd + to_bits(5, j * EMUL_reg), elem), MemException(e) => { @@ -258,7 +258,7 @@ function process_vsseg (nf, vm, vs3, load_width_bytes, rs1, EMUL_pow, num_elem) then { handle_mem_exception(vaddr, E_SAMO_Addr_Align()); return RETIRE_FAIL } else match translateAddr(vaddr, Write(Data)) { TR_Failure(e, _) => { handle_mem_exception(vaddr, e); return RETIRE_FAIL }, - TR_Address(paddr, _) => { + TR_Address(paddr, _, _) => { let eares : MemoryOpResult(unit) = mem_write_ea(paddr, load_width_bytes, false, false, false); match (eares) { MemException(e) => { handle_mem_exception(vaddr, e); return RETIRE_FAIL }, @@ -329,7 +329,7 @@ function process_vlsseg (nf, vm, vd, load_width_bytes, rs1, rs2, EMUL_pow, num_e then { handle_mem_exception(vaddr, E_Load_Addr_Align()); return RETIRE_FAIL } else match translateAddr(vaddr, Read(Data)) { TR_Failure(e, _) => { handle_mem_exception(vaddr, e); return RETIRE_FAIL }, - TR_Address(paddr, _) => { + TR_Address(paddr, _, _) => { match mem_read(Read(Data), paddr, load_width_bytes, false, false, false) { MemValue(elem) => write_single_element(load_width_bytes * 8, i, vd + to_bits(5, j * EMUL_reg), elem), MemException(e) => { handle_mem_exception(vaddr, e); return RETIRE_FAIL } @@ -395,7 +395,7 @@ function process_vssseg (nf, vm, vs3, load_width_bytes, rs1, rs2, EMUL_pow, num_ then { handle_mem_exception(vaddr, E_SAMO_Addr_Align()); return RETIRE_FAIL } else match translateAddr(vaddr, Write(Data)) { TR_Failure(e, _) => { handle_mem_exception(vaddr, e); return RETIRE_FAIL }, - TR_Address(paddr, _) => { + TR_Address(paddr, _, _) => { let eares : MemoryOpResult(unit) = mem_write_ea(paddr, load_width_bytes, false, false, false); match (eares) { MemException(e) => { handle_mem_exception(vaddr, e); return RETIRE_FAIL }, @@ -467,7 +467,7 @@ function process_vlxseg (nf, vm, vd, EEW_index_bytes, EEW_data_bytes, EMUL_index then { handle_mem_exception(vaddr, E_Load_Addr_Align()); return RETIRE_FAIL } else match translateAddr(vaddr, Read(Data)) { TR_Failure(e, _) => { handle_mem_exception(vaddr, e); return RETIRE_FAIL }, - TR_Address(paddr, _) => { + TR_Address(paddr, _, _) => { match mem_read(Read(Data), paddr, EEW_data_bytes, false, false, false) { MemValue(elem) => write_single_element(EEW_data_bytes * 8, i, vd + to_bits(5, j * EMUL_data_reg), elem), MemException(e) => { handle_mem_exception(vaddr, e); return RETIRE_FAIL } @@ -558,7 +558,7 @@ function process_vsxseg (nf, vm, vs3, EEW_index_bytes, EEW_data_bytes, EMUL_inde then { handle_mem_exception(vaddr, E_SAMO_Addr_Align()); return RETIRE_FAIL } else match translateAddr(vaddr, Write(Data)) { TR_Failure(e, _) => { handle_mem_exception(vaddr, e); return RETIRE_FAIL }, - TR_Address(paddr, _) => { + TR_Address(paddr, _, _) => { let eares : MemoryOpResult(unit) = mem_write_ea(paddr, EEW_data_bytes, false, false, false); match (eares) { MemException(e) => { handle_mem_exception(vaddr, e); return RETIRE_FAIL }, @@ -651,7 +651,7 @@ function process_vlre (nf, vd, load_width_bytes, rs1, elem_per_reg) = { then { handle_mem_exception(vaddr, E_Load_Addr_Align()); return RETIRE_FAIL } else match translateAddr(vaddr, Read(Data)) { TR_Failure(e, _) => { handle_mem_exception(vaddr, e); return RETIRE_FAIL }, - TR_Address(paddr, _) => { + TR_Address(paddr, _, _) => { match mem_read(Read(Data), paddr, load_width_bytes, false, false, false) { MemValue(elem) => write_single_element(load_width_bytes * 8, i, vd + to_bits(5, cur_field), elem), MemException(e) => { handle_mem_exception(vaddr, e); return RETIRE_FAIL } @@ -675,7 +675,7 @@ function process_vlre (nf, vd, load_width_bytes, rs1, elem_per_reg) = { then { handle_mem_exception(vaddr, E_Load_Addr_Align()); return RETIRE_FAIL } else match translateAddr(vaddr, Read(Data)) { TR_Failure(e, _) => { handle_mem_exception(vaddr, e); return RETIRE_FAIL }, - TR_Address(paddr, _) => { + TR_Address(paddr, _, _) => { match mem_read(Read(Data), paddr, load_width_bytes, false, false, false) { MemValue(elem) => write_single_element(load_width_bytes * 8, i, vd + to_bits(5, j), elem), MemException(e) => { handle_mem_exception(vaddr, e); return RETIRE_FAIL } @@ -733,7 +733,7 @@ function process_vsre (nf, load_width_bytes, rs1, vs3, elem_per_reg) = { then { handle_mem_exception(vaddr, E_SAMO_Addr_Align()); return RETIRE_FAIL } else match translateAddr(vaddr, Write(Data)) { TR_Failure(e, _) => { handle_mem_exception(vaddr, e); return RETIRE_FAIL }, - TR_Address(paddr, _) => { + TR_Address(paddr, _, _) => { let eares : MemoryOpResult(unit) = mem_write_ea(paddr, load_width_bytes, false, false, false); match (eares) { MemException(e) => { handle_mem_exception(vaddr, e); return RETIRE_FAIL }, @@ -767,7 +767,7 @@ function process_vsre (nf, load_width_bytes, rs1, vs3, elem_per_reg) = { then { handle_mem_exception(vaddr, E_SAMO_Addr_Align()); return RETIRE_FAIL } else match translateAddr(vaddr, Write(Data)) { TR_Failure(e, _) => { handle_mem_exception(vaddr, e); return RETIRE_FAIL }, - TR_Address(paddr, _) => { + TR_Address(paddr, _, _) => { let eares : MemoryOpResult(unit) = mem_write_ea(paddr, load_width_bytes, false, false, false); match (eares) { MemException(e) => { handle_mem_exception(vaddr, e); return RETIRE_FAIL }, @@ -835,7 +835,7 @@ function process_vm(vd_or_vs3, rs1, num_elem, evl, op) = { then { handle_mem_exception(vaddr, E_Load_Addr_Align()); return RETIRE_FAIL } else match translateAddr(vaddr, Read(Data)) { TR_Failure(e, _) => { handle_mem_exception(vaddr, e); return RETIRE_FAIL }, - TR_Address(paddr, _) => { + TR_Address(paddr, _, _) => { match mem_read(Read(Data), paddr, 1, false, false, false) { MemValue(elem) => write_single_element(8, i, vd_or_vs3, elem), MemException(e) => { handle_mem_exception(vaddr, e); return RETIRE_FAIL } @@ -851,7 +851,7 @@ function process_vm(vd_or_vs3, rs1, num_elem, evl, op) = { then { handle_mem_exception(vaddr, E_SAMO_Addr_Align()); return RETIRE_FAIL } else match translateAddr(vaddr, Write(Data)) { TR_Failure(e, _) => { handle_mem_exception(vaddr, e); return RETIRE_FAIL }, - TR_Address(paddr, _) => { + TR_Address(paddr, _, _) => { let eares : MemoryOpResult(unit) = mem_write_ea(paddr, 1, false, false, false); match (eares) { MemException(e) => { handle_mem_exception(vaddr, e); return RETIRE_FAIL }, diff --git a/model/riscv_sys_regs.sail b/model/riscv_sys_regs.sail index 66b601049..b7c2e1495 100644 --- a/model/riscv_sys_regs.sail +++ b/model/riscv_sys_regs.sail @@ -108,6 +108,12 @@ val sys_enable_vext = {c: "sys_enable_vext", ocaml: "Platform.enable_vext", _: " /* whether misa.b was enabled at boot */ val sys_enable_bext = {c: "sys_enable_bext", ocaml: "Platform.enable_bext", _: "sys_enable_bext"} : unit -> bool +/* whether svnapot was enabled at boot */ +val sys_enable_svnapot = {c: "sys_enable_svnapot", ocaml: "Platform.enable_svnapot", _: "sys_enable_svnapot"} : unit -> bool + +/* whether svpbmt was enabled at boot */ +val sys_enable_svpbmt = {c: "sys_enable_svpbmt", ocaml: "Platform.enable_svpbmt", _: "sys_enable_svpbmt"} : unit -> bool + /* This function allows an extension to veto a write to Misa if it would violate an alignment restriction on unsetting C. If it returns true the write will have no effect. */ @@ -172,6 +178,12 @@ function haveZalrsc() -> bool = haveAtomics() /* Zicond extension support */ function haveZicond() -> bool = true +/* Svpbmt extension support */ +function haveSvpbmt() -> bool = sys_enable_svpbmt() + +/* Svnapot extension support */ +function haveSvnapot() -> bool = sys_enable_svnapot() + /* * Illegal values legalized to least privileged mode supported. * Note: the only valid combinations of supported modes are M, M+U, M+S+U. @@ -840,7 +852,10 @@ register senvcfg : SEnvcfg 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]; + let o = [o with + FIOM = if sys_enable_writable_fiom() then v[FIOM] else 0b0, + PBMTE = if haveSvpbmt() then v[PBMTE] else 0b0 + ]; // Other extensions are not implemented yet so all other fields are read only zero. o } diff --git a/model/riscv_vmem.sail b/model/riscv_vmem.sail index 2bb96fe7a..d76609932 100644 --- a/model/riscv_vmem.sail +++ b/model/riscv_vmem.sail @@ -119,7 +119,9 @@ function pt_walk(sv_params, let pte : bits(64) = zero_extend(pte); let pte_flags = Mk_PTE_Flags(pte[7 .. 0]); - if pte_is_invalid(pte_flags) then + let ext_pte = msbs_of_PTE(sv_params, pte); + let ext_pte_flags = Mk_PTE_Ext_Flags(ext_pte); + if pte_is_invalid(pte_flags, ext_pte_flags, level) then PTW_Failure(PTW_Invalid_PTE(), ext_ptw) else { let ppns : bits(64) = PPNs_of_PTE(sv_params, pte); @@ -139,7 +141,6 @@ function pt_walk(sv_params, } else { // Leaf PTE - let ext_pte = msbs_of_PTE(sv_params, pte); let pte_check = check_PTE_permission(ac, priv, mxr, do_sum, pte_flags, ext_pte, ext_ptw); match pte_check { @@ -162,9 +163,14 @@ function pt_walk(sv_params, let pa = (ppn << pagesize_bits) | zero_extend(offset_of_va(va)); PTW_Success(pa, pte, pte_addr, level, global', ext_ptw) } - } - else { - let pa = (ppns << pagesize_bits) | zero_extend(offset_of_va(va)); + } else if (haveSvnapot() & ext_pte_flags[N] == 0b1 & ppns[3 .. 0] != 0b1000) then { + // Only 64K NAPOT PTEs are valid + PTW_Failure(PTW_Invalid_PTE(), ext_ptw) + } else { + let final_ppn : bits(64) = if haveSvnapot() & ext_pte_flags[N] == 0b1 + then ppns[63 .. 4] @ vpn_j[3 .. 0] + else ppns; + let pa = (final_ppn << pagesize_bits) | zero_extend(offset_of_va(va)); PTW_Success(pa, pte, pte_addr, level, global', ext_ptw) } } @@ -275,8 +281,8 @@ function write_pte forall 'n, 'n in {4, 8} . ( // Result of address translation // PUBLIC -union TR_Result('paddr : Type, 'failure : Type) = { - TR_Address : ('paddr, ext_ptw), +union TR_Result('paddr : Type, 'ext_pte_bits : Type, 'failure : Type) = { + TR_Address : ('paddr, 'ext_pte_bits, ext_ptw), TR_Failure : ('failure, ext_ptw) } @@ -294,7 +300,7 @@ function translate_TLB_hit(sv_params : SV_Params, ext_ptw : ext_ptw, tlb_index : nat, ent : TLB_Entry) - -> TR_Result(bits(64), PTW_Error) = { + -> TR_Result(bits(64), extPte, PTW_Error) = { let pte = ent.pte; let ext_pte = msbs_of_PTE(sv_params, pte); let pte_flags = Mk_PTE_Flags(pte[7 .. 0]); @@ -306,7 +312,7 @@ function translate_TLB_hit(sv_params : SV_Params, TR_Failure(ext_get_ptw_error(ext_ptw_fail), ext_ptw), PTE_Check_Success(ext_ptw) => match update_PTE_Bits(sv_params, pte, ac) { - None() => TR_Address(ent.pAddr | (vAddr & ent.vAddrMask), ext_ptw), + None() => TR_Address(ent.pAddr | (vAddr & ent.vAddrMask), ext_pte, ext_ptw), Some(pte') => // See riscv_platform.sail if not(plat_enable_dirty_update()) then @@ -323,7 +329,7 @@ function translate_TLB_hit(sv_params : SV_Params, MemException(e) => internal_error(__FILE__, __LINE__, "invalid physical address in TLB") }; - TR_Address(ent.pAddr | (vAddr & ent.vAddrMask), ext_ptw) + TR_Address(ent.pAddr | (vAddr & ent.vAddrMask), ext_pte, ext_ptw) } } } @@ -338,7 +344,7 @@ function translate_TLB_miss(sv_params : SV_Params, priv : Privilege, mxr : bool, do_sum : bool, - ext_ptw : ext_ptw) -> TR_Result(bits(64), PTW_Error) = { + ext_ptw : ext_ptw) -> TR_Result(bits(64), extPte, PTW_Error) = { let initial_level = sv_params.levels - 1; let ptw_result = pt_walk(sv_params, vAddr, ac, priv, mxr, do_sum, ptb, initial_level, false, ext_ptw); @@ -353,7 +359,7 @@ function translate_TLB_miss(sv_params : SV_Params, add_to_TLB(asid, vAddr, pAddr, pte, pteAddr, level, global, sv_params.vpn_size_bits, pagesize_bits); - TR_Address(pAddr, ext_ptw) + TR_Address(pAddr, ext_pte, ext_ptw) }, Some(pte') => // See riscv_platform.sail @@ -369,7 +375,7 @@ function translate_TLB_miss(sv_params : SV_Params, add_to_TLB(asid, vAddr, pAddr, pte', pteAddr, level, global, sv_params.vpn_size_bits, pagesize_bits); - TR_Address(pAddr, ext_ptw) + TR_Address(pAddr, ext_pte, ext_ptw) }, MemException(e) => TR_Failure(PTW_Access(), ext_ptw) @@ -390,7 +396,7 @@ function translate(sv_params : SV_Params, mxr : bool, do_sum : bool, ext_ptw : ext_ptw) - -> TR_Result(bits(64), PTW_Error) = { + -> TR_Result(bits(64), extPte, PTW_Error) = { let va_mask : bits(64) = zero_extend(ones(sv_params.va_size_bits)); let vAddr = (vAddr_arg & va_mask); @@ -408,7 +414,7 @@ function translate(sv_params : SV_Params, // PUBLIC: invoked from instr-fetch and load/store/amo function translateAddr(vAddr : xlenbits, ac : AccessType(ext_access_type)) - -> TR_Result(xlenbits, ExceptionType) = { + -> TR_Result(xlenbits, extPte, ExceptionType) = { // Internally the vmem code works with 64-bit values, whether xlen==32 or xlen==64 // This 'extend' is a no-op when xlen==64 and extends when xlen==32 let vAddr_64b : bits(64) = zero_extend(vAddr); @@ -417,7 +423,7 @@ function translateAddr(vAddr : xlenbits, let effPriv : Privilege = effectivePrivilege(ac, mstatus, cur_privilege); let mode : SATPMode = translationMode(effPriv); let (valid_va, sv_params) : (bool, SV_Params) = match mode { - Sbare => return TR_Address(vAddr, init_ext_ptw), + Sbare => return TR_Address(vAddr, zeros(), init_ext_ptw), Sv32 => (true, sv32_params), Sv39 => (is_valid_vAddr(sv39_params, vAddr_64b), sv39_params), Sv48 => (is_valid_vAddr(sv48_params, vAddr_64b), sv48_params), @@ -438,7 +444,7 @@ function translateAddr(vAddr : xlenbits, init_ext_ptw); // Fixup result PA or exception match tr_result1 { - TR_Address(pa, ext_ptw) => TR_Address(truncate(pa, sizeof(xlen)), ext_ptw), + TR_Address(pa, ext_pte, ext_ptw) => TR_Address(truncate(pa, sizeof(xlen)), ext_pte, ext_ptw), TR_Failure(f, ext_ptw) => TR_Failure(translationException(ac, f), ext_ptw) } } diff --git a/model/riscv_vmem_pte.sail b/model/riscv_vmem_pte.sail index 07a94a3ed..d16ed4084 100644 --- a/model/riscv_vmem_pte.sail +++ b/model/riscv_vmem_pte.sail @@ -19,13 +19,20 @@ type pte_flags_bits = bits(8) -// For PTW extensions (non-standard) -type extPte = bits(64) +// For PTW extensions (standard) +type extPte = bits(10) + +bitfield PTE_Ext_Flags : extPte = { + N : 9, + PBMT : 8 .. 7, + reserved : 6 .. 0 +} // PRIVATE: extract msbs of PTE above the PPN -function msbs_of_PTE(sv_params : SV_Params, pte : bits(64)) -> bits(64) = { +function msbs_of_PTE(sv_params : SV_Params, pte : bits(64)) -> bits(10) = { let mask : bits(64) = zero_extend(ones(sv_params.pte_msbs_size_bits)); - (pte >> sv_params.pte_msbs_lsb_index) & mask + let mbits: bits(64) = (pte >> sv_params.pte_msbs_lsb_index) & mask; + mbits[9 .. 0] } // PRIVATE: extract PPNs of PTE @@ -51,10 +58,33 @@ function pte_is_ptr(pte_flags : PTE_Flags) -> bool = (pte_flags[X] == 0b0) & (pte_flags[W] == 0b0) & (pte_flags[R] == 0b0) +// Extension hooks can request standard PTE validity checks by returning Ext_PTE_Std +enum Ext_isInvalPTE_Check = { + Ext_PTE_Invalid, + Ext_PTE_Valid, + Ext_PTE_Std +} + +// Extension hook to override standard definition of extended PTE attribute bits +function ext_pte_is_invalid (p : PTE_Flags, e : PTE_Ext_Flags) -> Ext_isInvalPTE_Check = + Ext_PTE_Std + // PRIVATE: check if a PTE is valid -function pte_is_invalid(pte_flags : PTE_Flags) -> bool = (pte_flags[V] == 0b0) - | ((pte_flags[W] == 0b1) - & (pte_flags[R] == 0b0)) +function pte_is_invalid(pte_flags : PTE_Flags, pte_ext_flags : PTE_Ext_Flags, level : PTW_Level) -> bool = { + match ext_pte_is_invalid(pte_flags, pte_ext_flags) { + Ext_PTE_Invalid => true, + Ext_PTE_Valid => false, + Ext_PTE_Std => { + pte_flags[V] == 0b0 + | pte_flags[W] == 0b1 & pte_flags[R] == 0b0 + | (pte_is_ptr(pte_flags) & (pte_flags[D] == 0b1 | pte_flags[A] == 0b1 | pte_flags[U] == 0b1)) + | pte_ext_flags[reserved] != zeros() + | pte_ext_flags[N] == 0b1 & (not(haveSvnapot()) | pte_is_ptr(pte_flags) | level > 0) + | pte_ext_flags[PBMT] == 0b11 + | (pte_ext_flags[PBMT] != 0b00 & (not(haveSvpbmt()) | pte_is_ptr(pte_flags) | menvcfg[PBMTE] == 0b0)) + } + } +} // ---------------- // Check access permissions in PTE diff --git a/ocaml_emulator/platform.ml b/ocaml_emulator/platform.ml index d10029a8b..83d60519e 100644 --- a/ocaml_emulator/platform.ml +++ b/ocaml_emulator/platform.ml @@ -17,7 +17,8 @@ let config_enable_vext = ref true let config_enable_bext = ref false let config_pmp_count = ref Big_int.zero let config_pmp_grain = ref Big_int.zero - +let config_enable_svnapot = ref false +let config_enable_svpbmt = 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 @@ -96,6 +97,8 @@ let enable_svinval () = !config_enable_svinval let enable_zcb () = !config_enable_zcb let enable_zfinx () = false let enable_writable_fiom () = !config_enable_writable_fiom +let enable_svnapot () = !config_enable_svnapot +let enable_svpbmt () = !config_enable_svpbmt let pmp_count () = !config_pmp_count let pmp_grain () = !config_pmp_grain diff --git a/ocaml_emulator/riscv_ocaml_sim.ml b/ocaml_emulator/riscv_ocaml_sim.ml index 344d1d272..ccbe808df 100644 --- a/ocaml_emulator/riscv_ocaml_sim.ml +++ b/ocaml_emulator/riscv_ocaml_sim.ml @@ -91,7 +91,13 @@ let options = Arg.align ([("-dump-dts", " requested isa"); ("-with-dtc", Arg.String PI.set_dtc, - " full path to dtc to use") + " full path to dtc to use"); + ("-enable-svnapot", + Arg.Set P.config_enable_svnapot, + " enable svnapot extension"); + ("-enable-svpbmt", + Arg.Set P.config_enable_svpbmt, + " enable svpbmt extension") ]) let usage_msg = "RISC-V platform options:"