Add the satp legalizer.

3 files changed, 20 insertions, 3 deletions

diff --git a/riscv/riscv.sail b/riscv/riscv.sail
index c8b3956a..69baea30 100644
--- a/riscv/riscv.sail
+++ b/riscv/riscv.sail
@@ -569,7 +569,7 @@ function writeCSR (csr : bits(12), value : xlenbits) -> unit =
     0x142 => scause->bits() = value,
     0x143 => stval = value,
     0x144 => mip->bits() = value,
-    0x180 => satp = value,
+    0x180 => satp = legalize_satp(cur_Architecture(), satp, value),
 
     _     => print_bits("unhandled write to CSR ", csr)
   }
diff --git a/riscv/riscv_sys.sail b/riscv/riscv_sys.sail
index 39d611cf..93a0199a 100644
--- a/riscv/riscv_sys.sail
+++ b/riscv/riscv_sys.sail
@@ -315,18 +315,26 @@ register sideleg : Minterrupts
 register sip     : Minterrupts
 register sie     : Minterrupts
 
-bitfield satp64 : bits(64) = {
+bitfield Satp64 : bits(64) = {
   Mode : 63 .. 60,
   Asid : 59 .. 44,
   PPN  : 43 .. 0
 }
+register satp : xlenbits
+
+function legalize_satp(a : Architecture, o : xlenbits, v : xlenbits) -> xlenbits = {
+  let s = Mk_Satp64(v);
+  match satpMode_of_bits(a, s.Mode()) {
+    None()  => o,
+    Some(_) => s.bits()
+  }
+}
 
 register stvec : Mtvec
 register sscratch : xlenbits
 register sepc : xlenbits
 register scause : Mcause
 register stval : xlenbits
-register satp : xlenbits
 
 /* csr access control */
 
diff --git a/riscv/riscv_types.sail b/riscv/riscv_types.sail
index 1e41133d..d42af3df 100644
--- a/riscv/riscv_types.sail
+++ b/riscv/riscv_types.sail
@@ -230,6 +230,15 @@ function extStatus_of_bits(e) = {
 type satp_mode = bits(4)
 enum SATPMode = {Sbare, Sv32, Sv39}
 
+function satpMode_of_bits(a : Architecture, m : satp_mode) -> option(SATPMode) = {
+  match (a, m) {
+    (_, 0x0)    => Some(Sbare),
+    (RV32, 0x1) => Some(Sv32),
+    (RV64, 0x8) => Some(Sv39),
+    (_, _)      => None()
+  }
+}
+
 /* CSR access control bits (from CSR addresses) */
 type csrRW = bits(2)  /* read/write */