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.
For most cores the easiest approach is to create a wrapper HDL module and a checks.cfg file and
use the genchecks.py scripts to create the formal checks. See
cores/picorv32/ for an example implementation. The checks generated by
genchecks.py are bounded model checks which use sby for verification.
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.
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. Note that X and Z extensions are not currently supported and should be removed from the string. |
| 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. |
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.
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.
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.
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.
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.
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
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.
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.
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.
This section is included after the prep command and before chformal.
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.
The following checks are managed by genchecks.py and can be implemented using the standard RVFI wrapper interface.
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.
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.
Expects two values: first is the number of cycles to reset for; second is the execution depth.
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.
Expects two values: first is the number of cycles to reset for; second is the execution depth.
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.
Expects two values: first is the number of cycles to reset for; second is the execution depth.
Expects two values: first is the number of cycles to reset for; second is the execution depth.
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.
Expects three values: first is the number of cycles to reset for; second is the trigger depth; and third is the execution depth.
This check makes sure that no two instructions with the same rvfi_order are retired by the core.
Expects three values: first is the number of cycles to reset for; second is the trigger depth; and third is the execution depth.
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.
Expects two values: first is the number of cycles to reset for; second is the execution depth.
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.
Expects two values: first is the number of cycles to reset for; second is the execution depth.
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.
The following checks are managed by genchecks.py and can be implemented using the standard RVFI wrapper interface when implementing the RVFI_BUS extension.
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.
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.
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.
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.
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.
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.
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.
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.
The bus_dmem_io_read_fault check makes sure that every retired faulting i/o memory write access appears as an individual faulting write on the bus.
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.
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.
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.
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.
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>.
The csrc_any check tests whether any value written to a CSR is then able to be read-back exactly
as written.
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.
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.
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.
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.
The csrc_zero check is similar to the CSR read-constant check, but exclusively tests for a
constant value of all zero.
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.
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 RVFI specification.
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.
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.
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.
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.
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.
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.
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.
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.
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.
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.