CSR check
ConceptIn the riscv-formal framework, CSR (Control and Status Register) checks are a family of formal verification checks, managed by the `genchecks.py` tool, that validate the behavior of CSR instructions, illegal CSR accesses, and CSR consistency properties using the standard RISC-V Formal Interface (RVFI) wrapper.
First seen 6/7/2026
Last seen 6/7/2026
Evidence 3 chunks
Wiki v1
WIKI
Overview
CSR checks are a category of formal verification checks used within the riscv-formal verification framework. They are managed by the genchecks.py tool and are implemented using the standard RISC-V Formal Interface (RVFI) wrapper. All CSR checks operate on one channel at a time and may not behave correctly if a CSR can be modified by more than one channel.
The CSR checks broadly fall into three groups:
NEIGHBORHOOD
No graph connections found for this entity yet. It may appear in future ingestion runs.
explore full graph →RELATIONSHIPS
2 connectionsgenchecks.py manages CSR checks as part of the standard checks
CSR checks operate on RVFI signal ports to validate CSR behavior
LINKED ENTITIES
2 linksCITATIONS
12 sources12 citations — click to expand
[1] CSR checks are managed by `genchecks.py` and can be implemented using the standard RVFI wrapper interface, and all checks operate on one channel at a time. Verification procedure - RISC-V Formal documentation
[2] The `csrw` check validates that CSR instructions modify the correct RVFI signal ports, using macros such as `RISCV_FORMAL_CSRW_NAME`, `csr_{m,s,u}index_<csrname>`, and optionally `RISCV_FORMAL_CSRWH` and `csr_{m,s,u}indexh_<csrname>`. Verification procedure - RISC-V Formal documentation
[3] The top two bits (`csr[11:10]`) indicate read/write versus read-only, and `csr[9:8]` encode the lowest privilege level that can access the CSR; valid reads assign `rvfi_csr_<csrname>_rdata` to `rvfi_rd_wdata` with correct `rvfi_rd_addr`, valid writes assign correct value to `rvfi_csr_<csrname>_wdata`, and any illegal access must result in a trap. Verification procedure - RISC-V Formal documentation
[4] The `csr_ill` check validates illegal access exceptions for CSRs not available through RVFI, using `RISCV_FORMAL_ILL_CSR_ADDR`, `RISCV_FORMAL_ILL_{M,S,U}MODE`, and `RISCV_FORMAL_ILL_{WRITE,READ}`. Verification procedure - RISC-V Formal documentation
[5] The `csrc_any` check tests whether any value written to a CSR can be read back exactly as written. Verification procedure - RISC-V Formal documentation
[6] The `csrc_inc` check tests whether a CSR value is always greater than or equal to a previous read/write, useful for hardware performance monitors, and constraining the MSB to 0 verifies that the value can never decrease except by writing. Verification procedure - RISC-V Formal documentation
[7] The `csrc_upcnt` check forbids writes to the CSR under test and requires the test value to be strictly greater than the previously read value, useful for `mcycle` and `minstret`. Verification procedure - RISC-V Formal documentation
[8] The `csrc_hpm` check is a cover check that verifies a hpm counter CSR *can* increase, used with `csrc_inc` to verify the hpm is able to increase and unable to decrease; it requires `RISCV_FORMAL_CSRC_NAME mhpmevent#`, `RISCV_FORMAL_CSRC_HPMCOUNTER mhpmcounter#`, `RISCV_FORMAL_CSRC_HPMEVENT <value>`, and `RISCV_FORMAL_CSR_MHPMCOUNTER#`/`RISCV_FORMAL_CSR_MHPMEVENT#` defined and connected. Verification procedure - RISC-V Formal documentation
[9] The `csrc_const` check tests whether a CSR is always the same, using `RISCV_FORMAL_CSRC_CONSTVAL` or `rdata_shadow` to compare against the previously read value. Verification procedure - RISC-V Formal documentation
[10] The `csrc_zero` check is similar to `csrc_const` but exclusively tests for a constant value of all zero. Verification procedure - RISC-V Formal documentation
[11] The `[depth]`, `[csrs]`, `[custom_csrs]`, and `[illegal_csrs]` configuration sections control how `genchecks.py` generates CSR checks, with depth specifying BMC depth and reset cycles, and `_mask=` allowing bit-mask expressions in `const`, `zero`, and `any` checks. Verification procedure - RISC-V Formal documentation
[12] Setting `csr_spec` in the `[options]` section automatically generates tests for all CSRs to match specification recommendations/requirements, adds them to `csrw` tests, generates corresponding `csrc` tests, and treats WPRI/WARL bits as reserved constant-zero. Currently the only supported value is `1.12` (version 1.12 of the Machine ISA, 20211203 Privileged Architecture document). Verification procedure - RISC-V Formal documentation