From 03b93503fea2cb719128c1f94a2c5dfba89e3f3e 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 | 13 +++++++++ model/riscv_vmem.sail | 47 +++++++++++++++++++------------ model/riscv_vmem_pte.sail | 44 ++++++++++++++++++++++++----- ocaml_emulator/platform.ml | 5 +++- ocaml_emulator/riscv_ocaml_sim.ml | 8 +++++- 16 files changed, 145 insertions(+), 55 deletions(-) diff --git a/c_emulator/riscv_platform.c b/c_emulator/riscv_platform.c index 2fdb63f92..01aab211b 100644 --- a/c_emulator/riscv_platform.c +++ b/c_emulator/riscv_platform.c @@ -87,6 +87,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 341bd5964..d923bced0 100644 --- a/c_emulator/riscv_platform.h +++ b/c_emulator/riscv_platform.h @@ -10,6 +10,8 @@ bool sys_enable_zfinx(unit); bool sys_enable_writable_misa(unit); bool sys_enable_writable_fiom(unit); bool sys_enable_vext(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 077fc50dc..ea06b61da 100644 --- a/c_emulator/riscv_platform_impl.c +++ b/c_emulator/riscv_platform_impl.c @@ -19,6 +19,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 c4289e679..3abe10bad 100644 --- a/c_emulator/riscv_platform_impl.h +++ b/c_emulator/riscv_platform_impl.h @@ -23,6 +23,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 3a9bfc08d..16e160c98 100644 --- a/c_emulator/riscv_sim.c +++ b/c_emulator/riscv_sim.c @@ -54,6 +54,8 @@ const char *RV32ISA = "RV32IMAC"; #define OPT_PMP_COUNT 1002 #define OPT_PMP_GRAIN 1003 #define OPT_ENABLE_SVINVAL 1004 +#define OPT_ENABLE_SVNAPOT 1006 +#define OPT_ENABLE_SVPBMT 1007 #define OPT_ENABLE_ZCB 10014 static bool do_dump_dts = false; @@ -152,6 +154,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 } }; @@ -408,6 +412,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 65d141923..3454926c6 100644 --- a/model/riscv_sys_regs.sail +++ b/model/riscv_sys_regs.sail @@ -105,6 +105,12 @@ val sys_pmp_grain = {c: "sys_pmp_grain", ocaml: "Platform.pmp_grain", _: "sys_pm /* whether misa.v was enabled at boot */ val sys_enable_vext = {c: "sys_enable_vext", ocaml: "Platform.enable_vext", _: "sys_enable_vext"} : 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. */ @@ -168,6 +174,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. @@ -837,6 +849,7 @@ 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 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..1b9b01d06 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) 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 { @@ -151,7 +152,10 @@ function pt_walk(sv_params, let mask_bits = level * sv_params.pte_PPN_j_size_bits; // Clear the lowest `mask_bits` bits. let ppns_masked = (ppns >> mask_bits) << mask_bits; - if not(ppns == ppns_masked) then + if haveSvnapot() & ext_pte_flags[N] == 0b1 then + // Superpage NAPOT PTEs are invalid + PTW_Failure(PTW_Invalid_PTE(), ext_ptw) + else if not(ppns == ppns_masked) then // misaligned superpage mapping PTW_Failure(PTW_Misaligned(), ext_ptw) else { @@ -162,9 +166,16 @@ 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) = match (haveSvnapot(), ext_pte_flags[N]) { + (false, _) => ppns, + (true, 0b0) => ppns, + (true, 0b1) => append(ppns[63 .. 4], vpn_j[3 .. 0]) + }; + let pa = (final_ppn << pagesize_bits) | zero_extend(offset_of_va(va)); PTW_Success(pa, pte, pte_addr, level, global', ext_ptw) } } @@ -275,8 +286,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 +305,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 +317,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 +334,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 +349,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 +364,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 +380,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 +401,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 +419,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 +428,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 +449,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..614409534 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, + RSVD : 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 +union Ext_isInvalPTE_Check = { + Ext_PTE_Invalid : unit, + Ext_PTE_Valid : unit, + Ext_PTE_Std : unit +} + +// 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) -> 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_ext_flags[RSVD] != 0b0000000 | pte_ext_flags[PBMT] == 0b11) | + (not(pte_is_ptr(pte_flags)) & (pte_ext_flags[N] != 0b0 ) & (not(haveSvnapot()))) | + (not(pte_is_ptr(pte_flags)) & (pte_ext_flags[PBMT] != 0b00) & (not(haveSvpbmt()) | menvcfg[PBMTE] == 0b0)) | + (pte_is_ptr(pte_flags) & (pte_flags[D] == 0b1 | pte_flags[A] == 0b1 | pte_flags[U] == 0b1 | + pte_ext_flags[N] != 0b0 | pte_ext_flags[PBMT] != 0b00)) + } + } +} // ---------------- // Check access permissions in PTE diff --git a/ocaml_emulator/platform.ml b/ocaml_emulator/platform.ml index 69f271496..3f947fa78 100644 --- a/ocaml_emulator/platform.ml +++ b/ocaml_emulator/platform.ml @@ -16,7 +16,8 @@ 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_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 @@ -94,6 +95,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 56be8d8a8..95a0496e2 100644 --- a/ocaml_emulator/riscv_ocaml_sim.ml +++ b/ocaml_emulator/riscv_ocaml_sim.ml @@ -88,7 +88,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:"