From 19ca9db7d7aac115fc27503cf8cb3e0d2b04de1c 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_insts_zicsr.sail | 8 ++--- model/riscv_pte.sail | 53 ++++++++++++++++++++++++-------- model/riscv_sys_regs.sail | 23 +++++++++++++- model/riscv_vmem_sv32.sail | 14 ++++----- model/riscv_vmem_sv39.sail | 34 +++++++++++++------- model/riscv_vmem_sv48.sail | 28 ++++++++++++----- 11 files changed, 145 insertions(+), 43 deletions(-) diff --git a/c_emulator/riscv_platform.c b/c_emulator/riscv_platform.c index fbd63fa88..f4831c60d 100644 --- a/c_emulator/riscv_platform.c +++ b/c_emulator/riscv_platform.c @@ -72,6 +72,16 @@ bool plat_enable_pmp(unit u) return rv_enable_pmp; } +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 4b6541f9c..2d6277dd4 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); bool plat_enable_dirty_update(unit); bool plat_enable_misaligned_access(unit); diff --git a/c_emulator/riscv_platform_impl.c b/c_emulator/riscv_platform_impl.c index 15ff8adf9..aa1191d0f 100644 --- a/c_emulator/riscv_platform_impl.c +++ b/c_emulator/riscv_platform_impl.c @@ -15,6 +15,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 e5c562af3..378f1d28e 100644 --- a/c_emulator/riscv_platform_impl.h +++ b/c_emulator/riscv_platform_impl.h @@ -19,6 +19,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 13d16534a..35a3ed67b 100644 --- a/c_emulator/riscv_sim.c +++ b/c_emulator/riscv_sim.c @@ -51,6 +51,8 @@ const char *RV32ISA = "RV32IMAC"; #define OPT_TRACE_OUTPUT 1000 #define OPT_ENABLE_WRITABLE_FIOM 1001 +#define OPT_ENABLE_SVNAPOT 1002 +#define OPT_ENABLE_SVPBMT 1003 static bool do_dump_dts = false; static bool do_show_times = false; @@ -145,6 +147,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 } }; @@ -381,6 +385,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_insts_zicsr.sail b/model/riscv_insts_zicsr.sail index 8953ad4b3..dfb024746 100644 --- a/model/riscv_insts_zicsr.sail +++ b/model/riscv_insts_zicsr.sail @@ -198,10 +198,10 @@ function writeCSR (csr : csreg, value : xlenbits) -> unit = { (0x304, _) => { mie = legalize_mie(mie, value); Some(mie.bits()) }, (0x305, _) => { Some(set_mtvec(value)) }, (0x306, _) => { mcounteren = legalize_mcounteren(mcounteren, value); Some(zero_extend(mcounteren.bits())) }, - (0x30A, 32) => { menvcfg = legalize_envcfg(menvcfg, menvcfg.bits()[63 .. 32] @ value); Some(menvcfg.bits()[31 .. 0]) }, - (0x30A, 64) => { menvcfg = legalize_envcfg(menvcfg, value); Some(menvcfg.bits()) }, + (0x30A, 32) => { menvcfg = legalize_menvcfg(menvcfg, menvcfg.bits()[63 .. 32] @ value); Some(menvcfg.bits()[31 .. 0]) }, + (0x30A, 64) => { menvcfg = legalize_menvcfg(menvcfg, value); Some(menvcfg.bits()) }, (0x310, 32) => { Some(mstatush.bits()) }, // ignore writes for now - (0x31A, 32) => { menvcfg = legalize_envcfg(menvcfg, value @ menvcfg.bits()[31 .. 0]); Some(menvcfg.bits()[63 .. 32]) }, + (0x31A, 32) => { menvcfg = legalize_menvcfg(menvcfg, value @ menvcfg.bits()[31 .. 0]); Some(menvcfg.bits()[63 .. 32]) }, (0x320, _) => { mcountinhibit = legalize_mcountinhibit(mcountinhibit, value); Some(zero_extend(mcountinhibit.bits())) }, (0x340, _) => { mscratch = value; Some(mscratch) }, (0x341, _) => { Some(set_xret_target(Machine, value)) }, @@ -248,7 +248,7 @@ function writeCSR (csr : csreg, value : xlenbits) -> unit = { (0x104, _) => { mie = legalize_sie(mie, mideleg, value); Some(mie.bits()) }, (0x105, _) => { Some(set_stvec(value)) }, (0x106, _) => { scounteren = legalize_scounteren(scounteren, value); Some(zero_extend(scounteren.bits())) }, - (0x10A, _) => { senvcfg = legalize_envcfg(senvcfg, zero_extend(value)); Some(senvcfg.bits()[sizeof(xlen) - 1 .. 0]) }, + (0x10A, _) => { senvcfg = legalize_senvcfg(senvcfg, zero_extend(value)); Some(senvcfg.bits()[sizeof(xlen) - 1 .. 0]) }, (0x140, _) => { sscratch = value; Some(sscratch) }, (0x141, _) => { Some(set_xret_target(Supervisor, value)) }, (0x142, _) => { scause->bits() = value; Some(scause.bits()) }, diff --git a/model/riscv_pte.sail b/model/riscv_pte.sail index 90345cc93..44c8d0c23 100644 --- a/model/riscv_pte.sail +++ b/model/riscv_pte.sail @@ -70,12 +70,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 @@ -84,9 +99,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, @@ -99,14 +114,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 = { @@ -117,11 +147,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), @@ -137,8 +167,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)) = { - let update_d = p.D() == 0b0 & (match a { // dirty-bit +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, Write(_) => true, @@ -149,6 +178,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 84f708e2f..a07c4fc1c 100644 --- a/model/riscv_sys_regs.sail +++ b/model/riscv_sys_regs.sail @@ -156,6 +156,12 @@ val sys_enable_writable_fiom = {c: "sys_enable_writable_fiom", ocaml: "Platform. /* 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. */ @@ -215,6 +221,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 @@ -865,7 +877,16 @@ bitfield Envcfg : bits(64) = { register menvcfg : Envcfg register senvcfg : Envcfg -function legalize_envcfg(o : Envcfg, v : bits(64)) -> Envcfg = { +function legalize_menvcfg(o : Envcfg, v : bits(64)) -> Envcfg = { + let v = Mk_Envcfg(v); + let o = update_FIOM(o, if sys_enable_writable_fiom() then v.FIOM() else 0b0); + // Svpbmt - PBMTE : PBMT enable + let o = update_PBMTE(o, if haveSvpbmt() then v.PBMTE() else 0b0); + // Other extensions are not implemented yet so all other fields are read only zero. + o +} + +function legalize_senvcfg(o : Envcfg, v : bits(64)) -> Envcfg = { let v = Mk_Envcfg(v); let o = update_FIOM(o, if sys_enable_writable_fiom() then v.FIOM() else 0b0); // Other extensions are not implemented yet so all other fields are read only zero. diff --git a/model/riscv_vmem_sv32.sail b/model/riscv_vmem_sv32.sail index 72def151a..a6b810b3b 100644 --- a/model/riscv_vmem_sv32.sail +++ b/model/riscv_vmem_sv32.sail @@ -94,7 +94,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=" ^ string_of_int(level) @@ -102,11 +102,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) @@ -116,7 +116,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) @@ -191,12 +191,12 @@ function translate32(asid, ptb, vAddr, ac, priv, mxr, do_sum, level, ext_ptw) = 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 = default_sv32_pte_std_ext_attribs; 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) { + match update_PTE_Bits(pteBits, ac, std_ext) { None() => TR_Address(ent.pAddr | zero_extend(vAddr & ent.vAddrMask), ext_ptw), Some(pbits, ext) => { if not(plat_enable_dirty_update()) diff --git a/model/riscv_vmem_sv39.sail b/model/riscv_vmem_sv39.sail index 25378a8dc..25c814487 100644 --- a/model/riscv_vmem_sv39.sail +++ b/model/riscv_vmem_sv39.sail @@ -88,19 +88,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 = 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=" ^ 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) @@ -110,7 +111,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) @@ -119,7 +120,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) @@ -133,9 +136,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) + } } } } @@ -185,12 +197,12 @@ function translate39(asid, ptb, vAddr, ac, priv, mxr, do_sum, level, ext_ptw) = 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 = 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) { + match update_PTE_Bits(pteBits, ac, std_ext) { None() => TR_Address(ent.pAddr | zero_extend(vAddr & ent.vAddrMask), ext_ptw), Some(pbits, ext) => { if not(plat_enable_dirty_update()) diff --git a/model/riscv_vmem_sv48.sail b/model/riscv_vmem_sv48.sail index 64c7a542a..3d8cc64ce 100644 --- a/model/riscv_vmem_sv48.sail +++ b/model/riscv_vmem_sv48.sail @@ -88,19 +88,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 = 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=" ^ 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) @@ -110,7 +111,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) @@ -119,7 +120,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) @@ -133,9 +136,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) + } } } }