aboutsummaryrefslogtreecommitdiff
path: root/model/riscv_vmem_common.sail
diff options
context:
space:
mode:
Diffstat (limited to 'model/riscv_vmem_common.sail')
-rw-r--r--model/riscv_vmem_common.sail245
1 files changed, 96 insertions, 149 deletions
diff --git a/model/riscv_vmem_common.sail b/model/riscv_vmem_common.sail
index 375dfa3..d17cb02 100644
--- a/model/riscv_vmem_common.sail
+++ b/model/riscv_vmem_common.sail
@@ -6,162 +6,109 @@
/* SPDX-License-Identifier: BSD-2-Clause */
/*=======================================================================================*/
-/* 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
-
-/*
- * Definitions for RV32, which has a single address translation mode: Sv32.
- */
-
-type vaddr32 = bits(32)
-type paddr32 = bits(34)
-type pte32 = bits(32)
-
-/* asid */
-type asid32 = bits(9)
-
-function curAsid32(satp : bits(32)) -> asid32 = {
- let s = Mk_Satp32(satp);
- s[Asid]
-}
-
-/* page table base from satp */
-function curPTB32(satp : bits(32)) -> paddr32 = {
- let s : Satp32 = Mk_Satp32(satp);
- shiftl(zero_extend(s[PPN]), PAGESIZE_BITS)
+// ****************************************************************
+// Parameters for VM modes sv32, sv39, sv48 and (TODO) Sv57
+
+// All VM modes use the same page size (4KB, with 12-bit index)
+
+// This two-line idiom constrains the value (2nd line) to be a singleton,
+// which helps in type-checking wherever it is used.
+type PAGESIZE_BITS : Int = 12
+let pagesize_bits = sizeof(PAGESIZE_BITS)
+
+// PRIVATE
+struct SV_Params = {
+ // VA
+ va_size_bits : {32, 39, 48}, // 32 39 48
+ vpn_size_bits : {10, 9}, // 10 9 9
+
+ // PTE
+ levels : { 2, 3, 4}, // 2 3 4
+ log_pte_size_bytes : { 2, 3}, // 2 3 3
+ pte_msbs_lsb_index : {32, 54}, // 32 54 54
+ pte_msbs_size_bits : { 0, 10}, // 0 10 10
+ pte_PPNs_lsb_index : {10}, // 10 10 10
+ pte_PPNs_size_bits : {22, 44}, // 22 44 44
+ pte_PPN_j_size_bits : {10, 9} // 10 9 9
}
-/* Sv32 parameters and bitfield layouts */
-
-let SV32_LEVEL_BITS = 10
-let SV32_LEVELS = 2
-let PTE32_LOG_SIZE = 2
-let PTE32_SIZE = 4
-
-bitfield SV32_Vaddr : vaddr32 = {
- VPNi : 31 .. 12,
- PgOfs : 11 .. 0
+// Current level during a page-table walk (0 to SV_Params.levels - 1)
+type PTW_Level = range(0,3) // range(0,4) when add Sv57 (TODO)
+
+// PRIVATE
+let sv32_params : SV_Params = struct {
+ // VA
+ va_size_bits = 32,
+ vpn_size_bits = 10,
+
+ // PTE
+ levels = 2,
+ log_pte_size_bytes = 2, // 4 Bytes
+ pte_msbs_lsb_index = 32,
+ pte_msbs_size_bits = 0,
+ pte_PPNs_lsb_index = 10,
+ pte_PPNs_size_bits = 22,
+ pte_PPN_j_size_bits = 10
}
-bitfield SV32_Paddr : paddr32 = {
- PPNi : 33 .. 12,
- PgOfs : 11 .. 0
+// PRIVATE
+let sv39_params : SV_Params = struct {
+ // VA
+ va_size_bits = 39,
+ vpn_size_bits = 9,
+
+ // PTE
+ levels = 3,
+ log_pte_size_bytes = 3, // 8 Bytes
+ pte_msbs_lsb_index = 54,
+ pte_msbs_size_bits = 10,
+ pte_PPNs_lsb_index = 10,
+ pte_PPNs_size_bits = 44,
+ pte_PPN_j_size_bits = 9
}
-bitfield SV32_PTE : pte32 = {
- PPNi : 31 .. 10,
- RSW : 9 .. 8,
- BITS : 7 .. 0
+// PRIVATE
+let sv48_params : SV_Params = struct {
+ // VA
+ va_size_bits = 48,
+ vpn_size_bits = 9,
+
+ // PTE
+ levels = 4,
+ log_pte_size_bytes = 3, // 8 Bytes
+ pte_msbs_lsb_index = 54,
+ pte_msbs_size_bits = 10,
+ pte_PPNs_lsb_index = 10,
+ pte_PPNs_size_bits = 44,
+ pte_PPN_j_size_bits = 9
}
+// TODO; not currently used
+// PRIVATE
/*
- * Definitions for RV64, which has two defined address translation modes: Sv39 and Sv48.
- */
-
-/* Sv48 and Sv64 are reserved but not defined. The size of the VPN
- * increases by 9 bits through Sv39, Sv48 and Sv57, but not for Sv64.
- * Also, the 45-bit size of the VPN for Sv57 exceeds the 44-bit size
- * of the PPN in satp64. Due to these corner cases, it is unlikely
- * that definitions can be shared across all four schemes, so separate
- * definitions might eventually be needed for each translation mode.
- *
- * But to keep things simple for now, since Sv39 and Sv48 have the
- * same PPN size, we share some definitions.
- */
-
-type paddr64 = bits(56)
-type pte64 = bits(64)
-
-/* asid */
-
-type asid64 = bits(16)
-
-function curAsid64(satp : bits(64)) -> asid64 = {
- let s = Mk_Satp64(satp);
- s[Asid]
-}
-
-/* page table base from satp */
-function curPTB64(satp : bits(64)) -> paddr64 = {
- let s = Mk_Satp64(satp);
- shiftl(zero_extend(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)
-
-bitfield SV39_Vaddr : vaddr39 = {
- VPNi : 38 .. 12,
- PgOfs : 11 .. 0
-}
-
-bitfield SV39_Paddr : paddr64 = {
- PPNi : 55 .. 12,
- PgOfs : 11 .. 0
-}
-
-bitfield SV39_PTE : pte64 = {
- Ext : 63 .. 54,
- 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 pte48 = bits(64)
-
-bitfield SV48_Vaddr : vaddr48 = {
- VPNi : 47 .. 12,
- PgOfs : 11 .. 0
-}
-
-bitfield SV48_Paddr : paddr64 = {
- PPNi : 55 .. 12,
- PgOfs : 11 .. 0
-}
-
-bitfield SV48_PTE : pte48 = {
- Ext : 63 .. 54,
- PPNi : 53 .. 10,
- RSW : 9 .. 8,
- BITS : 7 .. 0
-}
-
-/* The types below are parameterized by 'paddr and 'pte to support
- * various architectural widths (e.g. RV32, RV64). ext_ptw supports
- * extensions to the default address translation and page-table-walk.
- */
-
-/* Result of a page-table walk. */
-
-union PTW_Result('paddr : Type, 'pte : Type) = {
- PTW_Success: ('paddr, 'pte, 'paddr, nat, bool, ext_ptw),
- PTW_Failure: (PTW_Error, ext_ptw)
-}
-
-/* Result of address translation */
-
-union TR_Result('paddr : Type, 'failure : Type) = {
- TR_Address : ('paddr, ext_ptw),
- TR_Failure : ('failure, ext_ptw)
+let sv57_params : SV_Params = struct {
+ // VA
+ va_size_bits = 57,
+ vpn_size_bits = 9,
+
+ // PTE
+ levels = 5,
+ log_pte_size_bytes = 3, // 8 Bytes
+ pte_msbs_lsb_index = 54,
+ pte_msbs_size_bits = 10,
+ pte_PPNs_lsb_index = 10,
+ pte_PPNs_size_bits = 44,
+ pte_PPN_j_size_bits = 9
}
+*/
+
+// This 'undefined_SV_Params()' function is not used anywhere, but is
+// currently (2023-12) needed to work around an issue where Sail tries
+// to figure out how it could do
+// let x : SV_Params = undefined
+// even though the code never does this. This has been fixed in Sail.
+// The fix will become available in a new Sail release, at which point
+// this function can be deleted (TODO).
+// PRIVATE
+val undefined_SV_Params : unit -> SV_Params
+function undefined_SV_Params() = sv32_params
generated by cgit v1.1 at 2024-08-04 12:41:32 +0000