Unify VM code

Old vmem code had much 'cut-and-paste' replication for RV32 (Sv32) and (#408)

RV64 (Sv39, Sv48), and was scattered over several files.

New code unifies them into single set of parameterized functions
that works for RV32/RV64 and Sv32/Sv39/Sv48 (and is ready for Sv57).

Deleted old files:
    riscv_vmem_rv32.sail    riscv_vmem_rv64.sail
    riscv_vmem_sv32.sail    riscv_vmem_sv39.sail    riscv_vmem_sv48.sail
    riscv_pte.sail
    riscv_ptw.sail

Current files: all named riscv_vmem_*
    riscv_vmem.sail    (root file for vmem)
    riscv_vmem_common.sail
    riscv_vmem_pte.sail
    riscv_vmem_ptw.sail
    riscv_vmem_tlb.sail
    riscv_vmem_types.sail

Modified top-level Makefile accordingly.

Added documentation on new vmem code: doc/notes_Virtual_Memory.adoc

1 files changed, 452 insertions, 0 deletions

diff --git a/model/riscv_vmem.sail b/model/riscv_vmem.sail
new file mode 100644
index 0000000..2d1e5d1
--- /dev/null
+++ b/model/riscv_vmem.sail
@@ -0,0 +1,452 @@
+/*=======================================================================================*/
+/*  This Sail RISC-V architecture model, comprising all files and                        */
+/*  directories except where otherwise noted is subject the BSD                          */
+/*  two-clause license in the LICENSE file.                                              */
+/*                                                                                       */
+/*  SPDX-License-Identifier: BSD-2-Clause                                                */
+/*=======================================================================================*/
+
+// ****************************************************************
+// Virtual memory address translation and memory protection,
+// including PTWs (Page Table Walks) and TLBs (Translation Look-aside Buffers)
+// Supported VM modes: Sv32, Sv39, Sv48.  TODO: Sv57
+
+// STYLE NOTES:
+//   PRIVATE items are used only within this VM code.
+//   PUBLIC  items are invoked from other parts of sail-riscv.
+
+// TLB NOTE:
+// TLBs are not part of the RISC-V architecture specification.
+// However, we model a simple TLB so that
+// (1) we can meaningfully test SFENCE.VMA which is a no-op wihout TLBs;
+// (2) we can greatly speed up simulation speed
+//     (e.g., from 10s or minutes to few minutes for Linux boot)
+// The TLB implementation is in a separate file: riscv_vmem_tlb.sail
+// The code in this file is structured and commented so you can easily
+// ignore TLB functionality at first reading.
+
+// ****************************************************************
+// Fields of virtual addresses
+
+// PRIVATE: Extract full VPN field from VA
+function vpns_of_va(sv_params : SV_Params,
+                    va        : bits(64)) -> bits(64) = {
+  let mask : bits(64) = zero_extend(ones(sv_params.va_size_bits));
+  (va & mask) >> pagesize_bits
+}
+
+// PRIVATE: Extract VPN[level] from  VA
+function vpn_j_of_va(sv_params : SV_Params,
+                     va        : bits(64),
+                     level     : PTW_Level) -> bits(64) = {
+  let lsb  : range(0,63) = pagesize_bits + level * sv_params.vpn_size_bits;
+  assert (lsb < sizeof(xlen));
+  let mask : bits(64) = zero_extend(ones(sv_params.vpn_size_bits));
+  ((va >> lsb) & mask)
+}
+
+// PRIVATE: Extract offset within page from VA
+function offset_of_va(va : bits(64)) -> bits(PAGESIZE_BITS) = va[pagesize_bits - 1 .. 0]
+
+// Valid xlen-wide values containing virtual addrs must have upper
+// bits equal to the MSB of the virtual address.
+// Virtual address widths depend on the virtual memory mode.
+// PRIVATE
+function is_valid_vAddr(struct { va_size_bits, _ } : SV_Params,
+                        vAddr                      : bits(64)) -> bool =
+ vAddr == sign_extend(vAddr[va_size_bits - 1 .. 0])
+
+// ****************************************************************
+// Results of Page Table Walk (PTW)
+
+// PRIVATE
+union PTW_Result = {
+  PTW_Success: (bits(64), bits(64), bits(64), nat, bool, ext_ptw),
+  PTW_Failure: (PTW_Error, ext_ptw)
+}
+
+// ****************************************************************
+// Page Table Walk (PTW)
+
+// Note: 'pt_walk()' is recursive => needs separate 'val' decls
+
+// PRIVATE
+val pt_walk : (SV_Params,
+               bits(64),                     // virtual addr
+               AccessType(ext_access_type),  // Read/Write/ReadWrite/Execute
+               Privilege,                    // User/Supervisor/Machine
+               bool,                         // mstatus.MXR
+               bool,                         // do_sum
+               bits(64),                     // PT base addr
+               PTW_Level,                    // tree level for this recursive call
+               bool,                         // global translation,
+               ext_ptw)                      // ext_ptw
+              -> PTW_Result
+
+function pt_walk(sv_params,
+                 va,
+                 ac,
+                 priv,
+                 mxr,
+                 do_sum,
+                 pt_base,
+                 level,
+                 global,
+                 ext_ptw) = {
+  let vpn_j      = vpn_j_of_va(sv_params, va, level);
+  let pte_offset = vpn_j << sv_params.log_pte_size_bytes;
+  let pte_addr   = pt_base + pte_offset;
+
+  // In Sv32, physical addrs are actually 34 bits, not XLEN(=32) bits.
+  // Below, 'pte_phys_addr' is XLEN bits because it's an arg to
+  // 'mem_read_priv()' [riscv_mem.sail] where it's declared as xlenbits.
+  // That def and this use need to be fixed together (TODO)
+  let pte_phys_addr : xlenbits = pte_addr[(sizeof(xlen) - 1) .. 0];
+
+  // Read this-level PTE from mem
+  let mem_result = mem_read_priv(Read(Data),              // AccessType
+                                 Supervisor,              // Privilege
+                                 pte_phys_addr,
+                                 8,                       // atom (8)
+                                 false,                   // aq
+                                 false,                   // rl
+                                 false);                  // res
+
+  match mem_result {
+    MemException(_) => PTW_Failure(PTW_Access(), ext_ptw),
+    MemValue(pte)   => {
+      let pte_flags = Mk_PTE_Flags(pte[7 .. 0]);
+      if pte_is_invalid(pte_flags) then
+        PTW_Failure(PTW_Invalid_PTE(), ext_ptw)
+      else {
+        let ppns : bits(64) = PPNs_of_PTE(sv_params, pte);
+        let global'         = global | (pte_flags[G] == 0b1);
+        if pte_is_ptr(pte_flags) then {
+          // Non-Leaf PTE
+          if level > 0 then {
+            // follow the pointer to walk next level
+            let pt_base' : bits(64) = ppns << pagesize_bits;
+            let level'              = level - 1;
+            pt_walk(sv_params, va, ac, priv, mxr, do_sum,
+                    pt_base', level', global', ext_ptw)
+          }
+          else
+            // level 0 PTE, but contains a pointer instead of a leaf
+            PTW_Failure(PTW_Invalid_PTE(), ext_ptw)
+        }
+        else {
+          // Leaf PTE
+          let ext_pte   = msbs_of_PTE(sv_params, pte);
+          let pte_check = check_PTE_permission(ac, priv, mxr, do_sum, pte_flags,
+                                               ext_pte, ext_ptw);
+          match pte_check {
+            PTE_Check_Failure(ext_ptw, ext_ptw_fail) =>
+              PTW_Failure(ext_get_ptw_error(ext_ptw_fail), ext_ptw),
+            PTE_Check_Success(ext_ptw) =>
+              if level > 0 then {
+                // Superpage; construct mask for lower-level PPNs from the PTE
+                let mask_bits = level * sv_params.pte_PPN_j_size_bits;
+                // Clear the lowest `mask_bits` bits.
+                let ppns_masked = (ppns >> mask_bits) << mask_bits;
+                if not(ppns == ppns_masked) then
+                  // misaligned superpage mapping
+                  PTW_Failure(PTW_Misaligned(), ext_ptw)
+                else {
+                  // Compose final PA in superpage:
+                  // Superpage PPN + lower VPNs + pagesize_bits page-offset
+                  let mask : bits(64) = ~ (ones() << mask_bits);
+                  let ppn = ppns | (vpns_of_va(sv_params, va) & mask);
+                  let pa  = (ppn << pagesize_bits) | zero_extend(offset_of_va(va));
+                  PTW_Success(pa, pte, pte_addr, level, global', ext_ptw)
+                }
+              }
+              else {
+                let pa = (ppns << pagesize_bits) | zero_extend(offset_of_va(va));
+                PTW_Success(pa, pte, pte_addr, level, global', ext_ptw)
+              }
+          }
+        }
+      }
+    }
+  }
+}
+
+// ****************************************************************
+// Architectural SATP CSR
+
+// PUBLIC: see also riscv_insts_zicsr.sail and other CSR-related files
+register satp : xlenbits
+
+// See riscv_sys_regs.sail for legalize_satp{32,64}().
+// WARNING: those functions legalize Mode but not ASID?
+// PUBLIC: invoked from writeCSR() to fixup WARL fields
+function legalize_satp(a : Architecture,
+                       o : xlenbits,        // previous value of satp
+                       v : xlenbits)        // proposed new value of satp
+                      -> xlenbits = {       // new legal value of satp
+  if sizeof(xlen) == 32 then {
+    // The slice and extend ops below are no-ops when xlen==32,
+    // but appease the type-checker when xlen==64 (when this code is not executed!)
+    let o32      : bits(32) = o[31 .. 0];
+    let v32      : bits(32) = v[31 .. 0];
+    let new_satp : bits(32) = legalize_satp32(a, o32, v32);
+    zero_extend(new_satp);
+  } else if sizeof(xlen) == 64 then {
+    // The extend and truncate ops below are no-ops when xlen==64,
+    // but appease the type-checker when xlen==32 (when this code is not executed!)
+    let o64      : bits(64) = zero_extend(o);
+    let v64      : bits(64) = zero_extend(v);
+    let new_satp : bits(64) = legalize_satp64(a, o64, v64);
+    truncate(new_satp, sizeof(xlen))
+  } else
+    internal_error(__FILE__, __LINE__, "Unsupported xlen" ^ dec_str(sizeof(xlen)))
+}
+
+// ----------------
+// Fields of SATP
+
+// ASID is 9b in Sv32, 16b in Sv39/Sv48/Sv57: we use 16b for both
+// PRIVATE
+function satp_to_asid(satp_val : xlenbits) -> asidbits =
+   if      sizeof(xlen) == 32 then zero_extend(Mk_Satp32(satp_val)[Asid])
+   else if sizeof(xlen) == 64 then Mk_Satp64(satp_val)[Asid]
+   else internal_error(__FILE__, __LINE__,
+                       "Unsupported xlen" ^ dec_str(sizeof(xlen)))
+
+// Result is 64b to cover both RV32 and RV64 addrs
+// PRIVATE
+function satp_to_PT_base(satp_val : xlenbits) -> bits(64) = {
+  let ppn = if      sizeof(xlen) == 32 then zero_extend (64, Mk_Satp32(satp_val)[PPN])
+            else if sizeof(xlen) == 64 then zero_extend (64, Mk_Satp64(satp_val)[PPN])
+            else internal_error(__FILE__, __LINE__,
+                                "Unsupported xlen" ^ dec_str(sizeof(xlen)));
+  ppn << pagesize_bits
+}
+
+// Compute address translation mode from SATP register
+// PRIVATE
+function translationMode(priv : Privilege) -> SATPMode = {
+  if priv == Machine then
+    Sbare
+  else if sizeof(xlen) == 32 then
+    match Mk_Satp32(satp)[Mode] {
+      0b0 => Sbare,
+      0b1  => Sv32
+    }
+  else if sizeof(xlen) == 64 then {
+    // Translation mode is based on mstatus.SXL, which could be RV32 when xlen==64
+    let arch = architecture(get_mstatus_SXL(mstatus));
+    match arch {
+      Some(RV64) => { let mbits : bits(4) = satp[63 .. 60];
+                      match satp64Mode_of_bits(RV64, mbits) {    // see riscv_types.sail
+                        Some(m) => m,
+                        None()  => internal_error(__FILE__, __LINE__,
+                                                  "invalid RV64 translation mode in satp")
+                      }
+                    },
+      Some(RV32) => match Mk_Satp32(satp[31 .. 0])[Mode] {    // Note: satp is 64bits here
+                      // When xlen is 64, mstatus.SXL (for S privilege) can be RV32
+                      0b0 => Sbare,
+                      0b1  => Sv32
+                    },
+      _    => internal_error(__FILE__, __LINE__, "unsupported address translation arch")
+    }
+  }
+  else
+    internal_error(__FILE__, __LINE__, "unsupported xlen")
+}
+
+// ****************************************************************
+// VA to PA translation
+
+// Result of address translation
+
+// PUBLIC
+union TR_Result('paddr : Type, 'failure : Type) = {
+  TR_Address : ('paddr, ext_ptw),
+  TR_Failure : ('failure, ext_ptw)
+}
+
+// This function can be ignored on first reading since TLBs are not
+// part of RISC-V architecture spec (see TLB_NOTE above).
+// PRIVATE: translate on TLB hit, and maintenance of PTE in TLB
+function translate_TLB_hit(sv_params : SV_Params,
+                           asid      : asidbits,
+                           ptb       : bits(64),
+                           vAddr     : bits(64),
+                           ac        : AccessType(ext_access_type),
+                           priv      : Privilege,
+                           mxr       : bool,
+                           do_sum    : bool,
+                           ext_ptw   : ext_ptw,
+                           tlb_index : nat,
+                           ent       : TLB_Entry)
+                          -> TR_Result(bits(64), PTW_Error) = {
+  let pte       = ent.pte;
+  let ext_pte   = msbs_of_PTE(sv_params, pte);
+  let pte_flags = Mk_PTE_Flags(pte[7 .. 0]);
+  let pte_check = check_PTE_permission(ac, priv, mxr, do_sum, pte_flags,
+                                       ext_pte,
+                                       ext_ptw);
+  match pte_check {
+    PTE_Check_Failure(ext_ptw, ext_ptw_fail) =>
+      TR_Failure(ext_get_ptw_error(ext_ptw_fail), ext_ptw),
+    PTE_Check_Success(ext_ptw) =>
+      match update_PTE_Bits(sv_params, pte, ac) {
+        None()     => TR_Address(ent.pAddr | (vAddr & ent.vAddrMask), ext_ptw),
+        Some(pte') =>
+          // See riscv_platform.sail
+          if not(plat_enable_dirty_update()) then
+            // pte needs dirty/accessed update but that is not enabled
+            TR_Failure(PTW_PTE_Update(), ext_ptw)
+          else {
+            // Writeback the PTE (which has new A/D bits)
+            let n_ent = {ent with pte=pte'};
+            write_TLB(tlb_index, n_ent);
+            let pte_phys_addr = ent.pteAddr[(sizeof(xlen) - 1) .. 0];
+            let mv = mem_write_value_priv(pte_phys_addr,
+                                          8,
+                                          pte',
+                                          Supervisor,
+                                          false,
+                                          false,
+                                          false);
+            match mv {
+              MemValue(_)     => (),
+              MemException(e) => internal_error(__FILE__, __LINE__,
+                                                "invalid physical address in TLB")
+            };
+            TR_Address(ent.pAddr | (vAddr & ent.vAddrMask), ext_ptw)
+          }
+      }
+  }
+}
+
+// PRIVATE: translate on TLB miss (do a page-table walk)
+function translate_TLB_miss(sv_params : SV_Params,
+                            asid      : asidbits,
+                            ptb       : bits(64),
+                            vAddr     : bits(64),
+                            ac        : AccessType(ext_access_type),
+                            priv      : Privilege,
+                            mxr       : bool,
+                            do_sum    : bool,
+                            ext_ptw   : ext_ptw) -> TR_Result(bits(64), PTW_Error) = {
+  let initial_level = sv_params.levels - 1;
+  let ptw_result    = pt_walk(sv_params, vAddr, ac, priv, mxr, do_sum,
+                              ptb, initial_level, false, ext_ptw);
+  match ptw_result {
+    PTW_Failure(f, ext_ptw) => TR_Failure(f, ext_ptw),
+    PTW_Success(pAddr, pte, pteAddr, level, global, ext_ptw) => {
+      let ext_pte   = msbs_of_PTE(sv_params, pte);
+      // Without TLBs, this 'match' expression can be replaced simply
+      // by: 'TR_Address(pAddr, ext_ptw)'    (see TLB_NOTE above)
+      match update_PTE_Bits(sv_params, pte, ac) {
+        None() => {
+          add_to_TLB(asid, vAddr, pAddr, pte, pteAddr, level, global,
+                     sv_params.vpn_size_bits,
+                     pagesize_bits);
+          TR_Address(pAddr, ext_ptw)
+        },
+        Some(pte') =>
+          // See riscv_platform.sail
+          if not(plat_enable_dirty_update()) then
+            // pte needs dirty/accessed update but that is not enabled
+            TR_Failure(PTW_PTE_Update(), ext_ptw)
+          else {
+            // Writeback the PTE (which has new A/D bits)
+            let pte_phys_addr = pteAddr[(sizeof(xlen) - 1) .. 0];
+            let mv = mem_write_value_priv(pte_phys_addr, // pteAddr,
+                                          8,
+                                          pte',
+                                          Supervisor,
+                                          false,
+                                          false,
+                                          false);
+            match mv {
+              MemValue(_) => {
+                add_to_TLB(asid, vAddr, pAddr, pte', pteAddr, level, global,
+                           sv_params.vpn_size_bits,
+                           pagesize_bits);
+                TR_Address(pAddr, ext_ptw)
+              },
+              MemException(e) =>
+                TR_Failure(PTW_Access(), ext_ptw)
+            }
+          }
+        }
+      }
+    }
+}
+
+// PRIVATE
+function translate(sv_params : SV_Params,
+                   asid      : asidbits,
+                   ptb       : bits(64),
+                   vAddr_arg : bits(64),
+                   ac        : AccessType(ext_access_type),
+                   priv      : Privilege,
+                   mxr       : bool,
+                   do_sum    : bool,
+                   ext_ptw   : ext_ptw)
+                  -> TR_Result(bits(64), PTW_Error) = {
+  let va_mask : bits(64) = zero_extend(ones(sv_params.va_size_bits));
+  let vAddr              = (vAddr_arg & va_mask);
+
+  // On first reading, assume lookup_TLB returns None(), since TLBs
+  // are not part of RISC-V archticture spec (see TLB_NOTE above)
+  match lookup_TLB(asid, vAddr) {
+    Some(index, ent) => translate_TLB_hit(sv_params, asid, ptb, vAddr, ac, priv,
+                                          mxr, do_sum, ext_ptw, index, ent),
+    None()           => translate_TLB_miss(sv_params, asid, ptb, vAddr, ac, priv,
+                                           mxr, do_sum, ext_ptw)
+  }
+}
+
+// Top-level addr-translation function
+// PUBLIC: invoked from instr-fetch and load/store/amo
+function translateAddr(vAddr   : xlenbits,
+                       ac      : AccessType(ext_access_type))
+                      -> TR_Result(xlenbits, ExceptionType) = {
+  // Internally the vmem code works with 64-bit values, whether xlen==32 or xlen==64
+  // This 'extend' is a no-op when xlen==64 and extends when xlen==32
+  let vAddr_64b : bits(64) = zero_extend(vAddr);
+  // Effective privilege takes into account mstatus.PRV, mstatus.MPP
+  // See riscv_sys_regs.sail for effectivePrivilege() and cur_privilege
+  let effPriv   : Privilege = effectivePrivilege(ac, mstatus, cur_privilege);
+  let mode      : SATPMode  = translationMode(effPriv);
+  let (valid_va, sv_params) : (bool, SV_Params) = match mode {
+    Sbare => return TR_Address(vAddr, init_ext_ptw),
+    Sv32  => (true,                                 sv32_params),
+    Sv39  => (is_valid_vAddr(sv39_params, vAddr_64b), sv39_params),
+    Sv48  => (is_valid_vAddr(sv48_params, vAddr_64b), sv48_params),
+    // Sv57 => (is_valid_vAddr(sv57_params, vAddr_64b), sv57_params),    // TODO
+  };
+  if not(valid_va) then
+    TR_Failure(translationException(ac, PTW_Invalid_Addr()), init_ext_ptw)
+  else {
+    let mxr               = mstatus.MXR() == 0b1;
+    let do_sum            = mstatus.SUM() == 0b1;
+    let asid   : asidbits = satp_to_asid(satp);
+    let ptb    : bits(64) = satp_to_PT_base(satp);
+    let tr_result1 = translate(sv_params,
+                               asid,
+                               ptb,
+                               vAddr_64b,
+                               ac, effPriv, mxr, do_sum,
+                               init_ext_ptw);
+    // Fixup result PA or exception
+    match tr_result1 {
+      TR_Address(pa, ext_ptw) => TR_Address(truncate(pa, sizeof(xlen)), ext_ptw),
+      TR_Failure(f, ext_ptw)  => TR_Failure(translationException(ac, f), ext_ptw)
+    }
+  }
+}
+
+// ****************************************************************
+// Initialize Virtual Memory state
+
+// PUBLIC: invoked from init_model()
+function init_vmem() -> unit = init_TLB()
+
+// ****************************************************************