PTEs are invalid if reserved bits are non-zero

This has only been the case since version 1.12 of the spec, so I added support for setting the spec version. It isn't exposed on the command line yet since hopefully we'll be using the new config system soon.

model/riscv_extensions.sail

@@ -11,6 +11,13 @@ scattered enum extension
 // Note, these are sorted according to the canonical ordering vaguely described
 // in the `Subset Naming Convention` section of the unprivileged spec.
 
+// Machine and Supervisor Architectures v1.11
+enum clause extension = Ext_Sx1p11
+// Machine and Supervisor Architectures v1.12
+enum clause extension = Ext_Sx1p12
+// Machine and Supervisor Architectures v1.13
+enum clause extension = Ext_Sx1p13
+
 // Integer Multiplication and Division; not Machine!
 enum clause extension = Ext_M
 // Single-Precision Floating-Point

model/riscv_types.sail

@@ -16,6 +16,16 @@
 val extensionEnabled : extension -> bool
 scattered function extensionEnabled
 
+// Priv/unpriv spec version.
+// TODO: Replace the `true`s with configuration flags.
+
+// Machine and Supervisor Architectures v1.11
+function clause extensionEnabled(Ext_Sx1p11) = true
+// Machine and Supervisor Architectures v1.12
+function clause extensionEnabled(Ext_Sx1p12) = extensionEnabled(Ext_Sx1p11) | true
+// Machine and Supervisor Architectures v1.13
+function clause extensionEnabled(Ext_Sx1p13) = extensionEnabled(Ext_Sx1p12) | true
+
 /* this value is only defined for the runtime platform for ELF loading
  * checks, and not used in the model.
  */

model/riscv_vmem.sail

@@ -115,7 +115,9 @@ function pt_walk(sv_params,
       let pte : bits(64) = zero_extend(pte);
 
       let pte_flags = Mk_PTE_Flags(pte[7 .. 0]);
-      if pte_is_invalid(pte_flags) then
+      let ext_pte   = ext_bits_of_PTE(sv_params, pte);
+
+      if pte_is_invalid(pte_flags, ext_pte) then
         PTW_Failure(PTW_Invalid_PTE(), ext_ptw)
       else {
         let ppns : bits(64) = PPNs_of_PTE(sv_params, pte);
@@ -135,7 +137,7 @@ function pt_walk(sv_params,
         }
         else {
           // Leaf PTE
-          let ext_pte   = msbs_of_PTE(sv_params, pte);
+          let ext_pte   = ext_bits_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 {
@@ -296,7 +298,7 @@ function translate_TLB_hit(sv_params : SV_Params,
                            ent       : TLB_Entry)
                           -> TR_Result(bits(64), PTW_Error) = {
   let pte       = ent.pte;
-  let ext_pte   = msbs_of_PTE(sv_params, pte);
+  let ext_pte   = ext_bits_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,
@@ -345,7 +347,7 @@ function translate_TLB_miss(sv_params : SV_Params,
   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);
+      let ext_pte   = ext_bits_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) {

model/riscv_vmem_pte.sail

@@ -19,21 +19,6 @@
 
 type pte_flags_bits = bits(8)
 
-// For PTW extensions (non-standard)
-type extPte = bits(64)
-
-// PRIVATE: extract msbs of PTE above the PPN
-function msbs_of_PTE(sv_params : SV_Params, pte : bits(64)) -> bits(64) = {
-  let mask : bits(64) = zero_extend(ones(sv_params.pte_msbs_size_bits));
-  (pte >> sv_params.pte_msbs_lsb_index) & mask
-}
-
-// PRIVATE: extract PPNs of PTE
-function PPNs_of_PTE(sv_params : SV_Params, pte : bits(64)) -> bits(64) = {
-  let mask : bits(64) = zero_extend(ones(sv_params.pte_PPNs_size_bits));
-  (pte >> sv_params.pte_PPNs_lsb_index) & mask
-}
-
 // PRIVATE: 8 LSBs of PTEs in Sv32, Sv39, Sv48 and Sv57
 bitfield PTE_Flags : pte_flags_bits = {
   D : 7,    // dirty
@@ -46,21 +31,50 @@ bitfield PTE_Flags : pte_flags_bits = {
   V : 0     // Valid
 }
 
+/* Reserved PTE bits could be used by extensions on RV64.  There are
+ * no such available bits on RV32, so these bits will be zeros on RV32.
+ */
+type pte_ext_bits = bits(10)
+
+bitfield PTE_Ext : pte_ext_bits = {
+  N         : 9,      /* NAPOT page table entry */
+  PBMT      : 8 .. 7, /* Page based memory types */
+  reserved  : 6 .. 0,
+}
+
+// PRIVATE: extract msbs of PTE above the PPN
+function ext_bits_of_PTE(sv_params : SV_Params, pte : bits(64)) -> PTE_Ext = {
+  Mk_PTE_Ext(if sv_params.log_pte_size_bytes == 3 then pte[63 .. 54] else zeros())
+}
+
+// PRIVATE: extract PPNs of PTE
+function PPNs_of_PTE(sv_params : SV_Params, pte : bits(64)) -> bits(64) = {
+  let mask : bits(64) = zero_extend(ones(sv_params.pte_PPNs_size_bits));
+  (pte >> sv_params.pte_PPNs_lsb_index) & mask
+}
+
 // PRIVATE: check if a PTE is a pointer to next level (non-leaf)
 function pte_is_ptr(pte_flags : PTE_Flags) -> bool = (pte_flags[X] == 0b0)
                                                       & (pte_flags[W] == 0b0)
                                                       & (pte_flags[R] == 0b0)
 
 // PRIVATE: check if a PTE is valid
-function pte_is_invalid(pte_flags : PTE_Flags) -> bool = (pte_flags[V] == 0b0)
-                                                         | ((pte_flags[W] == 0b1)
-                                                            & (pte_flags[R] == 0b0))
+function pte_is_invalid(pte_flags : PTE_Flags, pte_ext : PTE_Ext) -> bool =
+    pte_flags[V] == 0b0
+  | (pte_flags[W] == 0b1 & pte_flags[R] == 0b0)
+  // Since version 1.12 of the spec, reserved bits must be zero.
+  | extensionEnabled(Ext_Sx1p12) & (
+    // If this is a non-leaf page, A/D/U bits are reserved
+      pte_is_ptr(pte_flags) & (pte_flags[A] @ pte_flags[D] @ pte_flags[U] != zeros())
+    // `pte_ext` contains bits for Svnapot and Svpbmt but these are not implemented yet.
+    | pte_ext.bits != zeros()
+  )
 
 // ----------------
 // Check access permissions in PTE
 
 // For (non-standard) extensions: this function gets the extension-available bits
-// of the PTE in extPte, and the accumulated information of the page-table-walk
+// of the PTE in PTE_Ext, and the accumulated information of the page-table-walk
 // in ext_ptw. It should return the updated ext_ptw in both success and failure cases.
 
 union PTE_Check = {
@@ -74,7 +88,7 @@ function check_PTE_permission(ac        : AccessType(ext_access_type),
                               mxr       : bool,
                               do_sum    : bool,
                               pte_flags : PTE_Flags,
-                              ext       : extPte,
+                              ext       : PTE_Ext,
                               ext_ptw   : ext_ptw) -> PTE_Check = {
   let pte_U = pte_flags[U];
   let pte_R = pte_flags[R];