Pull out the Sv39 and its TLB into separate files.

5 files changed, 226 insertions, 216 deletions

diff --git a/Makefile b/Makefile
index 050cc90..2c980bf 100644
--- a/Makefile
+++ b/Makefile
@@ -7,7 +7,7 @@ SAIL_RMEM_INST_SRCS = riscv_insts_begin.sail $(SAIL_RMEM_INST) riscv_insts_end.s
 
 SAIL_SYS_SRCS = riscv_csr_map.sail riscv_sys_regs.sail riscv_next_regs.sail riscv_next_control.sail riscv_sys_control.sail
 
-SAIL_VM_SRCS = riscv_vmem_common.sail riscv_vmem.sail
+SAIL_VM_SRCS = riscv_vmem_common.sail riscv_vmem_tlb.sail riscv_vmem_sv39.sail riscv_vmem.sail
 
 # non-instruction sources
 PRELUDE = prelude.sail prelude_mapping.sail riscv_xlen.sail prelude_mem.sail
diff --git a/model/riscv_vmem.sail b/model/riscv_vmem.sail
index 085024c..33f94dd 100644
--- a/model/riscv_vmem.sail
+++ b/model/riscv_vmem.sail
@@ -1,149 +1,13 @@
 /* RV64 Supervisor-mode address translation and page-table walks. */
 
+/* Define the architectural satp and its legalizer. */
+
 register satp : xlenbits
 
 function legalize_satp(a : Architecture, o : xlenbits, v : xlenbits) -> xlenbits =
   legalize_satp64(a, o, v)
 
-val walk39 : (vaddr39, AccessType, Privilege, bool, bool, paddr64, nat, bool) -> PTW_Result(paddr64, SV39_PTE) effect {rmem, escape}
-function walk39(vaddr, ac, priv, mxr, do_sum, ptb, level, global) = {
-  let va = Mk_SV39_Vaddr(vaddr);
-  let pt_ofs : paddr64 = shiftl(EXTZ(shiftr(va.VPNi(), (level * SV39_LEVEL_BITS))[(SV39_LEVEL_BITS - 1) .. 0]),
-                                PTE39_LOG_SIZE);
-  let pte_addr = ptb + pt_ofs;
-  /* FIXME: we assume here that walks only access physical-memory-backed addresses, and not MMIO regions. */
-  match (phys_mem_read(Data, EXTZ(pte_addr), xlen_bytes, false, false, false)) {
-    MemException(_) => {
-/*    print("walk39(vaddr=" ^ BitStr(vaddr) ^ " level=" ^ string_of_int(level)
-            ^ " pt_base=" ^ BitStr(ptb)
-            ^ " pt_ofs=" ^ BitStr(pt_ofs)
-            ^ " pte_addr=" ^ BitStr(pte_addr)
-            ^ ": invalid pte address"); */
-      PTW_Failure(PTW_Access)
-    },
-    MemValue(v) => {
-      let pte = Mk_SV39_PTE(v);
-      let pbits = pte.BITS();
-      let pattr = Mk_PTE_Bits(pbits);
-      let is_global = global | (pattr.G() == true);
-/*    print("walk39(vaddr=" ^ BitStr(vaddr) ^ " level=" ^ string_of_int(level)
-            ^ " pt_base=" ^ BitStr(ptb)
-            ^ " pt_ofs=" ^ BitStr(pt_ofs)
-            ^ " pte_addr=" ^ BitStr(pte_addr)
-            ^ " pte=" ^ BitStr(v)); */
-      if isInvalidPTE(pbits) then {
-/*      print("walk39: invalid pte"); */
-        PTW_Failure(PTW_Invalid_PTE)
-      } else {
-        if isPTEPtr(pbits) then {
-          if level == 0 then {
-            /* last-level PTE contains a pointer instead of a leaf */
-/*          print("walk39: last-level pte contains a ptr"); */
-            PTW_Failure(PTW_Invalid_PTE)
-          } else {
-            /* walk down the pointer to the next level */
-            walk39(vaddr, ac, priv, mxr, do_sum, EXTZ(shiftl(pte.PPNi(), PAGESIZE_BITS)), level - 1, is_global)
-          }
-        } else { /* leaf PTE */
-          if ~ (checkPTEPermission(ac, priv, mxr, do_sum, pattr)) then {
-/*          print("walk39: pte permission check failure"); */
-            PTW_Failure(PTW_No_Permission)
-          } else {
-            if level > 0 then { /* superpage */
-              /* fixme hack: to get a mask of appropriate size */
-              let mask = shiftl(pte.PPNi() ^ pte.PPNi() ^ EXTZ(0b1), level * SV39_LEVEL_BITS) - 1;
-              if (pte.PPNi() & mask) != EXTZ(0b0) then {
-                /* misaligned superpage mapping */
-/*              print("walk39: misaligned superpage mapping"); */
-                PTW_Failure(PTW_Misaligned)
-              } else {
-                /* add the appropriate bits of the VPN to the superpage PPN */
-                let ppn = pte.PPNi() | (EXTZ(va.VPNi()) & mask);
-/*              let res = append(ppn, va.PgOfs());
-                print("walk39: using superpage: pte.ppn=" ^ BitStr(pte.PPNi())
-                      ^ " ppn=" ^ BitStr(ppn) ^ " res=" ^ BitStr(res)); */
-                PTW_Success(append(ppn, va.PgOfs()), pte, pte_addr, level, is_global)
-              }
-            } else {
-              /* normal leaf PTE */
-/*            let res = append(pte.PPNi(), va.PgOfs());
-              print("walk39: pte.ppn=" ^ BitStr(pte.PPNi()) ^ " ppn=" ^ BitStr(pte.PPNi()) ^ " res=" ^ BitStr(res)); */
-              PTW_Success(append(pte.PPNi(), va.PgOfs()), pte, pte_addr, level, is_global)
-            }
-          }
-        }
-      }
-    }
-  }
-}
-
-val translate39 : (vaddr39, AccessType, Privilege, bool, bool, nat) -> TR_Result(paddr64, PTW_Error) effect {rreg, wreg, wmv, escape, rmem}
-function translate39(vAddr, ac, priv, mxr, do_sum, level) = {
-  let asid = curAsid64(satp);
-  match lookupTLB39(asid, vAddr) {
-    Some(idx, ent) => {
-      let pteBits = Mk_PTE_Bits(ent.pte.BITS());
-      if ~ (checkPTEPermission(ac, priv, mxr, do_sum, pteBits))
-      then TR_Failure(PTW_No_Permission)
-      else {
-        match update_PTE_Bits(pteBits, ac) {
-          None() => TR_Address(ent.pAddr | EXTZ(vAddr & ent.vAddrMask)),
-          Some(pbits) => {
-            if ~ (plat_enable_dirty_update ())
-            then {
-              /* pte needs dirty/accessed update but that is not enabled */
-              TR_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), xlen_bytes, ent.pte.bits(), false, false, false) {
-                MemValue(_) => (),
-                MemException(e) => internal_error("invalid physical address in TLB")
-              };
-              TR_Address(ent.pAddr | EXTZ(vAddr & ent.vAddrMask))
-            }
-          }
-        }
-      }
-    },
-    None() => {
-      match walk39(vAddr, ac, priv, mxr, do_sum, curPTB64(satp), 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) {
-            None() => {
-              addToTLB39(asid, vAddr, pAddr, pte, pteAddr, level, global);
-              TR_Address(pAddr)
-            },
-            Some(pbits) =>
-              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());
-                match checked_mem_write(EXTZ(pteAddr), xlen_bytes, w_pte.bits(), false, false, false) {
-                  MemValue(_) => {
-                    addToTLB39(asid, vAddr, pAddr, w_pte, pteAddr, level, global);
-                    TR_Address(pAddr)
-                  },
-                  MemException(e) => {
-                    /* pte is not in valid memory */
-                    TR_Failure(PTW_Access)
-                  }
-                }
-              }
-          }
-        }
-      }
-    }
-  }
-}
-
-/* Address translation mode */
+/* Compute the address translation mode. */
 
 val translationMode : (Privilege) -> SATPMode effect {rreg, escape}
 function translationMode(priv) = {
@@ -180,9 +44,13 @@ function translateAddr(vAddr, ac, rt) = {
   let mxr    : bool   = mstatus.MXR() == true;
   let do_sum : bool   = mstatus.SUM() == true;
   let mode : SATPMode = translationMode(effPriv);
+
+  let asid = curAsid64(satp);
+  let ptb  = curPTB64(satp);
+
   match mode {
     Sbare => TR_Address(vAddr),
-    SV39  => match translate39(vAddr[38 .. 0], ac, effPriv, mxr, do_sum, SV39_LEVELS - 1) {
+    SV39  => match translate39(asid, ptb, vAddr[38 .. 0], ac, effPriv, mxr, do_sum, SV39_LEVELS - 1) {
                TR_Address(pa) => TR_Address(EXTZ(pa)),
                TR_Failure(f)  => TR_Failure(translationException(ac, f))
              },
diff --git a/model/riscv_vmem_common.sail b/model/riscv_vmem_common.sail
index 37f4785..0e53fb8 100644
--- a/model/riscv_vmem_common.sail
+++ b/model/riscv_vmem_common.sail
@@ -237,78 +237,3 @@ union TR_Result('paddr : Type, 'failure : Type) = {
   TR_Address : 'paddr,
   TR_Failure : 'failure
 }
-
-/* idealized TLB to model fence.vm and also speed up simulation. */
-
-struct TLB39_Entry = {
-  asid : asid64,
-  global : bool,
-  vAddr : vaddr39,      /* VPN */
-  pAddr : paddr64,      /* PPN */
-  vMatchMask : vaddr39, /* matching mask for superpages */
-  vAddrMask : vaddr39,  /* selection mask for superpages */
-  pte : SV39_PTE,       /* permissions */
-  pteAddr : paddr64,    /* 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, paddr64, SV39_PTE, nat, paddr64) -> 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, paddr64, SV39_PTE, paddr64, 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
-}
diff --git a/model/riscv_vmem_sv39.sail b/model/riscv_vmem_sv39.sail
new file mode 100644
index 0000000..90b2b47
--- /dev/null
+++ b/model/riscv_vmem_sv39.sail
@@ -0,0 +1,139 @@
+/* Sv39 address translation for RV64. */
+
+val walk39 : (vaddr39, AccessType, Privilege, bool, bool, paddr64, nat, bool) -> PTW_Result(paddr64, SV39_PTE) effect {rmem, escape}
+function walk39(vaddr, ac, priv, mxr, do_sum, ptb, level, global) = {
+  let va = Mk_SV39_Vaddr(vaddr);
+  let pt_ofs : paddr64 = shiftl(EXTZ(shiftr(va.VPNi(), (level * SV39_LEVEL_BITS))[(SV39_LEVEL_BITS - 1) .. 0]),
+                                PTE39_LOG_SIZE);
+  let pte_addr = ptb + pt_ofs;
+  /* FIXME: we assume here that walks only access physical-memory-backed addresses, and not MMIO regions. */
+  match (phys_mem_read(Data, EXTZ(pte_addr), 8, false, false, false)) {
+    MemException(_) => {
+/*    print("walk39(vaddr=" ^ BitStr(vaddr) ^ " level=" ^ string_of_int(level)
+            ^ " pt_base=" ^ BitStr(ptb)
+            ^ " pt_ofs=" ^ BitStr(pt_ofs)
+            ^ " pte_addr=" ^ BitStr(pte_addr)
+            ^ ": invalid pte address"); */
+      PTW_Failure(PTW_Access)
+    },
+    MemValue(v) => {
+      let pte = Mk_SV39_PTE(v);
+      let pbits = pte.BITS();
+      let pattr = Mk_PTE_Bits(pbits);
+      let is_global = global | (pattr.G() == true);
+/*    print("walk39(vaddr=" ^ BitStr(vaddr) ^ " level=" ^ string_of_int(level)
+            ^ " pt_base=" ^ BitStr(ptb)
+            ^ " pt_ofs=" ^ BitStr(pt_ofs)
+            ^ " pte_addr=" ^ BitStr(pte_addr)
+            ^ " pte=" ^ BitStr(v)); */
+      if isInvalidPTE(pbits) then {
+/*      print("walk39: invalid pte"); */
+        PTW_Failure(PTW_Invalid_PTE)
+      } else {
+        if isPTEPtr(pbits) then {
+          if level == 0 then {
+            /* last-level PTE contains a pointer instead of a leaf */
+/*          print("walk39: last-level pte contains a ptr"); */
+            PTW_Failure(PTW_Invalid_PTE)
+          } else {
+            /* walk down the pointer to the next level */
+            walk39(vaddr, ac, priv, mxr, do_sum, EXTZ(shiftl(pte.PPNi(), PAGESIZE_BITS)), level - 1, is_global)
+          }
+        } else { /* leaf PTE */
+          if ~ (checkPTEPermission(ac, priv, mxr, do_sum, pattr)) then {
+/*          print("walk39: pte permission check failure"); */
+            PTW_Failure(PTW_No_Permission)
+          } else {
+            if level > 0 then { /* superpage */
+              /* fixme hack: to get a mask of appropriate size */
+              let mask = shiftl(pte.PPNi() ^ pte.PPNi() ^ EXTZ(0b1), level * SV39_LEVEL_BITS) - 1;
+              if (pte.PPNi() & mask) != EXTZ(0b0) then {
+                /* misaligned superpage mapping */
+/*              print("walk39: misaligned superpage mapping"); */
+                PTW_Failure(PTW_Misaligned)
+              } else {
+                /* add the appropriate bits of the VPN to the superpage PPN */
+                let ppn = pte.PPNi() | (EXTZ(va.VPNi()) & mask);
+/*              let res = append(ppn, va.PgOfs());
+                print("walk39: using superpage: pte.ppn=" ^ BitStr(pte.PPNi())
+                      ^ " ppn=" ^ BitStr(ppn) ^ " res=" ^ BitStr(res)); */
+                PTW_Success(append(ppn, va.PgOfs()), pte, pte_addr, level, is_global)
+              }
+            } else {
+              /* normal leaf PTE */
+/*            let res = append(pte.PPNi(), va.PgOfs());
+              print("walk39: pte.ppn=" ^ BitStr(pte.PPNi()) ^ " ppn=" ^ BitStr(pte.PPNi()) ^ " res=" ^ BitStr(res)); */
+              PTW_Success(append(pte.PPNi(), va.PgOfs()), pte, pte_addr, level, is_global)
+            }
+          }
+        }
+      }
+    }
+  }
+}
+
+val translate39 : (asid64, paddr64, vaddr39, AccessType, Privilege, bool, bool, nat) -> TR_Result(paddr64, PTW_Error) effect {rreg, wreg, wmv, escape, rmem}
+function translate39(asid, ptb, vAddr, ac, priv, mxr, do_sum, level) = {
+  match lookupTLB39(asid, vAddr) {
+    Some(idx, ent) => {
+      let pteBits = Mk_PTE_Bits(ent.pte.BITS());
+      if ~ (checkPTEPermission(ac, priv, mxr, do_sum, pteBits))
+      then TR_Failure(PTW_No_Permission)
+      else {
+        match update_PTE_Bits(pteBits, ac) {
+          None() => TR_Address(ent.pAddr | EXTZ(vAddr & ent.vAddrMask)),
+          Some(pbits) => {
+            if ~ (plat_enable_dirty_update ())
+            then {
+              /* pte needs dirty/accessed update but that is not enabled */
+              TR_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(), false, false, false) {
+                MemValue(_) => (),
+                MemException(e) => internal_error("invalid physical address in TLB")
+              };
+              TR_Address(ent.pAddr | EXTZ(vAddr & ent.vAddrMask))
+            }
+          }
+        }
+      }
+    },
+    None() => {
+      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) {
+            None() => {
+              addToTLB39(asid, vAddr, pAddr, pte, pteAddr, level, global);
+              TR_Address(pAddr)
+            },
+            Some(pbits) =>
+              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());
+                match checked_mem_write(EXTZ(pteAddr), 8, w_pte.bits(), false, false, false) {
+                  MemValue(_) => {
+                    addToTLB39(asid, vAddr, pAddr, w_pte, pteAddr, level, global);
+                    TR_Address(pAddr)
+                  },
+                  MemException(e) => {
+                    /* pte is not in valid memory */
+                    TR_Failure(PTW_Access)
+                  }
+                }
+              }
+          }
+        }
+      }
+    }
+  }
+}
+
diff --git a/model/riscv_vmem_tlb.sail b/model/riscv_vmem_tlb.sail
new file mode 100644
index 0000000..5e6b128
--- /dev/null
+++ b/model/riscv_vmem_tlb.sail
@@ -0,0 +1,78 @@
+/* idealized TLB to model fence.vm and also speed up simulation. */
+
+/* This could be made generic using polymorphic structs; however,
+ * the simulator backends don't support them.
+ */
+
+struct TLB39_Entry = {
+  asid : asid64,
+  global : bool,
+  vAddr : vaddr39,      /* VPN */
+  pAddr : paddr64,      /* PPN */
+  vMatchMask : vaddr39, /* matching mask for superpages */
+  vAddrMask : vaddr39,  /* selection mask for superpages */
+  pte : SV39_PTE,       /* permissions */
+  pteAddr : paddr64,    /* 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, paddr64, SV39_PTE, nat, paddr64) -> 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, paddr64, SV39_PTE, paddr64, 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
+}