From 99196870adbf3acea0f85ca16e5538e627d789e9 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 | 6 ++-- model/riscv_insts_base.sail | 4 +-- 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, 142 insertions(+), 51 deletions(-) diff --git a/c_emulator/riscv_platform.c b/c_emulator/riscv_platform.c index 6544de65c..927d36707 100644 --- a/c_emulator/riscv_platform.c +++ b/c_emulator/riscv_platform.c @@ -82,6 +82,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 4a53d12ac..669d82e47 100644 --- a/c_emulator/riscv_platform.h +++ b/c_emulator/riscv_platform.h @@ -9,6 +9,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 449bb1df7..6c799d78f 100644 --- a/c_emulator/riscv_platform_impl.c +++ b/c_emulator/riscv_platform_impl.c @@ -18,6 +18,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 d377c9c43..9c1d2d303 100644 --- a/c_emulator/riscv_platform_impl.h +++ b/c_emulator/riscv_platform_impl.h @@ -22,6 +22,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 bf68da282..a58368cf9 100644 --- a/c_emulator/riscv_sim.c +++ b/c_emulator/riscv_sim.c @@ -53,6 +53,8 @@ const char *RV32ISA = "RV32IMAC"; #define OPT_ENABLE_WRITABLE_FIOM 1001 #define OPT_PMP_COUNT 1002 #define OPT_PMP_GRAIN 1003 +#define OPT_ENABLE_SVNAPOT 1004 +#define OPT_ENABLE_SVPBMT 1005 #define OPT_ENABLE_ZCB 10014 static bool do_dump_dts = false; @@ -150,6 +152,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 } }; @@ -406,6 +410,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 9c9e06a4f..64305e264 100644 --- a/model/riscv_fetch.sail +++ b/model/riscv_fetch.sail @@ -24,7 +24,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. @@ -42,7 +42,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 0f4da8372..031d980ac 100644 --- a/model/riscv_insts_aext.sail +++ b/model/riscv_insts_aext.sail @@ -85,7 +85,7 @@ 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 (width, sizeof(xlen)) { (BYTE, _) => process_loadres(rd, vaddr, mem_read(Read(Data), addr, 1, aq, aq & rl, true), false), (HALF, _) => process_loadres(rd, vaddr, mem_read(Read(Data), addr, 2, aq, aq & rl, true), false), @@ -149,7 +149,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 : MemoryOpResult(unit) = match (width, sizeof(xlen)) { (BYTE, _) => mem_write_ea(addr, 1, aq & rl, rl, true), (HALF, _) => mem_write_ea(addr, 2, aq & rl, rl, true), @@ -221,7 +221,7 @@ function clause execute (AMO(op, aq, rl, rs2, rs1, width, rd)) = { Ext_DataAddr_OK(vaddr) => { match translateAddr(vaddr, ReadWrite(Data, Data)) { TR_Failure(e, _) => { handle_mem_exception(vaddr, e); RETIRE_FAIL }, - TR_Address(addr, _) => { + TR_Address(addr, _, _) => { let eares : MemoryOpResult(unit) = match (width, sizeof(xlen)) { (BYTE, _) => mem_write_ea(addr, 1, aq & rl, rl, true), (HALF, _) => mem_write_ea(addr, 2, aq & rl, rl, true), diff --git a/model/riscv_insts_base.sail b/model/riscv_insts_base.sail index 9c4630b33..ecf51dc95 100644 --- a/model/riscv_insts_base.sail +++ b/model/riscv_insts_base.sail @@ -333,7 +333,7 @@ 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 (width) { BYTE => process_load(rd, vaddr, mem_read(Read(Data), paddr, 1, aq, rl, false), is_unsigned), @@ -389,7 +389,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 : MemoryOpResult(unit) = match width { BYTE => mem_write_ea(paddr, 1, aq, rl, false), HALF => mem_write_ea(paddr, 2, aq, rl, false), diff --git a/model/riscv_insts_fext.sail b/model/riscv_insts_fext.sail index e4afb30d5..e8f715cb3 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 ce9cd6237..8763ee93e 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 3e198b43e..f5b7beac0 100644 --- a/model/riscv_sys_regs.sail +++ b/model/riscv_sys_regs.sail @@ -103,6 +103,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. */ @@ -162,6 +168,12 @@ function haveZmmul() -> bool = true /* 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() + bitfield Mstatush : bits(32) = { MBE : 5, SBE : 4 @@ -809,6 +821,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 2d1e5d162..8e7388b42 100644 --- a/model/riscv_vmem.sail +++ b/model/riscv_vmem.sail @@ -116,7 +116,9 @@ function pt_walk(sv_params, MemException(_) => PTW_Failure(PTW_Access(), ext_ptw), MemValue(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); @@ -136,7 +138,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 { @@ -148,7 +149,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 { @@ -159,9 +163,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) } } @@ -262,8 +273,8 @@ function translationMode(priv : Privilege) -> SATPMode = { // 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) } @@ -281,7 +292,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]); @@ -293,7 +304,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 @@ -316,7 +327,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) } } } @@ -331,7 +342,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); @@ -346,7 +357,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 @@ -368,7 +379,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) @@ -389,7 +400,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); @@ -407,7 +418,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); @@ -416,7 +427,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), @@ -437,7 +448,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 dfe032c0d..420f03ed2 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 2f0aaaf7c..bbce1271a 100644 --- a/ocaml_emulator/platform.ml +++ b/ocaml_emulator/platform.ml @@ -15,7 +15,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 @@ -92,6 +93,8 @@ let mtval_has_illegal_inst_bits () = !config_mtval_has_illegal_inst_bits 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 8dad8a45a..e873fcee7 100644 --- a/ocaml_emulator/riscv_ocaml_sim.ml +++ b/ocaml_emulator/riscv_ocaml_sim.ml @@ -85,7 +85,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:"