From 8f90f78870eb0d85e1ac830f1528a536b9c2687c Mon Sep 17 00:00:00 2001 From: Ved Shanbhogue Date: Mon, 22 Jan 2024 14:45:16 -0600 Subject: [PATCH] add svnapot and svpbmt --- 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_pte.sail | 55 +++++++++++++++++++++----------- model/riscv_sys_regs.sail | 10 ++++-- model/riscv_vmem_sv32.sail | 14 ++++---- model/riscv_vmem_sv39.sail | 27 ++++++++-------- model/riscv_vmem_sv48.sail | 21 ++++++------ 10 files changed, 104 insertions(+), 51 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_pte.sail b/model/riscv_pte.sail index 7e2633742..44c8d0c23 100644 --- a/model/riscv_pte.sail +++ b/model/riscv_pte.sail @@ -70,14 +70,23 @@ /* 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 EXT_PTE_Bits : extPte = { +bitfield PTE_StdExt_Bits : pteStdExtAttribs = { N : 9, PBMT : 8 .. 7, RSVD : 6 .. 0 @@ -90,9 +99,9 @@ bitfield EXT_PTE_Bits : extPte = { * 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, @@ -105,20 +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); - let e = Mk_EXT_PTE_Bits(ext); - a.V() == 0b0 | - (a.W() == 0b1 & a.R() == 0b0) | - (e.RSVD() != 0b0000000 | e.PBMT() == 0b11) | - (not(isPTEPtr(p, ext)) & (e.N() != 0b0 ) & (not(haveSvnapot()))) | - (not(isPTEPtr(p, ext)) & (e.PBMT() != 0b00) & (not(haveSvpbmt()) | menvcfg.PBMTE() == 0b0)) | - (isPTEPtr(p, ext) & (a.D() == 0b1 | a.A() == 0b1 | a.U() == 0b1 | e.N() != 0b0 | e.PBMT() != 0b00)) + 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 = { @@ -129,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), @@ -149,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, @@ -161,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 75c9f038a..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. */ @@ -216,10 +222,10 @@ function haveZmmul() -> bool = true function haveZicond() -> bool = true /* Svpbmt extension support */ -function haveSvpbmt() -> bool = true +function haveSvpbmt() -> bool = sys_enable_svpbmt() /* Svnapot extension support */ -function haveSvnapot() -> bool = true +function haveSvnapot() -> bool = sys_enable_svnapot() bitfield Mstatush : bits(32) = { MBE : 5, 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 eedbe08cc..25c814487 100644 --- a/model/riscv_vmem_sv39.sail +++ b/model/riscv_vmem_sv39.sail @@ -88,20 +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_EXT_PTE_Bits(ext_pte); + 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) @@ -111,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) @@ -120,7 +120,7 @@ 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 eattr.N() == 0b1 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 */ @@ -136,12 +136,13 @@ function walk39(vaddr, ac, priv, mxr, do_sum, ptb, level, global, ext_ptw) = { } } else { /* normal leaf PTE */ - if ( eattr.N() == 0b1 & pte.PPNi()[3 .. 0] != 0b1000 ) then { + if ( haveSvnapot() & eattr.N() == 0b1 & pte.PPNi()[3 .. 0] != 0b1000 ) then { PTW_Failure(PTW_Invalid_PTE(), ext_ptw) } else { - let ppn : bits(44) = match eattr.N() { - 0b0 => pte.PPNi(), - 0b1 => append(pte.PPNi()[43 .. 4], va.VPNi()[3 .. 0]) + 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)); */ @@ -196,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 d0fd0992c..3d8cc64ce 100644 --- a/model/riscv_vmem_sv48.sail +++ b/model/riscv_vmem_sv48.sail @@ -88,20 +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_EXT_PTE_Bits(ext_pte); + 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) @@ -111,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) @@ -120,7 +120,7 @@ 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 eattr.N() == 0b1 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 */ @@ -136,12 +136,13 @@ function walk48(vaddr, ac, priv, mxr, do_sum, ptb, level, global, ext_ptw) = { } } else { /* normal leaf PTE */ - if ( eattr.N() == 0b1 & pte.PPNi()[3 .. 0] != 0b1000 ) then { + if ( haveSvnapot() & eattr.N() == 0b1 & pte.PPNi()[3 .. 0] != 0b1000 ) then { PTW_Failure(PTW_Invalid_PTE(), ext_ptw) } else { - let ppn : bits(44) = match eattr.N() { - 0b0 => pte.PPNi(), - 0b1 => append(pte.PPNi()[43 .. 4], va.VPNi()[3 .. 0]) + 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)); */