diff --git a/model/riscv_sys_control.sail b/model/riscv_sys_control.sail index e7bcde791..cb67025a4 100644 --- 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 index 2af1ee95c..fce0e766c 100644 --- 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 }