From cc996651a3a756c862251e470dd21d9e19a4d420 Mon Sep 17 00:00:00 2001 From: Prashanth Mundkur Date: Tue, 16 Jul 2019 17:37:16 -0700 Subject: Use reserved bits in PTEs for vmem extensions on RV64, as allowed by the spec. This is not possible for RV32, so pass zeros there. --- model/riscv_pte.sail | 15 ++++++++++----- model/riscv_vmem_common.sail | 2 ++ model/riscv_vmem_rv32.sail | 6 +++--- model/riscv_vmem_sv32.sail | 24 ++++++++++++++---------- model/riscv_vmem_sv39.sail | 20 ++++++++++++-------- model/riscv_vmem_sv48.sail | 12 +++++++----- model/riscv_vmem_types.sail | 2 +- 7 files changed, 49 insertions(+), 32 deletions(-) (limited to 'model') diff --git a/model/riscv_pte.sail b/model/riscv_pte.sail index 34266cc..87a9f08 100644 --- a/model/riscv_pte.sail +++ b/model/riscv_pte.sail @@ -2,6 +2,11 @@ type pteAttribs = bits(8) +/* Reserved PTE bits could be used by extensions on RV64. There are + * no such available bits on RV32, so these bits will be zeros on RV32. + */ +type extPte = bits(10) + bitfield PTE_Bits : pteAttribs = { D : 7, A : 6, @@ -13,17 +18,17 @@ bitfield PTE_Bits : pteAttribs = { V : 0 } -function isPTEPtr(p : pteAttribs) -> bool = { +function isPTEPtr(p : pteAttribs, ext : extPte) -> bool = { let a = Mk_PTE_Bits(p); a.R() == false & a.W() == false & a.X() == false } -function isInvalidPTE(p : pteAttribs) -> bool = { +function isInvalidPTE(p : pteAttribs, ext : extPte) -> bool = { let a = Mk_PTE_Bits(p); a.V() == false | (a.W() == true & a.R() == false) } -function checkPTEPermission(ac : AccessType(ext_access_type), priv : Privilege, mxr : bool, do_sum : bool, p : PTE_Bits) -> bool = { +function checkPTEPermission(ac : AccessType(ext_access_type), priv : Privilege, mxr : bool, do_sum : bool, p : PTE_Bits, ext : extPte) -> bool = { match (ac, priv) { (Read(Data), User) => p.U() == true & (p.R() == true | (p.X() == true & mxr)), (Write(Data), User) => p.U() == true & p.W() == true, @@ -39,12 +44,12 @@ function checkPTEPermission(ac : AccessType(ext_access_type), priv : Privilege, } } -function update_PTE_Bits(p : PTE_Bits, a : AccessType(ext_access_type)) -> option(PTE_Bits) = { +function update_PTE_Bits(p : PTE_Bits, a : AccessType(ext_access_type), ext : extPte) -> option((PTE_Bits, extPte)) = { let update_d = (a == Write(Data) | a == ReadWrite(Data)) & 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) + Some(np, ext) } else None() } diff --git a/model/riscv_vmem_common.sail b/model/riscv_vmem_common.sail index f77366b..1a82d4c 100644 --- a/model/riscv_vmem_common.sail +++ b/model/riscv_vmem_common.sail @@ -106,6 +106,7 @@ bitfield SV39_Paddr : paddr64 = { } bitfield SV39_PTE : pte64 = { + Ext : 63 .. 54, PPNi : 53 .. 10, RSW : 9 .. 8, BITS : 7 .. 0 @@ -132,6 +133,7 @@ bitfield SV48_Paddr : paddr64 = { } bitfield SV48_PTE : pte48 = { + Ext : 63 .. 54, PPNi : 53 .. 10, RSW : 9 .. 8, BITS : 7 .. 0 diff --git a/model/riscv_vmem_rv32.sail b/model/riscv_vmem_rv32.sail index 5b640b1..f1b4ac0 100644 --- a/model/riscv_vmem_rv32.sail +++ b/model/riscv_vmem_rv32.sail @@ -26,11 +26,11 @@ function translationMode(priv) = { /* Top-level address translation dispatcher */ -val translateAddr : (xlenbits, AccessType) -> TR_Result(xlenbits, ExceptionType) effect {escape, rmem, rreg, wmv, wmvt, wreg} +val translateAddr : (xlenbits, AccessType(ext_access_type)) -> TR_Result(xlenbits, ExceptionType) effect {escape, rmem, rreg, wmv, wmvt, wreg} function translateAddr(vAddr, ac) = { let effPriv : Privilege = match ac { - Execute => cur_privilege, - _ => effectivePrivilege(mstatus, cur_privilege) + Execute() => cur_privilege, + _ => effectivePrivilege(mstatus, cur_privilege) }; let mxr : bool = mstatus.MXR() == true; let do_sum : bool = mstatus.SUM() == true; diff --git a/model/riscv_vmem_sv32.sail b/model/riscv_vmem_sv32.sail index 49d7ec1..fe4ae3e 100644 --- a/model/riscv_vmem_sv32.sail +++ b/model/riscv_vmem_sv32.sail @@ -6,7 +6,7 @@ function to_phys_addr(a : paddr32) -> xlenbits = a[31..0] -val walk32 : (vaddr32, AccessType, Privilege, bool, bool, paddr32, nat, bool) -> PTW_Result(paddr32, SV32_PTE) effect {rmem, rreg, escape} +val walk32 : (vaddr32, AccessType(ext_access_type), Privilege, bool, bool, paddr32, nat, bool) -> PTW_Result(paddr32, SV32_PTE) effect {rmem, rreg, escape} function walk32(vaddr, ac, priv, mxr, do_sum, ptb, level, global) = { let va = Mk_SV32_Vaddr(vaddr); let pt_ofs : paddr32 = shiftl(EXTZ(shiftr(va.VPNi(), (level * SV32_LEVEL_BITS))[(SV32_LEVEL_BITS - 1) .. 0]), @@ -24,6 +24,7 @@ function walk32(vaddr, ac, priv, mxr, do_sum, ptb, level, global) = { MemValue(v) => { let pte = Mk_SV32_PTE(v); let pbits = pte.BITS(); + let ext_pte : extPte = zeros(); // no reserved bits for extensions let pattr = Mk_PTE_Bits(pbits); let is_global = global | (pattr.G() == true); /* print("walk32(vaddr=" ^ BitStr(vaddr) ^ " level=" ^ string_of_int(level) @@ -31,11 +32,11 @@ function walk32(vaddr, ac, priv, mxr, do_sum, ptb, level, global) = { ^ " pt_ofs=" ^ BitStr(to_phys_addr(pt_ofs)) ^ " pte_addr=" ^ BitStr(to_phys_addr(pte_addr)) ^ " pte=" ^ BitStr(v)); */ - if isInvalidPTE(pbits) then { + if isInvalidPTE(pbits, ext_pte) then { /* print("walk32: invalid pte"); */ PTW_Failure(PTW_Invalid_PTE) } else { - if isPTEPtr(pbits) then { + if isPTEPtr(pbits, ext_pte) then { if level == 0 then { /* last-level PTE contains a pointer instead of a leaf */ /* print("walk32: last-level pte contains a ptr"); */ @@ -45,7 +46,7 @@ function walk32(vaddr, ac, priv, mxr, do_sum, ptb, level, global) = { walk32(vaddr, ac, priv, mxr, do_sum, shiftl(EXTZ(pte.PPNi()), PAGESIZE_BITS), level - 1, is_global) } } else { /* leaf PTE */ - if ~ (checkPTEPermission(ac, priv, mxr, do_sum, pattr)) then { + if ~ (checkPTEPermission(ac, priv, mxr, do_sum, pattr, ext_pte)) then { /* print("walk32: pte permission check failure"); */ PTW_Failure(PTW_No_Permission) } else { @@ -111,19 +112,20 @@ function flush_TLB32(asid, addr) = /* address translation */ -val translate32 : (asid32, paddr32, vaddr32, AccessType, Privilege, bool, bool, nat) -> TR_Result(paddr32, PTW_Error) effect {rreg, wreg, wmv, wmvt, escape, rmem} +val translate32 : (asid32, paddr32, vaddr32, AccessType(ext_access_type), Privilege, bool, bool, nat) -> TR_Result(paddr32, PTW_Error) effect {rreg, wreg, wmv, wmvt, escape, rmem} function translate32(asid, ptb, vAddr, ac, priv, mxr, do_sum, level) = { 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 pteBits = Mk_PTE_Bits(pte.BITS()); - if ~ (checkPTEPermission(ac, priv, mxr, do_sum, pteBits)) + if ~ (checkPTEPermission(ac, priv, mxr, do_sum, pteBits, ext_pte)) then TR_Failure(PTW_No_Permission) else { - match update_PTE_Bits(pteBits, ac) { + match update_PTE_Bits(pteBits, ac, ext_pte) { None() => TR_Address(ent.pAddr | EXTZ(vAddr & ent.vAddrMask)), - Some(pbits) => { + Some(pbits, ext) => { if ~ (plat_enable_dirty_update ()) then { /* pte needs dirty/accessed update but that is not enabled */ @@ -131,6 +133,7 @@ function translate32(asid, ptb, vAddr, ac, priv, mxr, do_sum, level) = { } else { /* update PTE entry and TLB */ n_pte = update_BITS(pte, pbits.bits()); + /* ext is unused since there are no reserved bits for extensions */ n_ent : TLB32_Entry = ent; n_ent.pte = n_pte.bits(); write_TLB32(idx, n_ent); @@ -149,18 +152,19 @@ function translate32(asid, ptb, vAddr, ac, priv, mxr, do_sum, level) = { match walk32(vAddr, ac, priv, mxr, do_sum, ptb, level, false) { PTW_Failure(f) => TR_Failure(f), PTW_Success(pAddr, pte, pteAddr, level, global) => { - match update_PTE_Bits(Mk_PTE_Bits(pte.BITS()), ac) { + 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) }, - Some(pbits) => + Some(pbits, ext) => if ~ (plat_enable_dirty_update ()) then { /* pte needs dirty/accessed update but that is not enabled */ TR_Failure(PTW_PTE_Update) } else { w_pte : SV32_PTE = update_BITS(pte, pbits.bits()); + /* ext is unused since there are no reserved bits for extensions */ match mem_write_value(to_phys_addr(pteAddr), 4, w_pte.bits(), false, false, false) { MemValue(_) => { add_to_TLB32(asid, vAddr, pAddr, w_pte, pteAddr, level, global); diff --git a/model/riscv_vmem_sv39.sail b/model/riscv_vmem_sv39.sail index c31a9bb..2ae2b4c 100644 --- a/model/riscv_vmem_sv39.sail +++ b/model/riscv_vmem_sv39.sail @@ -18,6 +18,7 @@ function walk39(vaddr, ac, priv, mxr, do_sum, ptb, level, global) = { MemValue(v) => { let pte = Mk_SV39_PTE(v); let pbits = pte.BITS(); + let ext_pte = pte.Ext(); let pattr = Mk_PTE_Bits(pbits); let is_global = global | (pattr.G() == true); /* print("walk39(vaddr=" ^ BitStr(vaddr) ^ " level=" ^ string_of_int(level) @@ -25,11 +26,11 @@ function walk39(vaddr, ac, priv, mxr, do_sum, ptb, level, global) = { ^ " pt_ofs=" ^ BitStr(pt_ofs) ^ " pte_addr=" ^ BitStr(pte_addr) ^ " pte=" ^ BitStr(v)); */ - if isInvalidPTE(pbits) then { + if isInvalidPTE(pbits, ext_pte) then { /* print("walk39: invalid pte"); */ PTW_Failure(PTW_Invalid_PTE) } else { - if isPTEPtr(pbits) then { + if isPTEPtr(pbits, ext_pte) then { if level == 0 then { /* last-level PTE contains a pointer instead of a leaf */ /* print("walk39: last-level pte contains a ptr"); */ @@ -39,7 +40,7 @@ function walk39(vaddr, ac, priv, mxr, do_sum, ptb, level, global) = { walk39(vaddr, ac, priv, mxr, do_sum, shiftl(EXTZ(pte.PPNi()), PAGESIZE_BITS), level - 1, is_global) } } else { /* leaf PTE */ - if ~ (checkPTEPermission(ac, priv, mxr, do_sum, pattr)) then { + if ~ (checkPTEPermission(ac, priv, mxr, do_sum, pattr, ext_pte)) then { /* print("walk39: pte permission check failure"); */ PTW_Failure(PTW_No_Permission) } else { @@ -111,13 +112,14 @@ function translate39(asid, ptb, vAddr, ac, priv, mxr, do_sum, level) = { Some(idx, ent) => { /* print("translate39: TLB39 hit for " ^ BitStr(vAddr)); */ let pte = Mk_SV39_PTE(ent.pte); + let ext_pte = pte.Ext(); let pteBits = Mk_PTE_Bits(pte.BITS()); - if ~ (checkPTEPermission(ac, priv, mxr, do_sum, pteBits)) + if ~ (checkPTEPermission(ac, priv, mxr, do_sum, pteBits, ext_pte)) then TR_Failure(PTW_No_Permission) else { - match update_PTE_Bits(pteBits, ac) { + match update_PTE_Bits(pteBits, ac, ext_pte) { None() => TR_Address(ent.pAddr | EXTZ(vAddr & ent.vAddrMask)), - Some(pbits) => { + Some(pbits, ext) => { if ~ (plat_enable_dirty_update ()) then { /* pte needs dirty/accessed update but that is not enabled */ @@ -125,6 +127,7 @@ function translate39(asid, ptb, vAddr, ac, priv, mxr, do_sum, level) = { } else { /* update PTE entry and TLB */ n_pte = update_BITS(pte, pbits.bits()); + n_pte = update_Ext(n_pte, ext); n_ent : TLB39_Entry = ent; n_ent.pte = n_pte.bits(); write_TLB39(idx, n_ent); @@ -143,18 +146,19 @@ function translate39(asid, ptb, vAddr, ac, priv, mxr, do_sum, level) = { match walk39(vAddr, ac, priv, mxr, do_sum, ptb, level, false) { PTW_Failure(f) => TR_Failure(f), PTW_Success(pAddr, pte, pteAddr, level, global) => { - match update_PTE_Bits(Mk_PTE_Bits(pte.BITS()), ac) { + 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) }, - Some(pbits) => + Some(pbits, ext) => if ~ (plat_enable_dirty_update ()) then { /* pte needs dirty/accessed update but that is not enabled */ TR_Failure(PTW_PTE_Update) } else { w_pte : SV39_PTE = update_BITS(pte, pbits.bits()); + w_pte : SV39_PTE = update_Ext(w_pte, ext); match mem_write_value(EXTZ(pteAddr), 8, w_pte.bits(), false, false, false) { MemValue(_) => { add_to_TLB39(asid, vAddr, pAddr, w_pte, pteAddr, level, global); diff --git a/model/riscv_vmem_sv48.sail b/model/riscv_vmem_sv48.sail index 664807c..0fe6545 100644 --- a/model/riscv_vmem_sv48.sail +++ b/model/riscv_vmem_sv48.sail @@ -18,6 +18,7 @@ function walk48(vaddr, ac, priv, mxr, do_sum, ptb, level, global) = { MemValue(v) => { let pte = Mk_SV48_PTE(v); let pbits = pte.BITS(); + let ext_pte = pte.Ext(); let pattr = Mk_PTE_Bits(pbits); let is_global = global | (pattr.G() == true); /* print("walk48(vaddr=" ^ BitStr(vaddr) ^ " level=" ^ string_of_int(level) @@ -25,11 +26,11 @@ function walk48(vaddr, ac, priv, mxr, do_sum, ptb, level, global) = { ^ " pt_ofs=" ^ BitStr(pt_ofs) ^ " pte_addr=" ^ BitStr(pte_addr) ^ " pte=" ^ BitStr(v)); */ - if isInvalidPTE(pbits) then { + if isInvalidPTE(pbits, ext_pte) then { /* print("walk48: invalid pte"); */ PTW_Failure(PTW_Invalid_PTE) } else { - if isPTEPtr(pbits) then { + if isPTEPtr(pbits, ext_pte) then { if level == 0 then { /* last-level PTE contains a pointer instead of a leaf */ /* print("walk48: last-level pte contains a ptr"); */ @@ -39,7 +40,7 @@ function walk48(vaddr, ac, priv, mxr, do_sum, ptb, level, global) = { walk48(vaddr, ac, priv, mxr, do_sum, shiftl(EXTZ(pte.PPNi()), PAGESIZE_BITS), level - 1, is_global) } } else { /* leaf PTE */ - if ~ (checkPTEPermission(ac, priv, mxr, do_sum, pattr)) then { + if ~ (checkPTEPermission(ac, priv, mxr, do_sum, pattr, ext_pte)) then { /* print("walk48: pte permission check failure"); */ PTW_Failure(PTW_No_Permission) } else { @@ -110,18 +111,19 @@ function translate48(asid, ptb, vAddr, ac, priv, mxr, do_sum, level) = { match walk48(vAddr, ac, priv, mxr, do_sum, ptb, level, false) { PTW_Failure(f) => TR_Failure(f), PTW_Success(pAddr, pte, pteAddr, level, global) => { - match update_PTE_Bits(Mk_PTE_Bits(pte.BITS()), ac) { + 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) }, - Some(pbits) => + Some(pbits, ext) => if ~ (plat_enable_dirty_update ()) then { /* pte needs dirty/accessed update but that is not enabled */ TR_Failure(PTW_PTE_Update) } else { w_pte : SV48_PTE = update_BITS(pte, pbits.bits()); + w_pte : SV48_PTE = update_Ext(w_pte, ext); match mem_write_value(EXTZ(pteAddr), 8, w_pte.bits(), false, false, false) { MemValue(_) => { add_to_TLB48(asid, vAddr, pAddr, w_pte, pteAddr, level, global); diff --git a/model/riscv_vmem_types.sail b/model/riscv_vmem_types.sail index 577de37..30a5687 100644 --- a/model/riscv_vmem_types.sail +++ b/model/riscv_vmem_types.sail @@ -1,4 +1,4 @@ -// Specialize the accesstype for memory +// Extensions for memory Accesstype type ext_access_type = unit -- cgit v1.1