From f11fbc70cad8efe0fbc43843626da19d7dcb31d0 Mon Sep 17 00:00:00 2001 From: Prashanth Mundkur Date: Wed, 2 May 2018 17:00:36 -0700 Subject: Finish up Sv39 address translation. --- riscv/riscv_sys.sail | 5 +- riscv/riscv_vmem.sail | 202 +++++++++++++++++++++++++++++++++++++++++++++++++- 2 files changed, 203 insertions(+), 4 deletions(-) (limited to 'riscv') diff --git a/riscv/riscv_sys.sail b/riscv/riscv_sys.sail index f0b655f3..e32836c7 100644 --- a/riscv/riscv_sys.sail +++ b/riscv/riscv_sys.sail @@ -392,8 +392,9 @@ register satp : xlenbits function legalize_satp(a : Architecture, o : xlenbits, v : xlenbits) -> xlenbits = { let s = Mk_Satp64(v); match satpMode_of_bits(a, s.Mode()) { - None() => o, - Some(_) => s.bits() + None() => o, + Some(Sv32) => o, /* Sv32 is unsupported for now */ + Some(_) => s.bits() } } diff --git a/riscv/riscv_vmem.sail b/riscv/riscv_vmem.sail index 5d209128..0c1b9949 100644 --- a/riscv/riscv_vmem.sail +++ b/riscv/riscv_vmem.sail @@ -27,7 +27,7 @@ function isInvalidPTE(p : pteAttribs) -> bool = { a.V() == false | (a.W() == true & a.R() == false) } -function checkPTEPermissions(ac : AccessType, priv : Privilege, mxr : bool, sum : bool, p : PTE_Bits) -> bool = { +function checkPTEPermission(ac : AccessType, priv : Privilege, mxr : bool, 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, @@ -103,6 +103,15 @@ bitfield SV39_PTE : pte39 = { BITS : 7 .. 0 } +/* ASID */ + +type asid64 = bits(16) + +function curAsid64() -> asid64 = { + let satp64 = Mk_Satp64(satp); + satp64.Asid() +} + /* Current page table base from satp */ function curPTB39() -> paddr39 = { let satp64 = Mk_Satp64(satp); @@ -136,7 +145,7 @@ function walk39(vaddr, ac, priv, mxr, sum, ptb, level, global) -> PTW_Result = { if level == 0 then PTW_Failure(PTW_Invalid_PTE) else walk39(vaddr, ac, priv, mxr, sum, EXTZ(pte.PPNi()), level - 1, is_global) } else { /* leaf PTE */ - if ~ (checkPTEPermissions(ac, priv, mxr, sum, pattr)) then + if ~ (checkPTEPermission(ac, priv, mxr, sum, pattr)) then PTW_Failure(PTW_No_Permission) else { if level > 0 then { /* superpage */ @@ -155,3 +164,192 @@ function walk39(vaddr, ac, priv, mxr, sum, ptb, level, global) -> PTW_Result = { } } } + +/* 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); + let vAddrMask : vaddr39 = shiftl(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 */ +let TLBEntries = 32 +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 +} + +let enable_dirty_update = true + +val translate39 : (vaddr39, AccessType, Privilege, bool, bool, nat) -> TR39_Result effect {rreg, wreg, wmv, escape, rmem} +function translate39(vAddr, ac, priv, mxr, sum, level) = { + let asid = curAsid64(); + match lookupTLB39(asid, vAddr) { + Some(idx, ent) => { + let pteBits = Mk_PTE_Bits(ent.pte.BITS()); + if ~ (checkPTEPermission(ac, priv, mxr, sum, pteBits)) + then TR39_Failure(PTW_No_Permission) + else { + match update_PTE_Bits(pteBits, ac) { + None() => TR39_Address(ent.pAddr | EXTZ(vAddr & ent.vAddrMask)), + Some(pbits) => { + if ~ (enable_dirty_update) + then TR39_Failure(PTW_PTE_Update) + else { + /* update PTE entry and TLB */ + n_ent : TLB39_Entry = ent; + n_ent.pte = update_BITS(ent.pte, pbits.bits()); + writeTLB39(idx, n_ent); + /* update page table */ + match checked_mem_write(EXTZ(ent.pteAddr), 8, ent.pte.bits()) { + MemValue(_) => (), + MemException(e) => internal_error("invalid physical address in TLB") + }; + TR39_Address(ent.pAddr | EXTZ(vAddr & ent.vAddrMask)) + } + } + } + } + }, + None() => { + match walk39(vAddr, ac, priv, mxr, sum, curPTB39(), level, false) { + PTW_Failure(f) => TR39_Failure(f), + PTW_Success(pAddr, pte, pteAddr, level, global) => { + match update_PTE_Bits(Mk_PTE_Bits(pte.BITS()), ac) { + None() => { + addToTLB39(asid, vAddr, pAddr, pte, pteAddr, level, global); + TR39_Address(pAddr) + }, + Some(pbits) => + if ~ (enable_dirty_update) + then TR39_Failure(PTW_PTE_Update) + else { + w_pte : SV39_PTE = update_BITS(pte, pbits.bits()); + match checked_mem_write(EXTZ(pteAddr), 8, w_pte.bits()) { + MemValue(_) => { + addToTLB39(asid, vAddr, pAddr, w_pte, pteAddr, level, global); + TR39_Address(pAddr) + }, + MemException(e) => TR39_Failure(PTW_Access) + } + } + } + } + } + } + } +} + +/* Address translation mode */ + +val translationMode : (Privilege) -> SATPMode effect {rreg, escape} +function translationMode(priv) = { + if priv == Machine then Sbare + else { + let arch = architecture(mstatus.SXL()); + match arch { + Some(RV64) => { + let mbits : satp_mode = Mk_Satp64(satp).Mode(); + match satpMode_of_bits(RV64, mbits) { + Some(m) => m, + None() => internal_error("invalid RV64 translation mode in satp") + } + }, + _ => internal_error("unsupported address translation arch") + } + } +} + +union TR_Result = { + TR_Address : xlenbits, + TR_Failure : ExceptionType +} + +/* Top-level address translation dispatcher */ + +val translateAddr : (xlenbits, AccessType, ReadType) -> TR_Result effect {escape, rmem, rreg, wmv, wreg} +function translateAddr(vAddr, ac, rt) = { + let effPriv : Privilege = match rt { + Instruction => cur_privilege, + Data => if mstatus.MPRV() == true + then privLevel_of_bits(mstatus.MPP()) + else cur_privilege + }; + let mxr : bool = mstatus.MXR() == true; + let sum : bool = mstatus.SUM() == true; + let mode : SATPMode = translationMode(effPriv); + match mode { + Sbare => TR_Address(vAddr), + SV39 => match translate39(vAddr[38 .. 0], ac, effPriv, mxr, sum, SV39_LEVELS - 1) { + TR39_Address(pa) => TR_Address(EXTZ(pa)), + TR39_Failure(f) => TR_Failure(translationException(ac, f)) + }, + _ => internal_error("unsupported address translation scheme") + } +} -- cgit v1.2.3