From 03e322f198ba33e36783a87c852ec52fa8d74b55 Mon Sep 17 00:00:00 2001
From: KotorinMinami <huangshuo4@gmail.com>
Date: Fri, 21 Mar 2025 12:36:37 +0800
Subject: [PATCH] add satp mode guard

---
 config/default.json         | 12 ++++++++++++
 model/riscv_extensions.sail | 10 ++++++++++
 model/riscv_sys_regs.sail   | 31 +++++++++++++++++++++++++++----
 3 files changed, 49 insertions(+), 4 deletions(-)

diff --git a/config/default.json b/config/default.json
index 9ef58c764..188b33a2d 100644
--- a/config/default.json
+++ b/config/default.json
@@ -195,6 +195,18 @@
     },
     "Svinval": {
       "supported": true
+    },
+    "Sv32": {
+      "supported": true
+    },
+    "Sv39": {
+      "supported": true
+    },
+    "Sv48": {
+      "supported": true
+    },
+    "Sv57": {
+      "supported": true
     }
   }
 }
diff --git a/model/riscv_extensions.sail b/model/riscv_extensions.sail
index f0c83a51b..3e67af9d8 100644
--- a/model/riscv_extensions.sail
+++ b/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
diff --git a/model/riscv_sys_regs.sail b/model/riscv_sys_regs.sail
index 73fd93039..e4c30af1b 100644
--- a/model/riscv_sys_regs.sail
+++ b/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))