From 1a3614c2ec80dc8293fab7dd9f998c77d300ff14 Mon Sep 17 00:00:00 2001
From: MingZhu Yan <yanmingzhu@iscas.ac.cn>
Date: Thu, 29 Aug 2024 10:06:28 +0800
Subject: [PATCH] Added constraint for SXLEN and UXLEN

---
 model/riscv_sys_regs.sail | 15 +++++++++++----
 model/riscv_types.sail    |  7 +++++++
 2 files changed, 18 insertions(+), 4 deletions(-)

diff --git a/model/riscv_sys_regs.sail b/model/riscv_sys_regs.sail
index fc19d5161..5622ade5a 100644
--- a/model/riscv_sys_regs.sail
+++ b/model/riscv_sys_regs.sail
@@ -204,14 +204,17 @@ function effectivePrivilege(t : AccessType(ext_access_type), m : Mstatus, priv :
 function get_mstatus_SXL(m : Mstatus) -> arch_xlen = {
   if   sizeof(xlen) == 32
   then arch_to_bits(RV32)
-  else m.bits[35 .. 34]
+  else
+    if   not(have_privLevel(privLevel_to_bits(Supervisor)))
+    then 0b00
+    else m.bits[35 .. 34]
 }
 
 function set_mstatus_SXL(m : Mstatus, a : arch_xlen) -> Mstatus = {
   if   sizeof(xlen) == 32
   then m
   else {
-    let m = vector_update_subrange(m.bits, 35, 34,  a);
+    let m = vector_update_subrange(m.bits, 35, 34, a);
     Mk_Mstatus(m)
   }
 }
@@ -219,14 +222,17 @@ function set_mstatus_SXL(m : Mstatus, a : arch_xlen) -> Mstatus = {
 function get_mstatus_UXL(m : Mstatus) -> arch_xlen = {
   if   sizeof(xlen) == 32
   then arch_to_bits(RV32)
-  else m.bits[33 .. 32]
+  else
+    if   not(have_privLevel(privLevel_to_bits(User)))
+    then 0b00
+    else m.bits[33 .. 32]
 }
 
 function set_mstatus_UXL(m : Mstatus, a : arch_xlen) -> Mstatus = {
   if   sizeof(xlen) == 32
   then m
   else {
-    let m = vector_update_subrange(m.bits, 33, 32,  a);
+    let m = vector_update_subrange(m.bits, 33, 32, a);
     Mk_Mstatus(m)
   }
 }
@@ -257,6 +263,7 @@ function legalize_mstatus(o : Mstatus, v : xlenbits) -> Mstatus = {
   let m = [m with SD = bool_to_bits(dirty)];
 
   /* We don't support dynamic changes to SXL and UXL. */
+  assert(arch_xlen_to_int(get_mstatus_SXL(o)) >= arch_xlen_to_int(get_mstatus_UXL(o)));
   let m = set_mstatus_SXL(m, get_mstatus_SXL(o));
   let m = set_mstatus_UXL(m, get_mstatus_UXL(o));
 
diff --git a/model/riscv_types.sail b/model/riscv_types.sail
index 166aee072..2555cd865 100644
--- a/model/riscv_types.sail
+++ b/model/riscv_types.sail
@@ -78,6 +78,13 @@ function arch_to_bits(a : Architecture) -> arch_xlen =
     RV128 => 0b11
   }
 
+function arch_xlen_to_int(a : arch_xlen) -> int =
+  match a {
+    0b01 => 32,
+    0b10 => 64,
+    0b11 => 128,
+    0b00 => 0
+  }
 
 /* model-internal exceptions */