diff --git a/model/riscv_csr_ext.sail b/model/riscv_csr_ext.sail index 4d43df543..f034460d6 100644 --- a/model/riscv_csr_ext.sail +++ b/model/riscv_csr_ext.sail @@ -14,7 +14,7 @@ end csr_name_map previously. */ function csr_name(csr) = csr_name_map(csr) -function clause ext_is_CSR_defined(_, _) = false +function clause ext_is_CSR_defined(_) = false end ext_is_CSR_defined function clause ext_read_CSR _ = None() diff --git a/model/riscv_csr_map.sail b/model/riscv_csr_map.sail index 22cffd5a6..6478919ca 100644 --- a/model/riscv_csr_map.sail +++ b/model/riscv_csr_map.sail @@ -188,10 +188,9 @@ overload to_str = {csr_name} */ -/* returns whether a CSR is defined and accessible at a given address - * and privilege +/* returns whether a CSR exists */ -val ext_is_CSR_defined : (csreg, Privilege) -> bool +val ext_is_CSR_defined : (csreg) -> bool scattered function ext_is_CSR_defined /* returns the value of the CSR if it is defined */ diff --git a/model/riscv_fdext_control.sail b/model/riscv_fdext_control.sail index 8f299994b..03450e8f6 100644 --- a/model/riscv_fdext_control.sail +++ b/model/riscv_fdext_control.sail @@ -15,11 +15,11 @@ /* **************************************************************** */ -/* val clause ext_is_CSR_defined : (csreg, Privilege) -> bool */ +/* val clause ext_is_CSR_defined : (csreg) -> bool */ -function clause ext_is_CSR_defined (0x001, _) = haveFExt() | haveZfinx() -function clause ext_is_CSR_defined (0x002, _) = haveFExt() | haveZfinx() -function clause ext_is_CSR_defined (0x003, _) = haveFExt() | haveZfinx() +function clause ext_is_CSR_defined (0x001) = haveFExt() | haveZfinx() +function clause ext_is_CSR_defined (0x002) = haveFExt() | haveZfinx() +function clause ext_is_CSR_defined (0x003) = haveFExt() | haveZfinx() function clause ext_read_CSR (0x001) = Some(zero_extend(fcsr[FFLAGS])) function clause ext_read_CSR (0x002) = Some(zero_extend(fcsr[FRM])) diff --git a/model/riscv_next_control.sail b/model/riscv_next_control.sail index 688d16d72..6ae84ea63 100644 --- a/model/riscv_next_control.sail +++ b/model/riscv_next_control.sail @@ -8,14 +8,14 @@ /* Functional specification for the 'N' user-level interrupts standard extension. */ -function clause ext_is_CSR_defined(0x000, _) = haveUsrMode() & haveNExt() // ustatus -function clause ext_is_CSR_defined(0x004, _) = haveUsrMode() & haveNExt() // uie -function clause ext_is_CSR_defined(0x005, _) = haveUsrMode() & haveNExt() // utvec -function clause ext_is_CSR_defined(0x040, _) = haveUsrMode() & haveNExt() // uscratch -function clause ext_is_CSR_defined(0x041, _) = haveUsrMode() & haveNExt() // uepc -function clause ext_is_CSR_defined(0x042, _) = haveUsrMode() & haveNExt() // ucause -function clause ext_is_CSR_defined(0x043, _) = haveUsrMode() & haveNExt() // utval -function clause ext_is_CSR_defined(0x044, _) = haveUsrMode() & haveNExt() // uip +function clause ext_is_CSR_defined(0x000) = haveUsrMode() & haveNExt() // ustatus +function clause ext_is_CSR_defined(0x004) = haveUsrMode() & haveNExt() // uie +function clause ext_is_CSR_defined(0x005) = haveUsrMode() & haveNExt() // utvec +function clause ext_is_CSR_defined(0x040) = haveUsrMode() & haveNExt() // uscratch +function clause ext_is_CSR_defined(0x041) = haveUsrMode() & haveNExt() // uepc +function clause ext_is_CSR_defined(0x042) = haveUsrMode() & haveNExt() // ucause +function clause ext_is_CSR_defined(0x043) = haveUsrMode() & haveNExt() // utval +function clause ext_is_CSR_defined(0x044) = haveUsrMode() & haveNExt() // uip function clause ext_read_CSR(0x000) = Some(lower_sstatus(lower_mstatus(mstatus)).bits) function clause ext_read_CSR(0x004) = Some(lower_sie(lower_mie(mie, mideleg), sideleg).bits) diff --git a/model/riscv_sys_control.sail b/model/riscv_sys_control.sail index 32775c27b..becf447a9 100644 --- a/model/riscv_sys_control.sail +++ b/model/riscv_sys_control.sail @@ -14,68 +14,68 @@ function csrAccess(csr : csreg) -> csrRW = csr[11..10] function csrPriv(csr : csreg) -> priv_level = csr[9..8] -function is_CSR_defined (csr : csreg, p : Privilege) -> bool = +function is_CSR_defined (csr : csreg) -> bool = match (csr) { /* machine mode: informational */ - 0xf11 => p == Machine, // mvendorid - 0xf12 => p == Machine, // marchdid - 0xf13 => p == Machine, // mimpid - 0xf14 => p == Machine, // mhartid - 0xf15 => p == Machine, // mconfigptr + 0xf11 => true, // mvendorid + 0xf12 => true, // marchdid + 0xf13 => true, // mimpid + 0xf14 => true, // mhartid + 0xf15 => true, // mconfigptr /* machine mode: trap setup */ - 0x300 => p == Machine, // mstatus - 0x301 => p == Machine, // misa - 0x302 => p == Machine & (haveSupMode() | haveNExt()), // medeleg - 0x303 => p == Machine & (haveSupMode() | haveNExt()), // mideleg - 0x304 => p == Machine, // mie - 0x305 => p == Machine, // mtvec - 0x306 => p == Machine & haveUsrMode(), // mcounteren - 0x30A => p == Machine & haveUsrMode(), // menvcfg - 0x310 => p == Machine & (sizeof(xlen) == 32), // mstatush - 0x31A => p == Machine & haveUsrMode() & (sizeof(xlen) == 32), // menvcfgh - 0x320 => p == Machine, // mcountinhibit + 0x300 => true, // mstatus + 0x301 => true, // misa + 0x302 => haveSupMode() | haveNExt(), // medeleg + 0x303 => haveSupMode() | haveNExt(), // mideleg + 0x304 => true, // mie + 0x305 => true, // mtvec + 0x306 => haveUsrMode(), // mcounteren + 0x30A => haveUsrMode(), // menvcfg + 0x310 => sizeof(xlen) == 32, // mstatush + 0x31A => haveUsrMode() & (sizeof(xlen) == 32), // menvcfgh + 0x320 => true, // mcountinhibit /* machine mode: trap handling */ - 0x340 => p == Machine, // mscratch - 0x341 => p == Machine, // mepc - 0x342 => p == Machine, // mcause - 0x343 => p == Machine, // mtval - 0x344 => p == Machine, // mip + 0x340 => true, // mscratch + 0x341 => true, // mepc + 0x342 => true, // mcause + 0x343 => true, // mtval + 0x344 => true, // mip // pmpcfgN - 0x3A @ idx : bits(4) => p == Machine & sys_pmp_count() > unsigned(idx) & (idx[0] == bitzero | sizeof(xlen) == 32), + 0x3A @ idx : bits(4) => sys_pmp_count() > unsigned(idx) & (idx[0] == bitzero | sizeof(xlen) == 32), // pmpaddrN. Unfortunately the PMP index does not nicely align with the CSR index bits. - 0x3B @ idx : bits(4) => p == Machine & sys_pmp_count() > unsigned(0b00 @ idx), - 0x3C @ idx : bits(4) => p == Machine & sys_pmp_count() > unsigned(0b01 @ idx), - 0x3D @ idx : bits(4) => p == Machine & sys_pmp_count() > unsigned(0b10 @ idx), - 0x3E @ idx : bits(4) => p == Machine & sys_pmp_count() > unsigned(0b11 @ idx), - 0xB00 => p == Machine, // mcycle - 0xB02 => p == Machine, // minstret + 0x3B @ idx : bits(4) => sys_pmp_count() > unsigned(0b00 @ idx), + 0x3C @ idx : bits(4) => sys_pmp_count() > unsigned(0b01 @ idx), + 0x3D @ idx : bits(4) => sys_pmp_count() > unsigned(0b10 @ idx), + 0x3E @ idx : bits(4) => sys_pmp_count() > unsigned(0b11 @ idx), + 0xB00 => true, // mcycle + 0xB02 => true, // minstret - 0xB80 => p == Machine & (sizeof(xlen) == 32), // mcycleh - 0xB82 => p == Machine & (sizeof(xlen) == 32), // minstreth + 0xB80 => sizeof(xlen) == 32, // mcycleh + 0xB82 => sizeof(xlen) == 32, // minstreth /* disabled trigger/debug module */ - 0x7a0 => p == Machine, + 0x7a0 => true, /* supervisor mode: trap setup */ - 0x100 => haveSupMode() & (p == Machine | p == Supervisor), // sstatus - 0x102 => haveSupMode() & haveNExt() & (p == Machine | p == Supervisor), // sedeleg - 0x103 => haveSupMode() & haveNExt() & (p == Machine | p == Supervisor), // sideleg - 0x104 => haveSupMode() & (p == Machine | p == Supervisor), // sie - 0x105 => haveSupMode() & (p == Machine | p == Supervisor), // stvec - 0x106 => haveSupMode() & (p == Machine | p == Supervisor), // scounteren - 0x10A => haveSupMode() & (p == Machine | p == Supervisor), // senvcfg + 0x100 => haveSupMode(), // sstatus + 0x102 => haveSupMode() & haveNExt(), // sedeleg + 0x103 => haveSupMode() & haveNExt(), // sideleg + 0x104 => haveSupMode(), // sie + 0x105 => haveSupMode(), // stvec + 0x106 => haveSupMode(), // scounteren + 0x10A => haveSupMode(), // senvcfg /* supervisor mode: trap handling */ - 0x140 => haveSupMode() & (p == Machine | p == Supervisor), // sscratch - 0x141 => haveSupMode() & (p == Machine | p == Supervisor), // sepc - 0x142 => haveSupMode() & (p == Machine | p == Supervisor), // scause - 0x143 => haveSupMode() & (p == Machine | p == Supervisor), // stval - 0x144 => haveSupMode() & (p == Machine | p == Supervisor), // sip + 0x140 => haveSupMode(), // sscratch + 0x141 => haveSupMode(), // sepc + 0x142 => haveSupMode(), // scause + 0x143 => haveSupMode(), // stval + 0x144 => haveSupMode(), // sip /* supervisor mode: address translation */ - 0x180 => haveSupMode() & (p == Machine | p == Supervisor), // satp + 0x180 => haveSupMode(), // satp /* user mode: counters */ 0xC00 => haveUsrMode(), // cycle @@ -90,7 +90,7 @@ function is_CSR_defined (csr : csreg, p : Privilege) -> bool = 0x015 => haveZkr(), /* check extensions */ - _ => ext_is_CSR_defined(csr, p) + _ => ext_is_CSR_defined(csr) } val check_CSR_access : (csrRW, priv_level, Privilege, bool) -> bool @@ -137,7 +137,7 @@ 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, p) + is_CSR_defined(csr) & check_CSR_access(csrAccess(csr), csrPriv(csr), p, isWrite) & check_TVM_SATP(csr, p) & check_Counteren(csr, p) diff --git a/model/riscv_vext_control.sail b/model/riscv_vext_control.sail index d7a17ee28..3344d7c5a 100755 --- a/model/riscv_vext_control.sail +++ b/model/riscv_vext_control.sail @@ -6,14 +6,14 @@ /* SPDX-License-Identifier: BSD-2-Clause */ /*=======================================================================================*/ -function clause ext_is_CSR_defined (0x008, _) = true -function clause ext_is_CSR_defined (0xC20, _) = true -function clause ext_is_CSR_defined (0xC21, _) = true -function clause ext_is_CSR_defined (0xC22, _) = true +function clause ext_is_CSR_defined (0x008) = true +function clause ext_is_CSR_defined (0xC20) = true +function clause ext_is_CSR_defined (0xC21) = true +function clause ext_is_CSR_defined (0xC22) = true -function clause ext_is_CSR_defined (0x009, _) = true -function clause ext_is_CSR_defined (0x00A, _) = true -function clause ext_is_CSR_defined (0x00F, _) = true +function clause ext_is_CSR_defined (0x009) = true +function clause ext_is_CSR_defined (0x00A) = true +function clause ext_is_CSR_defined (0x00F) = true function clause ext_read_CSR (0x009) = Some (zero_extend(vcsr[vxsat])) function clause ext_read_CSR (0x00A) = Some (zero_extend(vcsr[vxrm]))