Finish up Sv39 address translation.

2 files changed, 203 insertions, 4 deletions

diff --git a/riscv/riscv_sys.sail b/riscv/riscv_sys.sail
index f0b655f3..e32836c7 100644
--- a/riscv/riscv_sys.sail
+++ b/riscv/riscv_sys.sail
@@ -392,8 +392,9 @@ register satp : xlenbits
 function legalize_satp(a : Architecture, o : xlenbits, v : xlenbits) -> xlenbits = {
   let s = Mk_Satp64(v);
   match satpMode_of_bits(a, s.Mode()) {
-    None()  => o,
-    Some(_) => s.bits()
+    None()     => o,
+    Some(Sv32) => o,  /* Sv32 is unsupported for now */
+    Some(_)    => s.bits()
   }
 }
 
diff --git a/riscv/riscv_vmem.sail b/riscv/riscv_vmem.sail
index 5d209128..0c1b9949 100644
--- a/riscv/riscv_vmem.sail
+++ b/riscv/riscv_vmem.sail
@@ -27,7 +27,7 @@ function isInvalidPTE(p : pteAttribs) -> bool = {
   a.V() == false | (a.W() == true & a.R() == false)
 }
 
-function checkPTEPermissions(ac : AccessType, priv : Privilege, mxr : bool, sum : bool, p : PTE_Bits) -> bool = {
+function checkPTEPermission(ac : AccessType, priv : Privilege, mxr : bool, 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,
@@ -103,6 +103,15 @@ bitfield SV39_PTE : pte39 = {
   BITS  : 7 .. 0
 }
 
+/* ASID */
+
+type asid64 = bits(16)
+
+function curAsid64() -> asid64 = {
+  let satp64 = Mk_Satp64(satp);
+  satp64.Asid()
+}
+
 /* Current page table base from satp */
 function curPTB39() -> paddr39 = {
   let satp64 = Mk_Satp64(satp);
@@ -136,7 +145,7 @@ function walk39(vaddr, ac, priv, mxr, sum, ptb, level, global) -> PTW_Result = {
           if level == 0 then PTW_Failure(PTW_Invalid_PTE)
           else walk39(vaddr, ac, priv, mxr, sum, EXTZ(pte.PPNi()), level - 1, is_global)
         } else { /* leaf PTE */
-          if ~ (checkPTEPermissions(ac, priv, mxr, sum, pattr)) then
+          if ~ (checkPTEPermission(ac, priv, mxr, sum, pattr)) then
             PTW_Failure(PTW_No_Permission)
           else {
             if level > 0 then { /* superpage */
@@ -155,3 +164,192 @@ function walk39(vaddr, ac, priv, mxr, sum, ptb, level, global) -> PTW_Result = {
     }
   }
 }
+
+/* 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);
+  let vAddrMask : vaddr39 = shiftl(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 */
+let TLBEntries = 32
+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
+}
+
+let enable_dirty_update = true
+
+val translate39 : (vaddr39, AccessType, Privilege, bool, bool, nat) -> TR39_Result effect {rreg, wreg, wmv, escape, rmem}
+function translate39(vAddr, ac, priv, mxr, sum, level) = {
+  let asid = curAsid64();
+  match lookupTLB39(asid, vAddr) {
+    Some(idx, ent) => {
+      let pteBits = Mk_PTE_Bits(ent.pte.BITS());
+      if ~ (checkPTEPermission(ac, priv, mxr, sum, pteBits))
+      then TR39_Failure(PTW_No_Permission)
+      else {
+        match update_PTE_Bits(pteBits, ac) {
+          None() => TR39_Address(ent.pAddr | EXTZ(vAddr & ent.vAddrMask)),
+          Some(pbits) => {
+            if ~ (enable_dirty_update)
+            then TR39_Failure(PTW_PTE_Update)
+            else {
+              /* update PTE entry and TLB */
+              n_ent : TLB39_Entry = ent;
+              n_ent.pte = update_BITS(ent.pte, pbits.bits());
+              writeTLB39(idx, n_ent);
+              /* update page table */
+              match checked_mem_write(EXTZ(ent.pteAddr), 8, ent.pte.bits()) {
+                MemValue(_) => (),
+                MemException(e) => internal_error("invalid physical address in TLB")
+              };
+              TR39_Address(ent.pAddr | EXTZ(vAddr & ent.vAddrMask))
+            }
+          }
+        }
+      }
+    },
+    None() => {
+      match walk39(vAddr, ac, priv, mxr, sum, curPTB39(), level, false) {
+        PTW_Failure(f) => TR39_Failure(f),
+        PTW_Success(pAddr, pte, pteAddr, level, global) => {
+          match update_PTE_Bits(Mk_PTE_Bits(pte.BITS()), ac) {
+            None() => {
+              addToTLB39(asid, vAddr, pAddr, pte, pteAddr, level, global);
+              TR39_Address(pAddr)
+            },
+            Some(pbits) =>
+              if ~ (enable_dirty_update)
+              then TR39_Failure(PTW_PTE_Update)
+              else {
+                w_pte : SV39_PTE = update_BITS(pte, pbits.bits());
+                match checked_mem_write(EXTZ(pteAddr), 8, w_pte.bits()) {
+                  MemValue(_) => {
+                    addToTLB39(asid, vAddr, pAddr, w_pte, pteAddr, level, global);
+                    TR39_Address(pAddr)
+                  },
+                  MemException(e) => TR39_Failure(PTW_Access)
+                }
+              }
+          }
+        }
+      }
+    }
+  }
+}
+
+/* Address translation mode */
+
+val translationMode : (Privilege) -> SATPMode effect {rreg, escape}
+function translationMode(priv) = {
+  if priv == Machine then Sbare
+  else {
+    let arch = architecture(mstatus.SXL());
+    match arch {
+      Some(RV64) => {
+        let mbits : satp_mode = Mk_Satp64(satp).Mode();
+        match satpMode_of_bits(RV64, mbits) {
+          Some(m) => m,
+          None()  => internal_error("invalid RV64 translation mode in satp")
+        }
+      },
+      _    => internal_error("unsupported address translation arch")
+    }
+  }
+}
+
+union TR_Result = {
+  TR_Address : xlenbits,
+  TR_Failure : ExceptionType
+}
+
+/* Top-level address translation dispatcher */
+
+val translateAddr : (xlenbits, AccessType, ReadType) -> TR_Result effect {escape, rmem, rreg, wmv, wreg}
+function translateAddr(vAddr, ac, rt) = {
+  let effPriv : Privilege = match rt {
+    Instruction => cur_privilege,
+    Data => if mstatus.MPRV() == true
+            then privLevel_of_bits(mstatus.MPP())
+            else cur_privilege
+  };
+  let mxr : bool = mstatus.MXR() == true;
+  let sum : bool = mstatus.SUM() == true;
+  let mode : SATPMode = translationMode(effPriv);
+  match mode {
+    Sbare => TR_Address(vAddr),
+    SV39  => match translate39(vAddr[38 .. 0], ac, effPriv, mxr, sum, SV39_LEVELS - 1) {
+               TR39_Address(pa) => TR_Address(EXTZ(pa)),
+               TR39_Failure(f)  => TR_Failure(translationException(ac, f))
+             },
+    _     => internal_error("unsupported address translation scheme")
+  }
+}