From 567283586aa4d2efa914b59c7d0d9b59daee7ad1 Mon Sep 17 00:00:00 2001 From: Tim Hutt Date: Tue, 14 Jan 2025 12:22:48 +0000 Subject: [PATCH] Split check_CSR_access up Split the privilege level checking and read-only checking into separate functions. This is slightly neater and also helps CHERI where ASR permissions need to use `check_CSR_priv()`. --- model/riscv_sys_control.sail | 14 +++++++++----- 1 file changed, 9 insertions(+), 5 deletions(-) diff --git a/model/riscv_sys_control.sail b/model/riscv_sys_control.sail index ace2f545f..5c839277b 100644 --- a/model/riscv_sys_control.sail +++ b/model/riscv_sys_control.sail @@ -13,10 +13,13 @@ function csrAccess(csr : csreg) -> csrRW = csr[11..10] function csrPriv(csr : csreg) -> priv_level = csr[9..8] -val check_CSR_access : (csrRW, priv_level, Privilege, bool) -> bool -function check_CSR_access(csrrw, csrpr, p, isWrite) = - not(isWrite == true & csrrw == 0b11) /* read/write */ - & (privLevel_to_bits(p) >=_u csrpr) /* privilege */ +// Check that the CSR access is made with sufficient privilege. +function check_CSR_priv(csr : csreg, p : Privilege) -> bool = + privLevel_to_bits(p) >=_u csrPriv(csr) + +// Check that the CSR access isn't a write and read-only. +function check_CSR_access(csr : csreg, isWrite : bool) -> bool = + not(isWrite & (csrAccess(csr) == 0b11)) function check_TVM_SATP(csr : csreg, p : Privilege) -> bool = not(csr == 0x180 & p == Supervisor & mstatus[TVM] == 0b1) @@ -67,7 +70,8 @@ function check_seed_CSR (csr : csreg, p : Privilege, isWrite : bool) -> bool = { function check_CSR(csr : csreg, p : Privilege, isWrite : bool) -> bool = is_CSR_defined(csr) - & check_CSR_access(csrAccess(csr), csrPriv(csr), p, isWrite) + & check_CSR_priv(csr, p) + & check_CSR_access(csr, isWrite) // TODO: If we add `p` back to is_CSR_defined() we could move these three // check_ functions back there. We should also rename is_CSR_defined() // to is_CSR_accessible() or similar.