Start extracting bits of vmem that should be common to RV32, and add some definitions for Sv32 and Sv48.

1 files changed, 294 insertions, 0 deletions

diff --git a/model/riscv_vmem_common.sail b/model/riscv_vmem_common.sail
new file mode 100644
index 0000000..bf83b23
--- /dev/null
+++ b/model/riscv_vmem_common.sail
@@ -0,0 +1,294 @@
+/* Shared definitions for supervisor-mode page-table-entries and permission checks.
+ *
+ * These definitions are independent of xlen and do not involve
+ * accessing physical memory.
+ */
+
+/* PageSize */
+
+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 cast 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"
+  }
+
+/* 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
+  }
+}
+
+/* Sv32 parameters and bitfield layouts */
+
+let SV32_LEVEL_BITS = 9
+let SV32_LEVELS = 2
+let PTE32_LOG_SIZE = 2
+let PTE32_SIZE = 4
+
+type vaddr32 = bits(32)
+type paddr32 = bits(34)
+type pte32   = bits(32)
+
+bitfield SV32_Vaddr : vaddr32 = {
+  VPNi  : 31 .. 12,
+  PgOfs : 11 .. 0
+}
+
+bitfield SV32_Paddr : paddr32 = {
+  PPNi  : 33 .. 12,
+  PgOfs : 11 .. 0
+}
+
+bitfield SV32_PTE : pte32 = {
+  PPNi  : 31 .. 10,
+  RSW   : 9 .. 8,
+  BITS  : 7 .. 0
+}
+
+/* RV32: ASID */
+
+type asid32 = bits(9)
+
+function curAsid32(satp : bits(32)) -> asid32 = {
+  let s = Mk_Satp32(satp);
+  s.Asid()
+}
+
+/* RV32: Current page table base from satp */
+function curPTB32(satp : bits(32)) -> paddr32 = {
+  let s : Satp32 = Mk_Satp32(satp);
+  shiftl(EXTZ(s.PPN()), PAGESIZE_BITS)
+}
+
+/* Sv39 parameters and bitfield layouts */
+
+let SV39_LEVEL_BITS = 9
+let SV39_LEVELS = 3
+let PTE39_LOG_SIZE = 3
+let PTE39_SIZE = 8
+
+type vaddr39 = bits(39)
+type paddr39 = bits(56)
+type pte39   = bits(64)
+
+bitfield SV39_Vaddr : vaddr39 = {
+  VPNi  : 38 .. 12,
+  PgOfs : 11 .. 0
+}
+
+bitfield SV39_Paddr : paddr39 = {
+  PPNi  : 55 .. 12,
+  PgOfs : 11 .. 0
+}
+
+bitfield SV39_PTE : pte39 = {
+  PPNi  : 53 .. 10,
+  RSW   : 9 .. 8,
+  BITS  : 7 .. 0
+}
+
+/* Sv48 parameters and bitfield layouts */
+
+let SV48_LEVEL_BITS = 9
+let SV48_LEVELS = 4
+let PTE48_LOG_SIZE = 3
+let PTE48_SIZE = 8
+
+type vaddr48 = bits(48)
+type paddr48 = bits(56)
+type pte48   = bits(64)
+
+bitfield SV48_Vaddr : vaddr48 = {
+  VPNi  : 38 .. 12,
+  PgOfs : 11 .. 0
+}
+
+bitfield SV48_Paddr : paddr48 = {
+  PPNi  : 55 .. 12,
+  PgOfs : 11 .. 0
+}
+
+bitfield SV48_PTE : pte48 = {
+  PPNi  : 53 .. 10,
+  RSW   : 9 .. 8,
+  BITS  : 7 .. 0
+}
+
+/* RV64: ASID */
+
+type asid64 = bits(16)
+
+function curAsid64(satp : bits(64)) -> asid64 = {
+  let s = Mk_Satp64(satp);
+  s.Asid()
+}
+
+/* RV64: Current page table base from satp */
+function curPTB39(satp : bits(64)) -> paddr39 = {
+  let s = Mk_Satp64(satp);
+  EXTZ(shiftl(s.PPN(), PAGESIZE_BITS))
+}
+
+/* Result of a page-table walk. */
+
+union PTW_Result = {
+  PTW_Success: (paddr39, SV39_PTE, paddr39, nat, bool),
+  PTW_Failure: PTW_Error
+}
+
+/* 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);
+  /* fixme hack: use a better idiom for masks */
+  let vAddrMask : vaddr39 = shiftl(vAddr ^ vAddr ^ 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 */
+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
+}