diff options
Diffstat (limited to 'model/riscv_vmem_common.sail')
-rw-r--r-- | model/riscv_vmem_common.sail | 294 |
1 files changed, 294 insertions, 0 deletions
diff --git a/model/riscv_vmem_common.sail b/model/riscv_vmem_common.sail new file mode 100644 index 0000000..bf83b23 --- /dev/null +++ b/model/riscv_vmem_common.sail @@ -0,0 +1,294 @@ +/* Shared definitions for supervisor-mode page-table-entries and permission checks. + * + * These definitions are independent of xlen and do not involve + * accessing physical memory. + */ + +/* PageSize */ + +let PAGESIZE_BITS = 12 + +/* PTE attributes, permission checks and updates */ + +type pteAttribs = bits(8) + +bitfield PTE_Bits : pteAttribs = { + D : 7, + A : 6, + G : 5, + U : 4, + X : 3, + W : 2, + R : 1, + V : 0 +} + +function isPTEPtr(p : pteAttribs) -> bool = { + let a = Mk_PTE_Bits(p); + a.R() == false & a.W() == false & a.X() == false +} + +function isInvalidPTE(p : pteAttribs) -> bool = { + let a = Mk_PTE_Bits(p); + a.V() == false | (a.W() == true & a.R() == false) +} + +function checkPTEPermission(ac : AccessType, priv : Privilege, mxr : bool, do_sum : bool, p : PTE_Bits) -> bool = { + match (ac, priv) { + (Read, User) => p.U() == true & (p.R() == true | (p.X() == true & mxr)), + (Write, User) => p.U() == true & p.W() == true, + (ReadWrite, User) => p.U() == true & p.W() == true & (p.R() == true | (p.X() == true & mxr)), + (Execute, User) => p.U() == true & p.X() == true, + + (Read, Supervisor) => (p.U() == false | do_sum) & (p.R() == true | (p.X() == true & mxr)), + (Write, Supervisor) => (p.U() == false | do_sum) & p.W() == true, + (ReadWrite, Supervisor) => (p.U() == false | do_sum) & p.W() == true & (p.R() == true | (p.X() == true & mxr)), + (Execute, Supervisor) => p.U() == false & p.X() == true, + + (_, Machine) => internal_error("m-mode mem perm check") + } +} + +function update_PTE_Bits(p : PTE_Bits, a : AccessType) -> option(PTE_Bits) = { + let update_d = (a == Write | a == ReadWrite) & p.D() == false; // dirty-bit + let update_a = p.A() == false; // accessed-bit + if update_d | update_a then { + let np = update_A(p, true); + let np = if update_d then update_D(np, true) else np; + Some(np) + } else None() +} + +/* failure modes for address-translation/page-table-walks */ +enum PTW_Error = { + PTW_Access, /* physical memory access error for a PTE */ + PTW_Invalid_PTE, + PTW_No_Permission, + PTW_Misaligned, /* misaligned superpage */ + PTW_PTE_Update /* PTE update needed but not enabled */ +} +val cast ptw_error_to_str : PTW_Error -> string +function ptw_error_to_str(e) = + match (e) { + PTW_Access => "mem-access-error", + PTW_Invalid_PTE => "invalid-pte", + PTW_No_Permission => "no-permission", + PTW_Misaligned => "misaligned-superpage", + PTW_PTE_Update => "pte-update-needed" + } + +/* conversion of these translation/PTW failures into architectural exceptions */ +function translationException(a : AccessType, f : PTW_Error) -> ExceptionType = { + let e : ExceptionType = + match (a, f) { + (ReadWrite, PTW_Access) => E_SAMO_Access_Fault, + (ReadWrite, _) => E_SAMO_Page_Fault, + (Read, PTW_Access) => E_Load_Access_Fault, + (Read, _) => E_Load_Page_Fault, + (Write, PTW_Access) => E_SAMO_Access_Fault, + (Write, _) => E_SAMO_Page_Fault, + (Fetch, PTW_Access) => E_Fetch_Access_Fault, + (Fetch, _) => E_Fetch_Page_Fault + } in { +/* print("translationException(" ^ a ^ ", " ^ f ^ ") -> " ^ e); */ + e + } +} + +/* Sv32 parameters and bitfield layouts */ + +let SV32_LEVEL_BITS = 9 +let SV32_LEVELS = 2 +let PTE32_LOG_SIZE = 2 +let PTE32_SIZE = 4 + +type vaddr32 = bits(32) +type paddr32 = bits(34) +type pte32 = bits(32) + +bitfield SV32_Vaddr : vaddr32 = { + VPNi : 31 .. 12, + PgOfs : 11 .. 0 +} + +bitfield SV32_Paddr : paddr32 = { + PPNi : 33 .. 12, + PgOfs : 11 .. 0 +} + +bitfield SV32_PTE : pte32 = { + PPNi : 31 .. 10, + RSW : 9 .. 8, + BITS : 7 .. 0 +} + +/* RV32: ASID */ + +type asid32 = bits(9) + +function curAsid32(satp : bits(32)) -> asid32 = { + let s = Mk_Satp32(satp); + s.Asid() +} + +/* RV32: Current page table base from satp */ +function curPTB32(satp : bits(32)) -> paddr32 = { + let s : Satp32 = Mk_Satp32(satp); + shiftl(EXTZ(s.PPN()), PAGESIZE_BITS) +} + +/* Sv39 parameters and bitfield layouts */ + +let SV39_LEVEL_BITS = 9 +let SV39_LEVELS = 3 +let PTE39_LOG_SIZE = 3 +let PTE39_SIZE = 8 + +type vaddr39 = bits(39) +type paddr39 = bits(56) +type pte39 = bits(64) + +bitfield SV39_Vaddr : vaddr39 = { + VPNi : 38 .. 12, + PgOfs : 11 .. 0 +} + +bitfield SV39_Paddr : paddr39 = { + PPNi : 55 .. 12, + PgOfs : 11 .. 0 +} + +bitfield SV39_PTE : pte39 = { + PPNi : 53 .. 10, + RSW : 9 .. 8, + BITS : 7 .. 0 +} + +/* Sv48 parameters and bitfield layouts */ + +let SV48_LEVEL_BITS = 9 +let SV48_LEVELS = 4 +let PTE48_LOG_SIZE = 3 +let PTE48_SIZE = 8 + +type vaddr48 = bits(48) +type paddr48 = bits(56) +type pte48 = bits(64) + +bitfield SV48_Vaddr : vaddr48 = { + VPNi : 38 .. 12, + PgOfs : 11 .. 0 +} + +bitfield SV48_Paddr : paddr48 = { + PPNi : 55 .. 12, + PgOfs : 11 .. 0 +} + +bitfield SV48_PTE : pte48 = { + PPNi : 53 .. 10, + RSW : 9 .. 8, + BITS : 7 .. 0 +} + +/* RV64: ASID */ + +type asid64 = bits(16) + +function curAsid64(satp : bits(64)) -> asid64 = { + let s = Mk_Satp64(satp); + s.Asid() +} + +/* RV64: Current page table base from satp */ +function curPTB39(satp : bits(64)) -> paddr39 = { + let s = Mk_Satp64(satp); + EXTZ(shiftl(s.PPN(), PAGESIZE_BITS)) +} + +/* Result of a page-table walk. */ + +union PTW_Result = { + PTW_Success: (paddr39, SV39_PTE, paddr39, nat, bool), + PTW_Failure: PTW_Error +} + +/* idealized TLB to model fence.vm and also speed up simulation. */ + +struct TLB39_Entry = { + asid : asid64, + global : bool, + vAddr : vaddr39, /* VPN */ + pAddr : paddr39, /* PPN */ + vMatchMask : vaddr39, /* matching mask for superpages */ + vAddrMask : vaddr39, /* selection mask for superpages */ + pte : SV39_PTE, /* permissions */ + pteAddr : paddr39, /* for dirty writeback */ + age : xlenbits +} + +/* the rreg effect is an artifact of using the cycle counter to provide the age */ +val make_TLB39_Entry : (asid64, bool, vaddr39, paddr39, SV39_PTE, nat, paddr39) -> TLB39_Entry effect {rreg} + +function make_TLB39_Entry(asid, global, vAddr, pAddr, pte, level, pteAddr) = { + let shift : nat = PAGESIZE_BITS + (level * SV39_LEVEL_BITS); + /* fixme hack: use a better idiom for masks */ + let vAddrMask : vaddr39 = shiftl(vAddr ^ vAddr ^ EXTZ(0b1), shift) - 1; + let vMatchMask : vaddr39 = ~ (vAddrMask); + struct { + asid = asid, + global = global, + pte = pte, + pteAddr = pteAddr, + vAddrMask = vAddrMask, + vMatchMask = vMatchMask, + vAddr = vAddr & vMatchMask, + pAddr = shiftl(shiftr(pAddr, shift), shift), + age = mcycle + } +} + +/* TODO: make this a vector or array of entries */ +register tlb39 : option(TLB39_Entry) + +val lookupTLB39 : (asid64, vaddr39) -> option((int, TLB39_Entry)) effect {rreg} +function lookupTLB39(asid, vaddr) = { + match tlb39 { + None() => None(), + Some(e) => if (e.global | (e.asid == asid)) + & (e.vAddr == (e.vMatchMask & vaddr)) + then Some((0, e)) + else None() + } +} + +val addToTLB39 : (asid64, vaddr39, paddr39, SV39_PTE, paddr39, nat, bool) -> unit effect {wreg, rreg} +function addToTLB39(asid, vAddr, pAddr, pte, pteAddr, level, global) = { + let ent = make_TLB39_Entry(asid, global, vAddr, pAddr, pte, level, pteAddr); + tlb39 = Some(ent) +} + +function writeTLB39(idx : int, ent : TLB39_Entry) -> unit = + tlb39 = Some(ent) + +val flushTLB : (option(asid64), option(vaddr39)) -> unit effect {rreg, wreg} +function flushTLB(asid, addr) = { + let ent : option(TLB39_Entry) = + match (tlb39, asid, addr) { + (None(), _, _) => None(), + (Some(e), None(), None()) => None(), + (Some(e), None(), Some(a)) => if e.vAddr == (e.vMatchMask & a) + then None() else Some(e), + (Some(e), Some(i), None()) => if (e.asid == i) & (~ (e.global)) + then None() else Some(e), + (Some(e), Some(i), Some(a)) => if (e.asid == i) & (e.vAddr == (a & e.vMatchMask)) + & (~ (e.global)) + then None() else Some(e) + }; + tlb39 = ent +} + +union TR39_Result = { + TR39_Address : paddr39, + TR39_Failure : PTW_Error +} |