aboutsummaryrefslogtreecommitdiff
path: root/model
diff options
context:
space:
mode:
authorPrashanth Mundkur <prashanth.mundkur@gmail.com>2019-07-16 17:37:16 -0700
committerPrashanth Mundkur <prashanth.mundkur@gmail.com>2019-07-16 17:41:41 -0700
commitcc996651a3a756c862251e470dd21d9e19a4d420 (patch)
treead5a09b62e68aade733937ab5a3e00f3db9016a2 /model
parent39ed62d79e9f4ead6f52e755df9f9562e44696ac (diff)
downloadsail-riscv-cc996651a3a756c862251e470dd21d9e19a4d420.zip
sail-riscv-cc996651a3a756c862251e470dd21d9e19a4d420.tar.gz
sail-riscv-cc996651a3a756c862251e470dd21d9e19a4d420.tar.bz2
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.
Diffstat (limited to 'model')
-rw-r--r--model/riscv_pte.sail15
-rw-r--r--model/riscv_vmem_common.sail2
-rw-r--r--model/riscv_vmem_rv32.sail6
-rw-r--r--model/riscv_vmem_sv32.sail24
-rw-r--r--model/riscv_vmem_sv39.sail20
-rw-r--r--model/riscv_vmem_sv48.sail12
-rw-r--r--model/riscv_vmem_types.sail2
7 files changed, 49 insertions, 32 deletions
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