SymbiYosys tutorial · Chapter 8 of 10 · 25 min

Find PicoRV32's built-in test bugs with riscv-formal

PicoRV32 contains five deliberate bugs that riscv-formal is meant to find. This chapter checks the correct core, then switches on two of the bugs and finds each one with a different check. It uses the riscv-formal repository and the rvfi_trace.py script from Chapter 7.

What is PicoRV32, and what are its test bugs?

PicoRV32 is a RISC-V processor by Claire Xenia Wolf; its README calls it a size-optimized RISC-V CPU. The copy that riscv-formal checks is configured in cores/picorv32/checks.cfg as rv32imc: the base integer instructions with multiply and divide and the 16-bit compressed instructions. Its repository is archived; its README states that the core is no longer under active development and refers to riscv-formal for verifying it.

picorv32.v contains five test bugs, each compiled only when the macro PICORV32_TESTBUG_001 to PICORV32_TESTBUG_005 is defined. Two change what the core stores; three change only what it reports on RVFI.

Where the five test bugs sit, and the two checks this chapter runs.

Download PicoRV32 and generate the checks

The PicoRV32 folder in riscv-formal downloads picorv32.v from the core's repository. Download the commit this chapter uses, confirm the file size, and generate the checks:

$ cd ~/formal/riscv-formal/cores/picorv32
$ curl -L -o picorv32.v https://raw.githubusercontent.com/YosysHQ/picorv32/ef203c2b0a3f/picorv32.v
$ stat -c %s picorv32.v
$ python3 ../../checks/genchecks.py

output (last lines)

94657
Reading checks.cfg.
Creating checks directory.
Generated 87 checks.

Check the correct core

Run the ADD instruction check and the register-file check on the correct core:

$ cd checks
$ sby -f insn_add_ch0.sby
$ sby -f reg_ch0.sby

output (DONE lines)

SBY  0:00:52 [insn_add_ch0] DONE (PASS, rc=0)
SBY  0:03:50 [reg_ch0] DONE (PASS, rc=0)

The ADD check takes about 18 seconds. The register-file check takes about three minutes, because a PASS requires the solver to rule out every program up to the check's depth.

insn_add_ch0 checks one ADD: the reported result, destination register and next program counter must match the specification for the reported source values.
reg_ch0 checks the register file across instructions: when one instruction writes a value to a register, a later instruction that reads the register must receive that value.

Switch on test bug 001 and find it

Test bug 001 makes the core write each result to register rd ^ 1 instead of rd, for example to x17 instead of x16. To compile it, copy the configuration with the macro changed and generate a second set of checks in the folder testbug001:

$ cd ~/formal/riscv-formal/cores/picorv32
$ sed "s/PICORV32_TESTBUG_NONE/PICORV32_TESTBUG_001/" checks.cfg > testbug001.cfg
$ python3 ../../checks/genchecks.py testbug001
$ cd testbug001
$ sby -f reg_ch0.sby
$ sby -f insn_add_ch0.sby

output (excerpt)

Reading testbug001.cfg.
Creating testbug001 directory.
Generated 87 checks.
SBY  0:03:57 [reg_ch0] engine_0: ##   0:00:05  Assert failed in rvfi_testbench: rvfi_reg_check.sv:42.6-42.59 (_witness_.check_flatten_checker_inst__rvfi_reg_check_sv_42_assert_29)
SBY  0:03:58 [reg_ch0] summary:   failed assertion rvfi_testbench._witness_.check_flatten_checker_inst__rvfi_reg_check_sv_42_assert_29 at rvfi_reg_check.sv:42.6-42.59 step 25
SBY  0:03:58 [reg_ch0] DONE (FAIL, rc=0)
SBY  0:04:17 [insn_add_ch0] DONE (PASS, rc=0)

The register-file check fails in about 7 seconds. Line 42 of checks/rvfi_reg_check.sv asserts that the value read from a register equals the value last written to it. The trace shows the failure:

$ python3 ~/formal/rvfi_trace.py reg_ch0/engine_0/trace.vcd

output

  0  pc 00000000  0xea71      rs1 x12 = 7ffffffc  rs2 x0  = 00000000  rd x0  = 00000000
  1  pc 000000d4  0x0301080f  rs1 x2  = 00000000  rs2 x16 = 00000000  rd x16 = 00000004
  2  pc 000000d8  addi        rs1 x16 = 00000000  rs2 x0  = 00000000  rd x16 = fffffff0

Instruction 1 reports that it wrote 4 to x16. Instruction 2 reads x16 and receives 0, because the core stored the 4 in x17. Instruction 0 is a 16-bit compressed instruction, which the script prints as four hexadecimal digits.

The ADD check passes on the same faulty core. It examines one ADD and compares the reported result with the reported source values; the core still reports the destination register correctly, so each report is consistent on its own. Only a check that follows a value from one instruction to the next can see this bug.

Switch on test bug 004 and find it

Test bug 004 leaves the computation correct but flips bit 0 of the result that the core reports on RVFI. Generate its checks and run the ADD check:

$ cd ~/formal/riscv-formal/cores/picorv32
$ sed "s/PICORV32_TESTBUG_NONE/PICORV32_TESTBUG_004/" checks.cfg > testbug004.cfg
$ python3 ../../checks/genchecks.py testbug004
$ cd testbug004
$ sby -f insn_add_ch0.sby
$ python3 ~/formal/rvfi_trace.py insn_add_ch0/engine_0/trace.vcd

output (excerpt)

SBY  0:04:23 [insn_add_ch0] engine_0: ##   0:00:03  Assert failed in rvfi_testbench: rvfi_insn_check.sv:177.7-177.40 (_witness_.check_flatten_checker_inst__rvfi_insn_check_sv_177_assert_86)
SBY  0:04:23 [insn_add_ch0] summary:   failed assertion rvfi_testbench._witness_.check_flatten_checker_inst__rvfi_insn_check_sv_177_assert_86 at rvfi_insn_check.sv:177.7-177.40 step 20
SBY  0:04:23 [insn_add_ch0] DONE (FAIL, rc=0)
  0  pc 00000000  0xc0202073  rs1 x0  = 00000000  rs2 x0  = 00000000  rd x0  = 00000000
  1  pc 00000004  0x01ef3fef  rs1 x0  = 00000000  rs2 x0  = 00000000  rd x31 = 00000009
  2  pc 000f3022  0xffffffef  rs1 x0  = 00000000  rs2 x0  = 00000000  rd x31 = 000f3027
  3  pc 000f3020  add         rs1 x15 = fff0cfd8  rs2 x31 = 000f3026  rd x31 = ffffffff

The ADD check fails in about 6 seconds, on line 177 of rvfi_insn_check.sv, the result comparison that also caught NERV's bug in Chapter 7, “Inject a bug into the ADD instruction”. Instruction 3 is add x31, x15, x31: 0xfff0cfd8 + 0x000f3026 = 0xfffffffe, but the core reports 0xffffffff, with bit 0 flipped.

Which check catches which test bug?

Running both checks against each test bug, in the same way, gives the table below. Each FAIL takes under 30 seconds; a register-file PASS takes about three minutes.

Test bug	What it changes	insn_add_ch0	reg_ch0
None	Nothing	PASS	PASS
001	The core writes register rd ^ 1	PASS	FAIL
002	The core writes the result with bit 0 flipped	PASS	FAIL
003	RVFI reports destination register rd ^ 1	FAIL (line 176: destination)	FAIL
004	RVFI reports the result with bit 0 flipped	FAIL (line 177: result)	FAIL
005	RVFI reports the next program counter ^ 4	FAIL (line 178: next PC)	PASS

Bugs in what the core stores (001, 002) are invisible to an instruction check, because each instruction's report remains consistent. The register-file check follows values between instructions and catches both.
Bugs in what the core reports (003, 004, 005) make an instruction's report disagree with the specification, so the instruction check catches all three.
Test bug 005 changes only the reported program counter, which the register-file check does not examine.