path: root/model/riscv_vmem.sail

/*=======================================================================================*/
/*  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()

// ****************************************************************