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 genchecks.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.
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.
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.
The core may retire instructions out-of-order as long as causality is preserved. (This means a register write must be retired before the register reads that depend on it.) This check tests if the instruction stream is causal with respect to registers.
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.
This check makes sure that no two instructions with the same rvfi_order are retired by the core.
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 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.
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.
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.
See cover.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.