update to new syntax

riscv · Jul 18, 2024 · 5703495 · 5703495
1 parent 421f664
commit 5703495
Show file tree

Hide file tree

Showing 2 changed files with 9 additions and 6 deletions.
diff --git a/model/riscv_sys_control.sail b/model/riscv_sys_control.sail
@@ -80,9 +80,7 @@ function is_CSR_defined (csr : csreg) -> bool =
     0x180 => haveSupMode(), // satp
 
     /* supervisor mode: resource management configurations */
-    0x181 => haveSsqosid() & ((p == Machine) |
-                              ((p == Supervisor) & haveSmstateen() & (mstateen0.PRIV_V1P14() == 0b1)) |
-                              ((p == Supervisor) & not(haveSmstateen()))), // srmcfg
+    0x181 => haveSsqosid(), // srmcfg
 
     /* user mode: counters */
     0xC00 => haveUsrMode(),    // cycle
@@ -142,12 +140,18 @@ function check_seed_CSR (csr : csreg, p : Privilege, isWrite : bool) -> bool = {
   }
 }
 
+function check_srmcfg(csr : csreg, p : Privilege) -> bool =
+    csr == 0x181 
+    & p == Supervisor
+    & ((haveSmstateen() & mstateen0.PRIV_V1P14() == 0b1) | not(haveSmstateen()))
+
 function check_CSR(csr : csreg, p : Privilege, isWrite : bool) -> bool =
     is_CSR_defined(csr)
   & check_CSR_access(csrAccess(csr), csrPriv(csr), p, isWrite)
   & check_TVM_SATP(csr, p)
   & check_Counteren(csr, p)
   & check_seed_CSR(csr, p, isWrite)
+  & check_srmcfg(csr, p)
 
 /* Reservation handling for LR/SC.
  *

diff --git a/model/riscv_sys_regs.sail b/model/riscv_sys_regs.sail
@@ -890,7 +890,7 @@ function have_PRIV_V1P14_Extensions() -> bool = {
 
 function legalize_mstateen0(o : Mstateen0, v : bits(64)) -> Mstateen0 = {
   let v = Mk_Mstateen0(v);
-  let o = update_PRIV_V1P14(o, if have_PRIV_V1P14_Extensions() then v.PRIV_V1P14() else 0b0);
+  let o = [o with PRIV_V1P14 = if have_PRIV_V1P14_Extensions() then v[PRIV_V1P14] else 0b0];
   // Other extensions are not implemented yet so all other fields are read only zero.
   o
 }
@@ -990,7 +990,6 @@ bitfield Srmcfg : xlenbits = {
 register srmcfg : Srmcfg
 
 function legalize_srmcfg(s : Srmcfg, v : xlenbits) -> Srmcfg = {
-  let s = update_MCID(s, v[27 .. 16]);
-  let s = update_RCID(s, v[11 .. 0]);
+  let s = [s with MCID = v[27 .. 16], RCID = v[11 .. 0]];
   s
 }