Allow extensions to types of memory access, and factor out PTE and PTW definitions.

1 files changed, 0 insertions, 89 deletions

diff --git a/model/riscv_vmem_common.sail b/model/riscv_vmem_common.sail
index c8808f7..f77366b 100644
--- a/model/riscv_vmem_common.sail
+++ b/model/riscv_vmem_common.sail
@@ -8,95 +8,6 @@
 
 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 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"
-  }
-
-overload to_str = {ptw_error_to_str}
-
-/* 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
-  }
-}
-
 /*
  * Definitions for RV32, which has a single address translation mode: Sv32.
  */