Add satp mode guard

config/default.json

@@ -195,6 +195,18 @@
     },
     "Svinval": {
       "supported": true
+    },
+    "Sv32": {
+      "supported": true
+    },
+    "Sv39": {
+      "supported": true
+    },
+    "Sv48": {
+      "supported": true
+    },
+    "Sv57": {
+      "supported": true
     }
   }
 }

model/riscv_extensions.sail

@@ -202,6 +202,16 @@ function clause hartSupports(Ext_Svnapot) = false // Not supported yet
 enum clause extension = Ext_Svpbmt
 function clause hartSupports(Ext_Svpbmt) = false // Not supported yet
 
+// Supervisor-Level Address Translation Modes
+enum clause extension = Ext_Svbare
+enum clause extension = Ext_Sv32
+function clause hartSupports(Ext_Sv32) = config extensions.Sv32.supported : bool & (xlen == 32)
+enum clause extension = Ext_Sv39
+function clause hartSupports(Ext_Sv39) = config extensions.Sv39.supported : bool & (xlen == 64)
+enum clause extension = Ext_Sv48
+function clause hartSupports(Ext_Sv48) = config extensions.Sv48.supported : bool & (xlen == 64)
+enum clause extension = Ext_Sv57
+function clause hartSupports(Ext_Sv57) = config extensions.Sv57.supported : bool & (xlen == 64)
 // Cycle and Instret Privilege Mode Filtering
 enum clause extension = Ext_Smcntrpmf
 function clause hartSupports(Ext_Smcntrpmf) = config extensions.Smcntrpmf.supported

model/riscv_sys_regs.sail

@@ -140,6 +140,16 @@ function clause write_CSR(0x301, value) = { misa = legalize_misa(misa, value); m
 function clause currentlyEnabled(Ext_U) = hartSupports(Ext_U) & misa[U] == 0b1
 function clause currentlyEnabled(Ext_S) = hartSupports(Ext_S) & misa[S] == 0b1
 
+function clause currentlyEnabled(Ext_Svbare) = currentlyEnabled(Ext_S)
+function clause currentlyEnabled(Ext_Sv32) = hartSupports(Ext_Sv32) &  currentlyEnabled(Ext_S)
+function clause currentlyEnabled(Ext_Sv39) = hartSupports(Ext_Sv39) &  currentlyEnabled(Ext_S)
+function clause currentlyEnabled(Ext_Sv48) = hartSupports(Ext_Sv48) &  currentlyEnabled(Ext_S)
+function clause currentlyEnabled(Ext_Sv57) = hartSupports(Ext_Sv57) &  currentlyEnabled(Ext_S)
+
+function virtual_memory_supported() -> bool = {
+  currentlyEnabled(Ext_Sv32) | currentlyEnabled(Ext_Sv39) | currentlyEnabled(Ext_Sv48) | currentlyEnabled(Ext_Sv57)
+}
+
 /*
  * Illegal values legalized to least privileged mode supported.
  * Note: the only valid combinations of supported modes are M, M+U, M+S+U.
@@ -235,7 +245,7 @@ function legalize_mstatus(o : Mstatus, v : bits(64)) -> Mstatus = {
     TW = if currentlyEnabled(Ext_U) then v[TW] else 0b0,
     TVM = if currentlyEnabled(Ext_S) then v[TVM] else 0b0,
     MXR = if currentlyEnabled(Ext_S) then v[MXR] else 0b0,
-    SUM = if currentlyEnabled(Ext_S) then v[SUM] else 0b0, // TODO: Should also be disabled if satp.MODE is read-only 0
+    SUM = if virtual_memory_supported() then v[SUM] else 0b0,
     MPRV = if currentlyEnabled(Ext_U) then v[MPRV] else 0b0,
     /* We don't have any extension context yet. */
     XS = extStatus_to_bits(Off),
@@ -851,13 +861,26 @@ function legalize_satp(
   written_value : xlenbits,
 ) -> xlenbits = {
   if xlen == 32 then {
-    /* all 32-bit satp modes are valid */
-    written_value
+    let s = Mk_Satp32(written_value);
+    match satpMode_of_bits(arch, 0b000 @ s[Mode]) {
+      None()  => prev_value,
+      Some(Sv_mode) => match Sv_mode {
+        Bare if currentlyEnabled(Ext_Svbare) => s.bits,
+        Sv32 if currentlyEnabled(Ext_Sv32) => s.bits,
+        _ => prev_value,
+      }
+    }
   } else if xlen == 64 then {
     let s = Mk_Satp64(written_value);
     match satpMode_of_bits(arch, s[Mode]) {
       None()  => prev_value,
-      Some(_) => s.bits
+      Some(Sv_mode) =>  match Sv_mode {
+        Bare if currentlyEnabled(Ext_Svbare) => s.bits,
+        Sv39 if currentlyEnabled(Ext_Sv39) => s.bits,
+        Sv48 if currentlyEnabled(Ext_Sv48) => s.bits,
+        Sv57 if currentlyEnabled(Ext_Sv57) => s.bits,
+        _ => prev_value,
+      }
     }
   } else {
     internal_error(__FILE__, __LINE__, "Unsupported xlen" ^ dec_str(xlen))