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.

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