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
 }