The following formal test are performed to verify ISA compliance of RISC-V processors with riscv-formal. Depending on aspects like the strength of safety properties present in the core, the overall complexity of the core, and the verification requirements for the given application, the following tests might be set up as bounded model checks or as unbounded verification tasks.

Configuring check generation

A config file with extension .cfg is used to configure the genchecks.py script. By default, the name of this config file is expected to be checks. Calling genchecks.py with an argument will instead use the provided name. For example, python3 ../../checks/genchecks.py tests will load config settings from a file named tests.cfg. Note that the script will generate a folder with the same config name in the directory it is run.

It is expected for genchecks.py to be called from a subdirectory of the cores folder, such that the script is called as ../../checks/genchecks.py, and the subdirectory is the name of the core. This core name will be used for naming certain intermediary files, but is otherwise arbitrary and does not need to match anything else.

The config file consists of a number of sections, with each section starting with the name of the section in square brackets. Some of these sections are shared between tests, and some are used only for specific formal checks. The shared sections will be covered here, while check specific details will be covered in the relevant section below.

Comments can be included in the config file by prefixing a line with a # character.

[options]

This section primarily contains options which describe the core under test. Possible options are listed below, along with their expected value. For options with no expected value, simply including the option enables the specified effect.

Option	Value	Description
isa	String	ISA extensions, e.g. RV64IMAFD, or rv32i. Refer to the Supported ISAs section below for more information.
nret	Integer	The number of channels for the RVFI port. Defaults to 1.
blackbox	None	Signifies register file and ALU should be black-boxed.
solver	String	Name of solver, defaults to boolector.
dumpsmt2	None	Passed to smtbmc engine to output SMT2 trace.
abspath	None	Generated makefile will use absolute path of generated files.
mode	String	Solver mode, currently supports either bmc or prove, and defaults to bmc.

Supported ISAs

The following RISC-V ISA modules are supported for testing:

Module	Version	Notes
rv32i	2.1	Base integer instruction set (32bit).
rv64i	2.1	Base integer instruction set (64bit).
c	2.0	Extension for compressed instructions.
m	2.0	Extension for integer multiplication and division.
Zicsr	2.0	CSRs are handled separately and “Zicsr” should not be included in the isa string. See CSR checks.
b	1.0	Extension for bit manipulation, comprising instructions provided by the Zba, Zbb, and Zbs extensions.
Zba	1.0	Address generation.
Zbb	1.0	Basic bit-manipulation.
Zbc	1.0	Carry-less multiplication.
Zbs	1.0	Single-bit instructions.
Zbkb	1.0	Bit-manipulation for cryptography.
Zbkc	1.0	Carry-less multiplication for cryptography.
Zbkx	1.0	Crossbar permutations.

Instruction tests are available for each extension with both rv32i and rv64i base instruction sets, e.g. isa rv32iZbc. Support for multiple extensions in the same configuration file is currently limited, with only the following combinations available by default:

• rv32imc
• rv32iZba_Zbb_Zbc_Zbs
• rv32iZbkb_Zbkc_Zbkx
• rv64imc
• rv64iZba_Zbb_Zbc_Zbs
• rv64iZbkb_Zbkc_Zbkx

Warning

The isa string is currently case-sensitive and should match values in the above table exactly for instruction test generation.

Generating new combinations locally

Additional combinations can be generated locally as needed with the insns/generate.py script. First off, find the following section of code:

## Additional ISA combinations
isa_propagate("Zba_Zbb_Zbc_Zbs")
isa_propagate("Zbkb_Zbkc_Zbkx")

Add the desired combination(s), e.g. isa_propagate("mcb"), and then run the script with python3 generate.py. Each combination should generate a corresponding .txt and .v file that are used for testing.

[depth]

This section provides the execution depth to be used by the solver for each test. The name of the check is listed, followed by one or more integers separated by a space. For formal checks that expect multiple values to be provided here, the meaning of each will be defined in the relevant section.

For cores with multiple channels, the channel number can be used in the name of the check by appending _ch#. Note that a more specific name will be used over a less specific name. For example, if insn <depth0> and insn_ch1 <depth1> are both listed, insn tests on channel 1 will use depth1, while all other channels will use depth0.

If a formal check does not have a corresponding depth listed, it will not be generated. For example, providing reg_ch2 <values> but not reg <values> will run the reg check only on channel 2.

[groups]

This section defines a list of group names which are prepended to all check names which can then be used for grouping multiple checks together. These groups can then be used for testing with multiple depth values. Each group must be separated by whitespace.

As an example, if groups a and b are listed with depth settings of a_insn <x>, b_insn_bne <y>, then all instructions will be tested with depth x, and the bne instruction will be tested to both depths x and y.

[sort]

If this section is included, any listed checks will be run in the order they appear in this list, and will be run before any un-listed checks. Each item should be placed on its own line. When multiple checks match the same ordering, alphabetical order will be used.

Note that regex is used to search for a match of the full check name, including group and channel. This can be used to, for example, list all checks on channel 2 before any others by adding .*?_ch2 as the first item. If the user is unfamiliar with regex, simply providing the names of checks verbatim will also work.

Note that this sorting also determines the order in which checks are generated in the makefile. The order in which tests are started should be maintained by Make, however if parallelism is enabled then there is no guarantee that tests will complete in this order.

[filter-checks]

Specific checks can be enabled or disabled by adding them to this section prefixed with either a + or - and a space. As with [sort] above, regex is used for matching against each line. Note that the first match returns. For example, if + insn_(mul|div)_ch1 is listed before - insn_.*_ch1, then the mul and div instructions will be enabled for testing on channel 1, while all other instructions are disabled.

[assume]

Each line of this section provides a two value tuple. The first value is the regex pattern used to match the current check name, while the second value is code to be included in the file assume_stmts.vh. If the first value begins with a !, the code is used for all checks that do not match the pattern, otherwise the code is used for all checks that do match. This file is included verbatim at the end of the rvfi_testbench module in checks/rvfi_testbench.sv, and so should be valid System Verilog code.

Verbatim sections

A number of sections are included in the sby script essentially as-is. These sections are formatted with a few keyword substitutions. If using these substitutions, the keywords should be prepended and appended with a @ symbol, e.g. @basedir@/cores/@core@/wrapper.sv is using the basedir and core keywords to define the path.

Possible keywords include:

• basedir: the root directory of riscv-formal
• core: the name of the directory from which the script is executed
• ilang_file: filename of intermediary output
• channel: the current rvfi channel
• check: the current check, e.g. csrc
• checkch: the full name of the current check, e.g. a_csrc_misa_ch0

[script-defines]

This section is included at the start of the sby [script] section. Check specific code can also be included as [script-defines <check>], where <check> is the current check.

[verilog-files] and [vhdl-files]

These sections list all of the core source files which should be included in testing. All verilog files will be listed after read -sv, while all vhdl files will be listed after read -vhdl.

[script-sources]

This section can be used to add any other source files which do not fit under -sv or -vhdl, and is included before the prep command.

[script-link]

This section is included after the prep command and before chformal.

[defines]

This section is included as part of [file defines.sv]. Check specific code can also be included as [defines <check>], where <check> is the current check.

Standard checks

The following checks are managed by genchecks.py and can be implemented using the standard RVFI wrapper interface.

Instruction checks

The majority of formal checks needed to verify a core with riscv-formal are instruction checks (one per RVFI channel and RISC-V instruction supported by the core).

Instruction checks test if the instruction (rvfi_insn) matches the state transistion described by the other RVFI signals.

PC checks

There are two PC checks: pc_fwd and pc_bwd. Both of them are run for each RVFI channel.

The pc_fwd check assumes that the core retires an instruction at the end of the bounded model check, and that the previous instruction in the program (rvfi_order-1) was retired earlier. It then tests if rvfi_pc_wdata of the previous instruction matches rvfi_pc_rdata of the next instruction.

pc_bwd is like pc_fwd but for pairs of instructions that have been executed out of order: The check assumes that the core retires an instruction at the end of the bounded model check, and that the next instruction in the program (rvfi_order+1) was retired earlier. It then tests if rvfi_pc_wdata of the previous instruction matches rvfi_pc_rdata of the next instruction.

[depth] section

Expects two values: first is the number of cycles to reset for; second is the execution depth.

Register checks

This checks if writes to and reads from the register file are consistent with each other, i.e. if the value written to a register matches the value read from the register file by a later instructions.

This check assumes that the last instruction at the end of the bounded model check, reads a register. It then checks that the value read is consistent with the matching write to the same register by an earlier instruction.

[depth] section

Expects two values: first is the number of cycles to reset for; second is the execution depth.

Causality

There are three causality checks: causal, causal_mem and causal_io.

The core may retire instructions out-of-order as long as causality is preserved. (This means a write must be retired before the reads that depend on it.)

The causal check tests if the instruction stream is causal with respect to registers. The causal_mem check tests if the instruction stream is causal with respect to memory. The causal_io check tests if the instruction stream is causal with respect to i/o memory, where every i/o memory access is assumed to depend on all earlier i/o memory accesses.

Which areas of the adress space are considered to be i/o memory can be configured using the RISCV_FORMAL_IOADDR(addr) macro.

[depth] section

Expects two values: first is the number of cycles to reset for; second is the execution depth.

Liveness

This check makes sure that the core never freezes (unless an instruction with rvfi_halt asserted is retired): This check assumes that an instruction is retired at a configurable trigger point in the middle of the bounded model check. It then checks that the next instruction (rvfi_order+1) is also retired at some point during the span of the bounded model check.

It might be neccessary to add some bounded fairness constraints to the design for this check to succeed.

[depth] section

Expects three values: first is the number of cycles to reset for; second is the trigger depth; and third is the execution depth.

Uniqueness

This check makes sure that no two instructions with the same rvfi_order are retired by the core.

[depth] section

Expects three values: first is the number of cycles to reset for; second is the trigger depth; and third is the execution depth.

Faults

This check makes sure that dynamically occuring memory faults are handled. It requires defining RISCV_FORMAL_MEM_FAULT and the rvfi_mem_fault, rvfi_mem_fault_rmask and rvfi_mem_fault_wmask signals. When the mcause CSR is exposed via RVFI, this will also check that it is correctly updated on a memory fault.

[depth] section

Expects two values: first is the number of cycles to reset for; second is the execution depth.

Cover

A formal check using cover() SystemVerilog statements for various interesting RVFI events or sequences of events. The purpose of this formal check is to collect some data about the required bounds to reach certain states to set the bounds for the other bounded model checks. This check can also be used for creating witness traces, for example to examine the conditions under which a specific CSR bit goes high.

[depth] section

Expects two values: first is the number of cycles to reset for; second is the execution depth.

[cover] section

All code in this section is included verbatim in the file cover_stmts.vh, which is included verbatim in checks/rvfi_cover_check.sv, and so should be valid System Verilog code.

Standard bus checks

The following checks are managed by genchecks.py and can be implemented using the standard RVFI wrapper interface when implementing the RVFI_BUS extension.

Instruction bus memcheck

The bus_imem check adds a memory abstraction that only emulates a single word of memory (at an unconstrained address). This memory word is read-only and has an unconstrained value. The check makes sure that instructions fetched from this memory word are handled correctly and that the data from that memory word makes its way into rvfi_insn unharmed.

When the granularity of access faults as observed from the core is coarser than the width of the bus, RISCV_FORMAL_FAULT_WIDTH needs to be defined and set to the corresponding width in bytes. E.g. for a setup where a single word fault the monitored bus means that from the perspective of the core, any access of the corresponding cache line will fault, you would define RISCV_FORMAL_FAULT_WIDTH to be the width of a cache line in bytes.

Instruction bus fault memcheck

The bus_imem_fault check adds a memory abstraction that has a single always faulting word of memory (at an unconstrained address). The check makes sure that executing from this address causes an “instruction access fault” trap.

The RVFI signalling for the instruction with a faulting fetch requires an all-zero rvfi_insn value with rvfi_trap set. When RISCV_FORMAL_MEM_FAULT is defined the associated signals must also be set correctly.

Data bus memcheck

This bus_dmem check adds a memory abstraction that only emulates a single word of memory (at an unconstrained address). The memory word is read/write. The check tests if writes to and reads from the memory location (as reported via RVFI) are consistent. Additionally it checks that an initial value as reported via RVFI matches the fetched value on the bus. This check does not require writes to appear on the bus and is thus compatible with caches between the core and the observed bus.

When the granularity of access faults as observed from the core is coarser than the width of the bus, RISCV_FORMAL_FAULT_WIDTH needs to be defined. See “Instruction Bus Memcheck” above for more details.

Data bus fault memcheck

The bus_dmem_fault check adds a memory abstraction that has a single always faulting word of memory (at an unconstrained address). The check makes sure that reading from or writing to this address causes a “load access fault” or “store/AMO access fault” trap respectively.

The RVFI signalling for an instruction causing either fault has rvfi_trap and does not include a register update or memory write, even if the instruction would have performed one if the memory access didn’t fault. When RISCV_FORMAL_MEM_FAULT is defined the associated signals must also be set correctly.

Data bus I/O checks

These checks can provide stronger guarantees on data bus accesses that are not required to hold in general, but should often hold for i/o memory regions. Depending on the use-case only a subset may be applicable or some checks may only be applicable for certain areas of the address space. The memory addresses for which these checks are run can be configured using the RISCV_FORMAL_IOADDR(addr) macro.

Data bus I/O reads

The bus_dmem_io_read check makes sure that every retired non-faulting i/o memory read access appears as an individual read on the bus. The whole read has to appear on its own in a single RVFI_BUS cycle. A read is allowed to also read adjacent bytes within the same RVFI_BUS cycle.

Data bus I/O read faults

The bus_dmem_io_read_fault check makes sure that every retired faulting i/o memory read access appears as an individual faulting read on the bus.

Data bus I/O writes

The bus_dmem_io_write check makes sure that every retired non-faulting i/o memory write access appears as an individual write on the bus. The whole write has to appear on its own in a single RVFI_BUS cycle and may not write any additional adjacent bytes.

Data bus I/O write faults

The bus_dmem_io_write_fault check makes sure that every retired faulting i/o memory write access appears as an individual faulting write on the bus.

Data bus I/O ordering

The bus_dmem_io_order check makes sure that all i/o memory accesses appear in-order on the bus. This is done by checking that every pair of adjacent i/o memory accesses (as observed via RVFI) corresponds to adjacent i/o memory accesses on the bus. Non-i/o accesses are ignored by this check, so they can be arbitrarily reordered relative to i/o accesses and relative to each other.

CSR checks

The following checks are managed by genchecks.py and can be implemented using the standard RVFI wrapper interface. All checks operate on one channel at a time and may not work correctly if a CSR is able to be modified by more than one channel.

CSR instruction check

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

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

A valid read instruction must assign rvfi_csr_<csrname>_rdata to rvfi_rd_wdata, as well as the correct rvfi_rd_addr. A valid write instruction must assign the correct value to rvfi_csr_<csrname>_wdata. And any illegal accesses should result in a trap.

Illegal CSR access

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

CSR consistency checks

These checks perform multiple reads/writes and compare the values on rvfi_csr_<csrname>_rdata and rvfi_csr_<csrname>_wdata during the check cycle.

In each case, RISCV_FORMAL_CSRC_NAME <csrname> must be defined for the CSR under test, along with the corresponsing csr_{m,s,u}index_<csrname> <csraddr>.

CSR write-any

The csrc_any check tests whether any value written to a CSR is then able to be read-back exactly as written.

CSR increments

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

CSR up-counter

The csrc_upcnt check is similar to the CSR increments check but with more constraints. First, no writes of the csr under test are allowed. Second, the test value must be greater than the previously read value. Without fairness guarantees this has limited use, but can verify some hpm functions, especially mcycle and minstret.

CSR hpm event cover check

Unlike most of the other checks, csrc_hpm is a cover check. Similarly to the CSR up-counter check, the value of a hpm counter CSR is compared with a previously stored value and must increase. However, because this is a cover check this 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 can verify that the hpm is able to increase and unable to decrease.

This check must be performed on a hpm event CSR, with RISCV_FORMAL_CSRC_NAME mhpmevent# and RISCV_FORMAL_CSRC_HPMCOUNTER mhpmcounter#. The event must be defined by RISCV_FORMAL_CSRC_HPMEVENT <value>. Note that both RISCV_FORMAL_CSR_MHPMCOUNTER# and RISCV_FORMAL_CSR_MHPMEVENT# must be defined and the corresponding rvfi signals connected.

CSR read-constant

The csrc_const check 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 so long as it remains constant during operation, a value of rdata_shadow can be assigned which will compare with the previously read value.

CSR read-zero

The csrc_zero check is similar to the CSR read-constant check, but exclusively tests for a constant value of all zero.

genchecks config

[depth]

The csrw and csr_ill checks expect one value, indicating the maximum depth of the Bounded Model Checker (BMC).

All csrc_* checks expect two values, with the first being the number of cycles to hold reset for, and the second being the maximum depth of the BMC.

Depth can be specified for all tests of one type, e.g. csrc_zero, or individual to a particular CSR, e.g. csrw_mcycle.

Any test without a corresponding value in the depth section will not be run.

[csrs]

The csrs config section lists all standard CSRs which can be tested. By default, all CSRs will be run through the CSR instruction check (csrw). Consistency checks can be defined as a space seperated list after the csr name. For checks which expect a value, using quotation marks will allow for verbatim values.

e.g. misa zero const="32'h 0" declares two tests for the misa CSR. First using the csrc_zero_check, and then using the csrc_const_check with RISCV_FORMAL_CSRC_CONSTVAL defined as 32'h 0.

Each named CSR must be connected as described in the RISC-V Formal Interface (RVFI).

Consistency checks can be appended with _mask= with a verilog expression which will be applied to the CSR as a bit mask before testing the return value. Note that _mask must be defined after any other value assignment for the check. For example, the statement misa const=0_mask="32'h 0aaa_ffff" masks the misa CSR and then checks for a constant value of 0. A mask value is currently only supported in the const, zero, and any checks.

const supports value assignment, while hpm requires it. If no value is provided for const, a value of rdata_shadow will be assigned such that any value is accepted provided it is constant. In the case of hpm the value is assigned to the hpmevent register prior to testing if the hpmcounter register is able to increase.

[custom_csrs]

Platform defined CSRs can be included for testing in the custom_csrs section. Each line is a space separated list of values defining one CSR and the corresponding tests. The first value is the CSR address in hexadecimal, and the second value is the privilege modes in which the CSR is available. The rest of the line follows the same format as the csrs config section with the CSR name followed by any tests in addition to csrw.

e.g. fc0 m custom_ro const="32'h dead_beef" defines a CSR in the machine-level custom read-only address space at address 0xFC0 called custom_ro which can be accessed from machine mode and should be tested for a constant value of 0xdeadbeef using csrc_const_check.

As with the standard CSRs, each of the custom CSRs must be connected through the RVFI wrapper.

Note that the privilege modes defined will not prevent the CSR instruction check from expecting an illegal access exception based on the address.

[illegal_csrs]

The illegal_csrs section lists unnamed CSRs not available through the RVFI wrapper interface. Each line lists one CSR address to be tested with csr_ill, along with the relevant modes to check. Three space separated values are expected; the first provides the address in hexadecimal, the second is the privilege modes to test, and the third indicates whether to test reads and writes or just writes.

e.g. fff msu rw defines a test at address oxFFF for machine, supervisor, and user modes which should cause an illegal access exception on both reads and writes.

CSR spec test generation

By setting csr_spec in the options section, it is possible to automatically generate tests for all CSRs to match the specification recommendations/requirements. This option will add all defined CSRs to be tested under csrw as well as generating corresponding csrc tests where relevant. For those CSRs which should only exist in certain conditions, e.g. if U mode is available, then those CSRs are included if the isa option includes them, otherwise the addresses are checked as being an expected illegal access exception. Optional CSRs are not automatically tested and will need to be specified as described above. CSRs which are defined with certain bits being reserved for future use (either WPRI or WARL) are tested as being constant zero, masking for just the reserved bits.

At present the only supported value for csr_spec is 1.12, corresponding to version 1.12 of the Machine ISA, as defined in the 20211203 Priveleged Architecture document.

Other checks

The following checks are not yet managed by genchecks.py and can not be implemented using the standard RVFI wrapper interface. Some of them may be integrated with genchecks.py in the future.

Instruction memcheck

This check adds a memory abstraction that only emulates a single word of memory (at an unconstrained address). This memory word is read-only and has an unconstrained value. The check makes sure that instructions fetched from this memory word are handled correctly and that the data from that memory word makes its way into rvfi_insn unharmed.

See imemcheck.sv in cores/picorv32/ for an example implementation.

This check is superseded by the equivalent standard bus check above.

Data memcheck

This check adds a memory abstraction that only emulates a single word of memory (at an unconstrained address). The memory word is read/write. The check tests if writes to and reads from the memory location (as reported via RVFI) are consistent.

See dmemcheck.sv in cores/picorv32/ for one possible implementation of this test.

This check is superseded by the equivalent standard bus check above.

Checking for equivalence of core with and without RVFI

An equivalence check of the core with and without RVFI (with respect to the non-RVFI outputs) is performed. This proves that the verification results for the core with enabled RVFI also prove that the (non-RVFI) production core is correct without extra burden on the core designer to isolate the RVFI implementation from the rest of the core.

See equiv.sh in cores/picorv32/ for an example implementation.

Complete

An additional check to make sure the core can not (without trap) retire any instructions that are not covered by the riscv-formal instruction checks.

See complete.sv in cores/picorv32/ for one possible implementation of this test.

Verification of riscv-formal models against spike models

The checks in tests/spike/ use the Yosys SimpleC back-end and CBMC to check the riscv-formal models and the C instruction models from spike for equivalence.