Skip to content
STIMSMITH

CSR check

Concept WIKI v1 · 6/7/2026

In 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.

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:

  • The CSR instruction check (csrw)
  • The illegal CSR access check (csr_ill)
  • A set of CSR consistency checks (csrc_*)

CSR instruction check

The csrw check validates that CSR instructions modify the correct RVFI signal ports. For the CSR under test, RISCV_FORMAL_CSRW_NAME <csrname> must be defined along with csr_{m,s,u}index_<csrname> <csraddr>. If the CSR has a corresponding 'h' register holding upper bits, RISCV_FORMAL_CSRWH and csr_{m,s,u}indexh_<csrname> <csraddr> should also be defined.

Per the standard CSR address mapping convention, the top two bits (csr[11:10]) indicate whether the register is read/write (00, 01, or 10) or read-only (11), and the next two bits (csr[9:8]) encode the lowest privilege level that can access the CSR.

Expected behavior:

  • A valid read must assign rvfi_csr_<csrname>_rdata to rvfi_rd_wdata, along with the correct rvfi_rd_addr.
  • A valid write must assign the correct value to rvfi_csr_<csrname>_wdata.
  • Any illegal access must result in a trap.

Illegal CSR access

The csr_ill check validates that illegal access exceptions are raised for CSRs which are not available through the RVFI wrapper interface, including those which may not be implemented. The macro RISCV_FORMAL_ILL_CSR_ADDR <csraddr> must be defined for the CSR under test. The macros RISCV_FORMAL_ILL_{M,S,U}MODE specify which modes should be tested for access, and RISCV_FORMAL_ILL_{WRITE,READ} specify what accesses are expected to be illegal.

CSR consistency checks

The consistency checks perform multiple reads and writes and compare the values on rvfi_csr_<csrname>_rdata and rvfi_csr_<csrname>_wdata during the check cycle. For each of these checks, RISCV_FORMAL_CSRC_NAME <csrname> must be defined for the CSR under test, along with the corresponding csr_{m,s,u}index_<csrname> <csraddr>.

CSR write-any (csrc_any)

Tests whether any value written to a CSR can be read back exactly as written.

CSR increments (csrc_inc)

Tests whether the value in a CSR is always greater than or equal to a previous read or write of the CSR. By constraining the most significant bit to 0, this check can verify that a CSR's value can never decrease except by writing to it. This is particularly useful for hardware performance monitors.

CSR up-counter (csrc_upcnt)

Similar to the CSR increments check but with more constraints:

  • No writes of the CSR under test are allowed.
  • The test value must be strictly greater than the previously read value.

Without fairness guarantees, this has limited use, but it can verify some hpm functions, especially mcycle and minstret.

CSR hpm event cover check (csrc_hpm)

Unlike most of the other checks, csrc_hpm is a cover check. Similarly to the up-counter check, it compares the value of a hpm counter CSR with a previously stored value, and the value must increase. However, because this is a cover check, it tests that the CSR can increase, not that it must increase. Used in conjunction with a csrc_inc test of the corresponding hpm counter CSR, this combination can verify that the hpm is able to increase and unable to decrease.

This check must be performed on a hpm event CSR. It requires RISCV_FORMAL_CSRC_NAME mhpmevent# and RISCV_FORMAL_CSRC_HPMCOUNTER mhpmcounter#, with the event defined by RISCV_FORMAL_CSRC_HPMEVENT <value>. Both RISCV_FORMAL_CSR_MHPMCOUNTER# and RISCV_FORMAL_CSR_MHPMEVENT# must be defined and the corresponding RVFI signals must be connected.

CSR read-constant (csrc_const)

Tests whether the value in a CSR is always the same, ignoring any value which may be written. RISCV_FORMAL_CSRC_CONSTVAL <value> must be defined as the value to be expected. For CSRs which can take any value provided it remains constant during operation, a value of rdata_shadow can be assigned, which will compare against the previously read value.

CSR read-zero (csrc_zero)

Similar to the CSR read-constant check, but exclusively tests for a constant value of all zero.

genchecks.py configuration

The genchecks.py tool reads its configuration from several sections that govern how CSR checks are generated:

  • [depth] — csrw and csr_ill checks expect one value indicating the maximum depth of the BMC. All csrc_* checks expect two values: the number of cycles to hold reset and the maximum depth of the BMC. Depth can be specified for all tests of one type (e.g. csrc_zero) or for an individual CSR (e.g. csrw_mcycle). Tests without a corresponding value in the [depth] section will not be run.
  • [csrs] — Lists all standard CSRs which can be tested. By default, all CSRs are run through the CSR instruction check (csrw). Consistency checks can be appended as a space-separated list after the CSR name. For checks which expect a value, quotation marks allow verbatim values. A _mask= suffix can be used to specify a Verilog bit-mask expression applied to the CSR before testing (currently supported for const, zero, and any). Each named CSR must be connected as described in the RVFI documentation.
  • [custom_csrs] — Lists platform-defined CSRs. Each line is a space-separated list defining one CSR: address in hexadecimal, the privilege modes in which it is available, and the rest of the line follows the same format as [csrs]. Each custom CSR must be connected through the RVFI wrapper.
  • [illegal_csrs] — Lists unnamed CSRs not available through the RVFI wrapper. Each line lists one CSR address to test with csr_ill, the relevant modes to check, and whether to test reads and writes or just writes.
  • csr_spec (in [options]) — When set, automatically generates tests for all CSRs to match the specification recommendations/requirements. This adds all defined CSRs to be tested under csrw and generates corresponding csrc tests where relevant. CSRs which are defined with certain reserved-for-future-use bits (either WPRI or WARL) are tested as being constant zero, masking for the reserved bits. At present the only supported value is 1.12, corresponding to version 1.12 of the Machine ISA from the 20211203 Privileged Architecture document.

The privilege modes defined in any of these sections do not prevent the CSR instruction check from expecting an illegal access exception based on the address.

LINKED ENTITIES

2 links
genchecks.py INTRODUCES
RVFI USES

CITATIONS

12 sources
12 citations
[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