From 3cadf656fb6cac35c7ad52c444e54d39446c76ed 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_pte.sail | 52 ++++++++++++++++++++++++------- model/riscv_sys_regs.sail | 13 ++++++++ model/riscv_vmem_common.sail | 4 +-- model/riscv_vmem_rv32.sail | 8 ++--- model/riscv_vmem_rv64.sail | 10 +++--- model/riscv_vmem_sv32.sail | 24 +++++++------- model/riscv_vmem_sv39.sail | 46 +++++++++++++++++---------- model/riscv_vmem_sv48.sail | 36 ++++++++++++++------- ocaml_emulator/platform.ml | 11 +++++++ ocaml_emulator/riscv_ocaml_sim.ml | 8 ++++- 21 files changed, 200 insertions(+), 88 deletions(-) diff --git a/c_emulator/riscv_platform.c b/c_emulator/riscv_platform.c index 253da353f..d593a3d6e 100644 --- a/c_emulator/riscv_platform.c +++ b/c_emulator/riscv_platform.c @@ -77,6 +77,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 38fac2f07..4f635b83c 100644 --- a/c_emulator/riscv_platform.h +++ b/c_emulator/riscv_platform.h @@ -8,6 +8,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 c2ae256ef..4e36d0fb1 100644 --- a/c_emulator/riscv_platform_impl.c +++ b/c_emulator/riscv_platform_impl.c @@ -17,6 +17,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 e3e4a9678..88d9d5458 100644 --- a/c_emulator/riscv_platform_impl.h +++ b/c_emulator/riscv_platform_impl.h @@ -21,6 +21,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 0094e9ad9..d1bc67f57 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 static bool do_dump_dts = false; static bool do_show_times = false; @@ -148,6 +150,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 } }; @@ -400,6 +404,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 e72f91270..03efd2589 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 caea73a4b..f3a9fc9b1 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 942fbaf69..d0023db4a 100644 --- a/model/riscv_insts_vext_mem.sail +++ b/model/riscv_insts_vext_mem.sail @@ -95,7 +95,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 } @@ -182,7 +182,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) => { @@ -265,7 +265,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 }, @@ -336,7 +336,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 } @@ -402,7 +402,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 }, @@ -474,7 +474,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 } @@ -565,7 +565,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 }, @@ -658,7 +658,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 } @@ -682,7 +682,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 } @@ -740,7 +740,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 }, @@ -774,7 +774,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 }, @@ -842,7 +842,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 } @@ -858,7 +858,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_pte.sail b/model/riscv_pte.sail index 1a5bb0ecc..516a31a5f 100644 --- a/model/riscv_pte.sail +++ b/model/riscv_pte.sail @@ -8,12 +8,27 @@ /* PTE attributes, permission checks and updates */ + +/* 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 +} + type pteAttribs = bits(8) -/* Reserved PTE bits could be used by extensions on RV64. There are +/* Reserved PTE bits could be used by standard extensions on RV64. There are * no such available bits on RV32, so these bits will be zeros on RV32. */ -type extPte = bits(10) +type pteStdExtAttribs = bits(10) + +bitfield PTE_StdExt_Bits : pteStdExtAttribs = { + N : 9, + PBMT : 8 .. 7, + RSVD : 6 .. 0 +} /* * On SV32, there are no reserved bits available to extensions. Therefore, by @@ -22,9 +37,9 @@ type extPte = bits(10) * those PTEs. To avoid the need for "inhibit" bits in extensions (i.e., so * that extensions can use the more common and more RISC-V flavored "enable" * disposition), we allow extensions to use any constant value by overriding - * this default_sv32_ext_pte value. + * this default_sv32_pte_std_ext_attribs value. */ -let default_sv32_ext_pte : extPte = zeros() +let default_sv32_pte_std_ext_attribs : pteStdExtAttribs = zeros() bitfield PTE_Bits : pteAttribs = { D : 7, @@ -37,14 +52,29 @@ bitfield PTE_Bits : pteAttribs = { V : 0 } -function isPTEPtr(p : pteAttribs, ext : extPte) -> bool = { +function ext_isInvalidPTE (p : pteAttribs, std_ext : pteStdExtAttribs) -> Ext_isInvalPTE_Check = + Ext_PTE_Std() + +function isPTEPtr(p : pteAttribs, std_ext : pteStdExtAttribs) -> bool = { let a = Mk_PTE_Bits(p); a[R] == 0b0 & a[W] == 0b0 & a[X] == 0b0 } -function isInvalidPTE(p : pteAttribs, ext : extPte) -> bool = { +function isInvalidPTE(p : pteAttribs, std_ext : pteStdExtAttribs) -> bool = { let a = Mk_PTE_Bits(p); - a[V] == 0b0 | (a[W] == 0b1 & a[R] == 0b0) + let e = Mk_PTE_StdExt_Bits(std_ext); + match ext_isInvalidPTE (p , std_ext) { + Ext_PTE_Invalid() => true, + Ext_PTE_Valid() => false, + Ext_PTE_Std() => { + a[V] == 0b0 | + (a[W] == 0b1 & a[R] == 0b0) | + (e[RSVD] != 0b0000000 | e[PBMT] == 0b11) | + (not(isPTEPtr(p, std_ext)) & (e[N] != 0b0 ) & (not(haveSvnapot()))) | + (not(isPTEPtr(p, std_ext)) & (e[PBMT] != 0b00) & (not(haveSvpbmt()) | menvcfg[PBMTE] == 0b0)) | + (isPTEPtr(p, std_ext) & (a[D] == 0b1 | a[A] == 0b1 | a[U] == 0b1 | e[N] != 0b0 | e[PBMT] != 0b00)) + } + } } union PTE_Check = { @@ -55,11 +85,11 @@ union PTE_Check = { function to_pte_check(b : bool) -> PTE_Check = if b then PTE_Check_Success(()) else PTE_Check_Failure((), ()) -/* For extensions: this function gets the extension-available bits of the PTE in extPte, +/* For extensions: this function gets the extension-available bits of the PTE in std_ext, * and the accumulated information of the page-table-walk in ext_ptw. It should return * the updated ext_ptw in both the success and failure cases. */ -function checkPTEPermission(ac : AccessType(ext_access_type), priv : Privilege, mxr : bool, do_sum : bool, p : PTE_Bits, ext : extPte, ext_ptw : ext_ptw) -> PTE_Check = { +function checkPTEPermission(ac : AccessType(ext_access_type), priv : Privilege, mxr : bool, do_sum : bool, p : PTE_Bits, std_ext : pteStdExtAttribs, ext_ptw : ext_ptw) -> PTE_Check = { match (ac, priv) { (Read(_), User) => to_pte_check(p[U] == 0b1 & (p[R] == 0b1 | (p[X] == 0b1 & mxr))), (Write(_), User) => to_pte_check(p[U] == 0b1 & p[W] == 0b1), @@ -75,7 +105,7 @@ function checkPTEPermission(ac : AccessType(ext_access_type), priv : Privilege, } } -function update_PTE_Bits(p : PTE_Bits, a : AccessType(ext_access_type), ext : extPte) -> option((PTE_Bits, extPte)) = { +function update_PTE_Bits(p : PTE_Bits, a : AccessType(ext_access_type), std_ext : pteStdExtAttribs) -> option((PTE_Bits, pteStdExtAttribs)) = { let update_d = p[D] == 0b0 & (match a { // dirty-bit Execute() => false, Read() => false, @@ -87,6 +117,6 @@ function update_PTE_Bits(p : PTE_Bits, a : AccessType(ext_access_type), ext : ex if update_d | update_a then { let np = update_A(p, 0b1); let np = if update_d then update_D(np, 0b1) else np; - Some(np, ext) + Some(np, std_ext) } else None() } diff --git a/model/riscv_sys_regs.sail b/model/riscv_sys_regs.sail index 4a5ab9205..80da6b2ce 100644 --- a/model/riscv_sys_regs.sail +++ b/model/riscv_sys_regs.sail @@ -101,6 +101,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. */ @@ -160,6 +166,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 @@ -804,6 +816,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_common.sail b/model/riscv_vmem_common.sail index 375dfa370..cfdbf3728 100644 --- a/model/riscv_vmem_common.sail +++ b/model/riscv_vmem_common.sail @@ -161,7 +161,7 @@ union PTW_Result('paddr : Type, 'pte : Type) = { /* Result of address translation */ -union TR_Result('paddr : Type, 'failure : Type) = { - TR_Address : ('paddr, ext_ptw), +union TR_Result('paddr : Type, 'std_ext_bits : Type, 'failure : Type) = { + TR_Address : ('paddr, 'std_ext_bits, ext_ptw), TR_Failure : ('failure, ext_ptw) } diff --git a/model/riscv_vmem_rv32.sail b/model/riscv_vmem_rv32.sail index 33cc9c123..ef0acdda5 100644 --- a/model/riscv_vmem_rv32.sail +++ b/model/riscv_vmem_rv32.sail @@ -34,7 +34,7 @@ function translationMode(priv) = { /* Top-level address translation dispatcher */ -val translateAddr_priv : (xlenbits, AccessType(ext_access_type), Privilege) -> TR_Result(xlenbits, ExceptionType) +val translateAddr_priv : (xlenbits, AccessType(ext_access_type), Privilege) -> TR_Result(xlenbits, pteStdExtAttribs, ExceptionType) function translateAddr_priv(vAddr, ac, effPriv) = { let mxr : bool = mstatus[MXR] == 0b1; let do_sum : bool = mstatus[SUM] == 0b1; @@ -47,16 +47,16 @@ function translateAddr_priv(vAddr, ac, effPriv) = { let ext_ptw : ext_ptw = init_ext_ptw; match mode { - Sbare => TR_Address(vAddr, ext_ptw), + Sbare => TR_Address(vAddr, zeros(), ext_ptw), Sv32 => match translate32(asid, ptb, vAddr, ac, effPriv, mxr, do_sum, SV32_LEVELS - 1, ext_ptw) { - TR_Address(pa, ext_ptw) => TR_Address(to_phys_addr(pa), ext_ptw), + TR_Address(pa, std_ext, ext_ptw) => TR_Address(to_phys_addr(pa), std_ext, ext_ptw), TR_Failure(f, ext_ptw) => TR_Failure(translationException(ac, f), ext_ptw) }, _ => internal_error(__FILE__, __LINE__, "unsupported address translation scheme") } } -val translateAddr : (xlenbits, AccessType(ext_access_type)) -> TR_Result(xlenbits, ExceptionType) +val translateAddr : (xlenbits, AccessType(ext_access_type)) -> TR_Result(xlenbits, pteStdExtAttribs, ExceptionType) function translateAddr(vAddr, ac) = translateAddr_priv(vAddr, ac, effectivePrivilege(ac, mstatus, cur_privilege)) diff --git a/model/riscv_vmem_rv64.sail b/model/riscv_vmem_rv64.sail index 9ead6425f..05e5f49f5 100644 --- a/model/riscv_vmem_rv64.sail +++ b/model/riscv_vmem_rv64.sail @@ -55,7 +55,7 @@ function translationMode(priv) = { /* Top-level address translation dispatcher */ -val translateAddr_priv : (xlenbits, AccessType(ext_access_type), Privilege) -> TR_Result(xlenbits, ExceptionType) +val translateAddr_priv : (xlenbits, AccessType(ext_access_type), Privilege) -> TR_Result(xlenbits, pteStdExtAttribs, ExceptionType) function translateAddr_priv(vAddr, ac, effPriv) = { let mxr : bool = mstatus[MXR] == 0b1; let do_sum : bool = mstatus[SUM] == 0b1; @@ -68,17 +68,17 @@ function translateAddr_priv(vAddr, ac, effPriv) = { let ext_ptw : ext_ptw = init_ext_ptw; match mode { - Sbare => TR_Address(vAddr, ext_ptw), + Sbare => TR_Address(vAddr, zeros(), ext_ptw), Sv39 => { if isValidSv39Addr(vAddr) then match translate39(asid, ptb, vAddr[38 .. 0], ac, effPriv, mxr, do_sum, SV39_LEVELS - 1, ext_ptw) { - TR_Address(pa, ext_ptw) => TR_Address(zero_extend(pa), ext_ptw), + TR_Address(pa, std_ext, ext_ptw) => TR_Address(zero_extend(pa), std_ext, ext_ptw), TR_Failure(f, ext_ptw) => TR_Failure(translationException(ac, f), ext_ptw) } else TR_Failure(translationException(ac, PTW_Invalid_Addr()), ext_ptw) }, Sv48 => { if isValidSv48Addr(vAddr) then match translate48(asid, ptb, vAddr[47 .. 0], ac, effPriv, mxr, do_sum, SV48_LEVELS - 1, ext_ptw) { - TR_Address(pa, ext_ptw) => TR_Address(zero_extend(pa), ext_ptw), + TR_Address(pa, std_ext, ext_ptw) => TR_Address(zero_extend(pa), std_ext, ext_ptw), TR_Failure(f, ext_ptw) => TR_Failure(translationException(ac, f), ext_ptw) } else TR_Failure(translationException(ac, PTW_Invalid_Addr()), ext_ptw) @@ -87,7 +87,7 @@ function translateAddr_priv(vAddr, ac, effPriv) = { } } -val translateAddr : (xlenbits, AccessType(ext_access_type)) -> TR_Result(xlenbits, ExceptionType) +val translateAddr : (xlenbits, AccessType(ext_access_type)) -> TR_Result(xlenbits, pteStdExtAttribs, ExceptionType) function translateAddr(vAddr, ac) = translateAddr_priv(vAddr, ac, effectivePrivilege(ac, mstatus, cur_privilege)) diff --git a/model/riscv_vmem_sv32.sail b/model/riscv_vmem_sv32.sail index 1de109c28..ebf414ec8 100644 --- a/model/riscv_vmem_sv32.sail +++ b/model/riscv_vmem_sv32.sail @@ -32,7 +32,7 @@ function walk32(vaddr, ac, priv, mxr, do_sum, ptb, level, global, ext_ptw) = { MemValue(v) => { let pte = Mk_SV32_PTE(v); let pbits = pte[BITS]; - let ext_pte : extPte = default_sv32_ext_pte; + let std_ext : pteStdExtAttribs = default_sv32_pte_std_ext_attribs; let pattr = Mk_PTE_Bits(pbits); let is_global = global | (pattr[G] == 0b1); /* print("walk32(vaddr=" ^ BitStr(vaddr) ^ " level=" ^ dec_str(level) @@ -40,11 +40,11 @@ function walk32(vaddr, ac, priv, mxr, do_sum, ptb, level, global, ext_ptw) = { ^ " pt_ofs=" ^ BitStr(to_phys_addr(pt_ofs)) ^ " pte_addr=" ^ BitStr(to_phys_addr(pte_addr)) ^ " pte=" ^ BitStr(v)); */ - if isInvalidPTE(pbits, ext_pte) then { + if isInvalidPTE(pbits, std_ext) then { /* print("walk32: invalid pte"); */ PTW_Failure(PTW_Invalid_PTE(), ext_ptw) } else { - if isPTEPtr(pbits, ext_pte) then { + if isPTEPtr(pbits, std_ext) then { if level > 0 then { /* walk down the pointer to the next level */ walk32(vaddr, ac, priv, mxr, do_sum, shiftl(zero_extend(pte[PPNi]), PAGESIZE_BITS), level - 1, is_global, ext_ptw) @@ -54,7 +54,7 @@ function walk32(vaddr, ac, priv, mxr, do_sum, ptb, level, global, ext_ptw) = { PTW_Failure(PTW_Invalid_PTE(), ext_ptw) } } else { /* leaf PTE */ - match checkPTEPermission(ac, priv, mxr, do_sum, pattr, ext_pte, ext_ptw) { + match checkPTEPermission(ac, priv, mxr, do_sum, pattr, std_ext, ext_ptw) { PTE_Check_Failure(ext_ptw, ext_ptw_fail) => { /* print("walk32: pte permission check failure"); */ PTW_Failure(ext_get_ptw_error(ext_ptw_fail), ext_ptw) @@ -123,19 +123,19 @@ function flush_TLB32(asid, addr) = /* address translation */ -val translate32 : (asid32, paddr32, vaddr32, AccessType(ext_access_type), Privilege, bool, bool, nat, ext_ptw) -> TR_Result(paddr32, PTW_Error) +val translate32 : (asid32, paddr32, vaddr32, AccessType(ext_access_type), Privilege, bool, bool, nat, ext_ptw) -> TR_Result(paddr32, pteStdExtAttribs, PTW_Error) function translate32(asid, ptb, vAddr, ac, priv, mxr, do_sum, level, ext_ptw) = { match lookup_TLB32(asid, vAddr) { Some(idx, ent) => { /* print("translate32: TLB32 hit for " ^ BitStr(vAddr)); */ let pte = Mk_SV32_PTE(ent.pte); - let ext_pte : extPte = zeros(); // no reserved bits for extensions + let std_ext : pteStdExtAttribs = zeros(); // no reserved bits for extensions let pteBits = Mk_PTE_Bits(pte[BITS]); - match checkPTEPermission(ac, priv, mxr, do_sum, pteBits, ext_pte, ext_ptw) { + match checkPTEPermission(ac, priv, mxr, do_sum, pteBits, std_ext, ext_ptw) { PTE_Check_Failure(ext_ptw, ext_ptw_fail) => { TR_Failure(ext_get_ptw_error(ext_ptw_fail), ext_ptw) }, PTE_Check_Success(ext_ptw) => { - match update_PTE_Bits(pteBits, ac, ext_pte) { - None() => TR_Address(ent.pAddr | zero_extend(vAddr & ent.vAddrMask), ext_ptw), + match update_PTE_Bits(pteBits, ac, std_ext) { + None() => TR_Address(ent.pAddr | zero_extend(vAddr & ent.vAddrMask), std_ext, ext_ptw), Some(pbits, ext) => { if not(plat_enable_dirty_update()) then { @@ -153,7 +153,7 @@ function translate32(asid, ptb, vAddr, ac, priv, mxr, do_sum, level, ext_ptw) = MemValue(_) => (), MemException(e) => internal_error(__FILE__, __LINE__, "invalid physical address in TLB") }; - TR_Address(ent.pAddr | zero_extend(vAddr & ent.vAddrMask), ext_ptw) + TR_Address(ent.pAddr | zero_extend(vAddr & ent.vAddrMask), std_ext, ext_ptw) } } } @@ -167,7 +167,7 @@ function translate32(asid, ptb, vAddr, ac, priv, mxr, do_sum, level, ext_ptw) = match update_PTE_Bits(Mk_PTE_Bits(pte[BITS]), ac, zeros()) { None() => { add_to_TLB32(asid, vAddr, pAddr, pte, pteAddr, level, global); - TR_Address(pAddr, ext_ptw) + TR_Address(pAddr, zeros(), ext_ptw) }, Some(pbits, ext) => if not(plat_enable_dirty_update()) @@ -180,7 +180,7 @@ function translate32(asid, ptb, vAddr, ac, priv, mxr, do_sum, level, ext_ptw) = match mem_write_value_priv(to_phys_addr(pteAddr), 4, w_pte.bits, Supervisor, false, false, false) { MemValue(_) => { add_to_TLB32(asid, vAddr, pAddr, w_pte, pteAddr, level, global); - TR_Address(pAddr, ext_ptw) + TR_Address(pAddr, zeros(), ext_ptw) }, MemException(e) => { /* pte is not in valid memory */ diff --git a/model/riscv_vmem_sv39.sail b/model/riscv_vmem_sv39.sail index 68f3d553c..857978d0c 100644 --- a/model/riscv_vmem_sv39.sail +++ b/model/riscv_vmem_sv39.sail @@ -26,19 +26,20 @@ function walk39(vaddr, ac, priv, mxr, do_sum, ptb, level, global, ext_ptw) = { MemValue(v) => { let pte = Mk_SV39_PTE(v); let pbits = pte[BITS]; - let ext_pte = pte[Ext]; + let std_ext : pteStdExtAttribs = pte[Ext]; let pattr = Mk_PTE_Bits(pbits); + let eattr = Mk_PTE_StdExt_Bits(std_ext); let is_global = global | (pattr[G] == 0b1); -/* print("walk39(vaddr=" ^ BitStr(vaddr) ^ " level=" ^ dec_str(level) +/* print("walk39(vaddr=" ^ BitStr(vaddr) ^ " level=" ^ string_of_int(level) ^ " pt_base=" ^ BitStr(ptb) ^ " pt_ofs=" ^ BitStr(pt_ofs) ^ " pte_addr=" ^ BitStr(pte_addr) ^ " pte=" ^ BitStr(v)); */ - if isInvalidPTE(pbits, ext_pte) then { + if isInvalidPTE(pbits, std_ext) then { /* print("walk39: invalid pte"); */ PTW_Failure(PTW_Invalid_PTE(), ext_ptw) } else { - if isPTEPtr(pbits, ext_pte) then { + if isPTEPtr(pbits, std_ext) then { if level > 0 then { /* walk down the pointer to the next level */ walk39(vaddr, ac, priv, mxr, do_sum, shiftl(zero_extend(pte[PPNi]), PAGESIZE_BITS), level - 1, is_global, ext_ptw) @@ -48,7 +49,7 @@ function walk39(vaddr, ac, priv, mxr, do_sum, ptb, level, global, ext_ptw) = { PTW_Failure(PTW_Invalid_PTE(), ext_ptw) } } else { /* leaf PTE */ - match checkPTEPermission(ac, priv, mxr, do_sum, pattr, ext_pte, ext_ptw) { + match checkPTEPermission(ac, priv, mxr, do_sum, pattr, std_ext, ext_ptw) { PTE_Check_Failure(ext_ptw, ext_ptw_fail) => { /* print("walk39: pte permission check failure"); */ PTW_Failure(ext_get_ptw_error(ext_ptw_fail), ext_ptw) @@ -57,7 +58,9 @@ function walk39(vaddr, ac, priv, mxr, do_sum, ptb, level, global, ext_ptw) = { if level > 0 then { /* superpage */ /* fixme hack: to get a mask of appropriate size */ let mask = shiftl(pte[PPNi] ^ pte[PPNi] ^ zero_extend(0b1), level * SV39_LEVEL_BITS) - 1; - if (pte[PPNi] & mask) != zero_extend(0b0) then { + if haveSvnapot() & eattr[N] == 0b1 then { + PTW_Failure(PTW_Invalid_PTE(), ext_ptw) + } else if (pte[PPNi] & mask) != zero_extend(0b0) then { /* misaligned superpage mapping */ /* print("walk39: misaligned superpage mapping"); */ PTW_Failure(PTW_Misaligned(), ext_ptw) @@ -71,9 +74,18 @@ function walk39(vaddr, ac, priv, mxr, do_sum, ptb, level, global, ext_ptw) = { } } else { /* normal leaf PTE */ -/* let res = append(pte[PPNi], va[PgOfs]); - print("walk39: pte.ppn=" ^ BitStr(pte[PPNi]) ^ " ppn=" ^ BitStr(pte[PPNi]) ^ " res=" ^ BitStr(res)); */ - PTW_Success(append(pte[PPNi], va[PgOfs]), pte, pte_addr, level, is_global, ext_ptw) + if ( haveSvnapot() & eattr[N] == 0b1 & pte.PPNi()[3 .. 0] != 0b1000 ) then { + PTW_Failure(PTW_Invalid_PTE(), ext_ptw) + } else { + let ppn : bits(44) = match (haveSvnapot(), eattr[N]) { + (false, _) => pte[PPNi], + (true, 0b0) => pte[PPNi], + (true, 0b1) => append(pte.PPNi()[43 .. 4], va.VPNi()[3 .. 0]) + }; +/* let res = append(ppn, va[PgOfs]); + print("walk39: pte.ppn=" ^ BitStr(pte[PPNi]) ^ " ppn=" ^ BitStr(ppn) ^ " res=" ^ BitStr(res)); */ + PTW_Success(append(ppn, va[PgOfs]), pte, pte_addr, level, is_global, ext_ptw) + } } } } @@ -117,19 +129,19 @@ function flush_TLB39(asid, addr) = /* address translation */ -val translate39 : (asid64, paddr64, vaddr39, AccessType(ext_access_type), Privilege, bool, bool, nat, ext_ptw) -> TR_Result(paddr64, PTW_Error) +val translate39 : (asid64, paddr64, vaddr39, AccessType(ext_access_type), Privilege, bool, bool, nat, ext_ptw) -> TR_Result(paddr64, pteStdExtAttribs, PTW_Error) function translate39(asid, ptb, vAddr, ac, priv, mxr, do_sum, level, ext_ptw) = { match lookup_TLB39(asid, vAddr) { Some(idx, ent) => { /* print("translate39: TLB39 hit for " ^ BitStr(vAddr)); */ let pte = Mk_SV39_PTE(ent.pte); - let ext_pte = pte[Ext]; + let std_ext : pteStdExtAttribs = pte[Ext]; let pteBits = Mk_PTE_Bits(pte[BITS]); - match checkPTEPermission(ac, priv, mxr, do_sum, pteBits, ext_pte, ext_ptw) { + match checkPTEPermission(ac, priv, mxr, do_sum, pteBits, std_ext, ext_ptw) { PTE_Check_Failure(ext_ptw, ext_ptw_fail) => { TR_Failure(ext_get_ptw_error(ext_ptw_fail), ext_ptw) }, PTE_Check_Success(ext_ptw) => { - match update_PTE_Bits(pteBits, ac, ext_pte) { - None() => TR_Address(ent.pAddr | zero_extend(vAddr & ent.vAddrMask), ext_ptw), + match update_PTE_Bits(pteBits, ac, std_ext) { + None() => TR_Address(ent.pAddr | zero_extend(vAddr & ent.vAddrMask), std_ext, ext_ptw), Some(pbits, ext) => { if not(plat_enable_dirty_update()) then { @@ -147,7 +159,7 @@ function translate39(asid, ptb, vAddr, ac, priv, mxr, do_sum, level, ext_ptw) = MemValue(_) => (), MemException(e) => internal_error(__FILE__, __LINE__, "invalid physical address in TLB") }; - TR_Address(ent.pAddr | zero_extend(vAddr & ent.vAddrMask), ext_ptw) + TR_Address(ent.pAddr | zero_extend(vAddr & ent.vAddrMask), std_ext, ext_ptw) } } } @@ -161,7 +173,7 @@ function translate39(asid, ptb, vAddr, ac, priv, mxr, do_sum, level, ext_ptw) = match update_PTE_Bits(Mk_PTE_Bits(pte[BITS]), ac, pte[Ext]) { None() => { add_to_TLB39(asid, vAddr, pAddr, pte, pteAddr, level, global); - TR_Address(pAddr, ext_ptw) + TR_Address(pAddr, pte[Ext], ext_ptw) }, Some(pbits, ext) => if not(plat_enable_dirty_update()) @@ -174,7 +186,7 @@ function translate39(asid, ptb, vAddr, ac, priv, mxr, do_sum, level, ext_ptw) = match mem_write_value_priv(zero_extend(pteAddr), 8, w_pte.bits, Supervisor, false, false, false) { MemValue(_) => { add_to_TLB39(asid, vAddr, pAddr, w_pte, pteAddr, level, global); - TR_Address(pAddr, ext_ptw) + TR_Address(pAddr, pte[Ext], ext_ptw) }, MemException(e) => { /* pte is not in valid memory */ diff --git a/model/riscv_vmem_sv48.sail b/model/riscv_vmem_sv48.sail index 517450aa0..45e6d2d46 100644 --- a/model/riscv_vmem_sv48.sail +++ b/model/riscv_vmem_sv48.sail @@ -26,19 +26,20 @@ function walk48(vaddr, ac, priv, mxr, do_sum, ptb, level, global, ext_ptw) = { MemValue(v) => { let pte = Mk_SV48_PTE(v); let pbits = pte[BITS]; - let ext_pte = pte[Ext]; + let std_ext : pteStdExtAttribs = pte[Ext]; let pattr = Mk_PTE_Bits(pbits); + let eattr = Mk_PTE_StdExt_Bits(std_ext); let is_global = global | (pattr[G] == 0b1); -/* print("walk48(vaddr=" ^ BitStr(vaddr) ^ " level=" ^ dec_str(level) +/* print("walk48(vaddr=" ^ BitStr(vaddr) ^ " level=" ^ string_of_int(level) ^ " pt_base=" ^ BitStr(ptb) ^ " pt_ofs=" ^ BitStr(pt_ofs) ^ " pte_addr=" ^ BitStr(pte_addr) ^ " pte=" ^ BitStr(v)); */ - if isInvalidPTE(pbits, ext_pte) then { + if isInvalidPTE(pbits, std_ext) then { /* print("walk48: invalid pte"); */ PTW_Failure(PTW_Invalid_PTE(), ext_ptw) } else { - if isPTEPtr(pbits, ext_pte) then { + if isPTEPtr(pbits, std_ext) then { if level > 0 then { /* walk down the pointer to the next level */ walk48(vaddr, ac, priv, mxr, do_sum, shiftl(zero_extend(pte[PPNi]), PAGESIZE_BITS), level - 1, is_global, ext_ptw) @@ -48,7 +49,7 @@ function walk48(vaddr, ac, priv, mxr, do_sum, ptb, level, global, ext_ptw) = { PTW_Failure(PTW_Invalid_PTE(), ext_ptw) } } else { /* leaf PTE */ - match checkPTEPermission(ac, priv, mxr, do_sum, pattr, ext_pte, ext_ptw) { + match checkPTEPermission(ac, priv, mxr, do_sum, pattr, std_ext, ext_ptw) { PTE_Check_Failure(ext_ptw, ext_ptw_fail) => { /* print("walk48: pte permission check failure"); */ PTW_Failure(ext_get_ptw_error(ext_ptw_fail), ext_ptw) @@ -57,7 +58,9 @@ function walk48(vaddr, ac, priv, mxr, do_sum, ptb, level, global, ext_ptw) = { if level > 0 then { /* superpage */ /* fixme hack: to get a mask of appropriate size */ let mask = shiftl(pte[PPNi] ^ pte[PPNi] ^ zero_extend(0b1), level * SV48_LEVEL_BITS) - 1; - if (pte[PPNi] & mask) != zero_extend(0b0) then { + if haveSvnapot() & eattr[N] == 0b1 then { + PTW_Failure(PTW_Invalid_PTE(), ext_ptw) + } else if (pte[PPNi] & mask) != zero_extend(0b0) then { /* misaligned superpage mapping */ /* print("walk48: misaligned superpage mapping"); */ PTW_Failure(PTW_Misaligned(), ext_ptw) @@ -71,9 +74,18 @@ function walk48(vaddr, ac, priv, mxr, do_sum, ptb, level, global, ext_ptw) = { } } else { /* normal leaf PTE */ -/* let res = append(pte[PPNi], va[PgOfs]); - print("walk48: pte.ppn=" ^ BitStr(pte[PPNi]) ^ " ppn=" ^ BitStr(pte[PPNi]) ^ " res=" ^ BitStr(res)); */ - PTW_Success(append(pte[PPNi], va[PgOfs]), pte, pte_addr, level, is_global, ext_ptw) + if ( haveSvnapot() & eattr[N] == 0b1 & pte.PPNi()[3 .. 0] != 0b1000 ) then { + PTW_Failure(PTW_Invalid_PTE(), ext_ptw) + } else { + let ppn : bits(44) = match (haveSvnapot(), eattr[N]) { + (false, _) => pte[PPNi], + (true, 0b0) => pte[PPNi], + (true, 0b1) => append(pte.PPNi()[43 .. 4], va.VPNi()[3 .. 0]) + }; +/* let res = append(ppn, va[PgOfs]); + print("walk48: pte.ppn=" ^ BitStr(pte[PPNi]) ^ " ppn=" ^ BitStr(ppn) ^ " res=" ^ BitStr(res)); */ + PTW_Success(append(ppn, va[PgOfs]), pte, pte_addr, level, is_global, ext_ptw) + } } } } @@ -117,7 +129,7 @@ function flush_TLB48(asid, addr) = /* address translation */ -val translate48 : (asid64, paddr64, vaddr48, AccessType(ext_access_type), Privilege, bool, bool, nat, ext_ptw) -> TR_Result(paddr64, PTW_Error) +val translate48 : (asid64, paddr64, vaddr48, AccessType(ext_access_type), Privilege, bool, bool, nat, ext_ptw) -> TR_Result(paddr64, pteStdExtAttribs, PTW_Error) function translate48(asid, ptb, vAddr, ac, priv, mxr, do_sum, level, ext_ptw) = { match walk48(vAddr, ac, priv, mxr, do_sum, ptb, level, false, ext_ptw) { PTW_Failure(f, ext_ptw) => TR_Failure(f, ext_ptw), @@ -125,7 +137,7 @@ function translate48(asid, ptb, vAddr, ac, priv, mxr, do_sum, level, ext_ptw) = match update_PTE_Bits(Mk_PTE_Bits(pte[BITS]), ac, pte[Ext]) { None() => { add_to_TLB48(asid, vAddr, pAddr, pte, pteAddr, level, global); - TR_Address(pAddr, ext_ptw) + TR_Address(pAddr, pte[Ext], ext_ptw) }, Some(pbits, ext) => if not(plat_enable_dirty_update()) @@ -138,7 +150,7 @@ function translate48(asid, ptb, vAddr, ac, priv, mxr, do_sum, level, ext_ptw) = match mem_write_value_priv(zero_extend(pteAddr), 8, w_pte.bits, Supervisor, false, false, false) { MemValue(_) => { add_to_TLB48(asid, vAddr, pAddr, w_pte, pteAddr, level, global); - TR_Address(pAddr, ext_ptw) + TR_Address(pAddr, pte[Ext], ext_ptw) }, MemException(e) => { /* pte is not in valid memory */ diff --git a/ocaml_emulator/platform.ml b/ocaml_emulator/platform.ml index a8bde44d6..e7051b01d 100644 --- a/ocaml_emulator/platform.ml +++ b/ocaml_emulator/platform.ml @@ -12,12 +12,19 @@ let config_enable_misaligned_access = ref false let config_mtval_has_illegal_inst_bits = ref false 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 +let config_enable_svnapot = ref false +let config_enable_svpbmt = ref false + let platform_arch = ref P.RV64 (* logging *) @@ -90,9 +97,13 @@ let enable_misaligned_access () = !config_enable_misaligned_access let mtval_has_illegal_inst_bits () = !config_mtval_has_illegal_inst_bits let enable_zfinx () = false let enable_writable_fiom () = !config_enable_writable_fiom + let pmp_count () = !config_pmp_count let pmp_grain () = !config_pmp_grain +let enable_svnapot () = !config_enable_svnapot +let enable_svpbmt () = !config_enable_svpbmt + let rom_base () = arch_bits_of_int64 P.rom_base let rom_size () = arch_bits_of_int !rom_size_ref diff --git a/ocaml_emulator/riscv_ocaml_sim.ml b/ocaml_emulator/riscv_ocaml_sim.ml index 03887b775..44d3b2c8b 100644 --- a/ocaml_emulator/riscv_ocaml_sim.ml +++ b/ocaml_emulator/riscv_ocaml_sim.ml @@ -82,7 +82,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:"