SymbiYosys tutorial · Chapter 7 of 10 · 30 min

Verify the NERV RISC-V core with riscv-formal

riscv-formal checks a RISC-V processor against the RISC-V instruction-set specification withSymbiYosys. This chapter runs it on NERV, a small core in the riscv-formal repository: first one check, then all 96. It then injects a bug into the ADD instruction and reads the counterexample the check produces.

What are riscv-formal and RVFI?

riscv-formal is a set of formal checks for RISC-V cores, maintained by YosysHQ. A core under test reports every instruction it retires (completes) on a standard output port, the RISC-V Formal Interface (RVFI). For each instruction, RVFI carries the instruction word, the program counter, the source registers and their values, the destination register and the value written to it, and any memory access.

An instruction check compares those reported values with what the specification requires. The check for ADD, for example, computes rs1 + rs2 from the reported source values and asserts that the core wrote that result and advanced the program counter by 4. Other checks cover the register file, the program counter between instructions, memory buses and control registers.

How make check turns one configuration file into 96 SymbiYosys jobs, and what one instruction check compares.

NERV is a single-stage RISC-V processor written for teaching. The copy in riscv-formal is configured in cores/nerv/checks.cfg as rv32ib: the base 32-bit integer instructions plus the bit-manipulation extension, so its instruction checks include clz, rol and sh1add as well as add.

Get riscv-formal and generate the checks

Clone riscv-formal, check out the commit this chapter uses, and generate the checks for NERV:

$ cd ~/formal
$ git clone https://github.com/YosysHQ/riscv-formal
$ cd riscv-formal
$ git checkout c992aa6
$ cd cores/nerv
$ python3 ../../checks/genchecks.py

output (last lines)

Reading checks.cfg.
Creating checks directory.
Generated 96 checks.

genchecks.py reads checks.cfg and writes one job file per check into checks/, for example checks/insn_add_ch0.sby for ADD.

Run one instruction check

$ cd checks
$ sby -f insn_add_ch0.sby

output (last lines)

SBY 23:15:06 [insn_add_ch0] summary: engine_0 (smtbmc boolector) returned pass
SBY 23:15:06 [insn_add_ch0] summary: engine_0 did not produce any traces
SBY 23:15:06 [insn_add_ch0] DONE (PASS, rc=0)

The check takes about 7 seconds. It is a bmc job of depth 11 that inspects the instruction retiring at cycle 10, and the solver chooses the program. A PASS means that no program can make NERV retire an ADD at that cycle with a wrong result or a wrong next program counter.

The log also contains 53 warnings of the form Latch inferred for signal `\nerv.$fordecl_block$6.i …. They refer to for loop variables in nerv.sv and do not affect the result.

Run all 96 checks

Run every check. make clean must come first; the next section explains why.

$ cd ~/formal/riscv-formal/cores/nerv
$ make clean
$ make -j$(nproc) check

make check regenerates the checks, runs each one with sby, and writes a summary file. On a 4-core machine the run takes about four minutes and writes about 750 MB of work folders. All 96 checks pass:

Checks	Count
Instruction checks (insn_*)	66
Control and status register checks (csr*)	19
Memory bus checks (bus_*)	4
Register file, program counter forward and backward, uniqueness, causality, illegal instructions, cover	1 each, 7 in total

Read the summary file

cexdata/status.txt lists one line per check, sorted by run time, so the longest checks come last. Run times vary by a few seconds between runs, so your last lines may appear in a different order:

checks/insn_lh_ch0               pass      0:00:24
checks/bus_dmem_ch0              pass      0:00:25
checks/reg_ch0                   pass      0:00:42

Two problems can leave the summary empty or stale:

An empty summary. The summary script, cexdata.sh, calls gensub, a GNU awk function. Ubuntu's default awk is mawk, which lacks it: every check still runs and make finishes, but status.txt is empty and the output shows awk: line 2: function gensub never defined. Install gawk (Chapter 2, “What do you need before you start?”) and rebuild the summary with bash cexdata.sh; the checks do not need to run again.
A make check that runs nothing. The check target depends on a target named checks, which is also the name of the folder genchecks.py creates. When the folder exists, make treats that step as done and skips the checks. Run make clean first.

Inject a bug into the ADD instruction

NERV computes ADD on line 986 of nerv.sv as rs1_value + rs2_value. Replace + with |, bitwise OR. The two operations agree whenever the operands have no set bit in common, for example 1 + 2 = 1 | 2 = 3, so a test that uses such values cannot see the difference.

$ cd ~/formal/riscv-formal/cores/nerv
$ sed -i 's/next_rd = rs1_value + rs2_value; end/next_rd = rs1_value | rs2_value; end/' nerv.sv
$ grep -n "ADD  \*/" nerv.sv

output

986:					10'b 0000000_000 /* ADD  */: begin next_wr = 1; next_rd = rs1_value | rs2_value; end

The job files in checks/ name nerv.sv by its full path, so they use the edited file without being regenerated. Run the ADD check again:

$ cd checks
$ sby -f insn_add_ch0.sby

output (excerpt)

SBY 23:59:54 [insn_add_ch0] engine_0: ##   0:00:05  Assert failed in rvfi_testbench: rvfi_insn_check.sv:177.7-177.40 (_witness_.check_flatten_checker_inst__rvfi_insn_check_sv_177_assert_132)
SBY 23:59:55 [insn_add_ch0] summary: counterexample trace: insn_add_ch0/engine_0/trace.vcd
SBY 23:59:55 [insn_add_ch0] summary:   failed assertion rvfi_testbench._witness_.check_flatten_checker_inst__rvfi_insn_check_sv_177_assert_132 at rvfi_insn_check.sv:177.7-177.40 step 10
SBY 23:59:55 [insn_add_ch0] DONE (FAIL, rc=0)

The check fails in about 10 seconds. Line 177 of checks/rvfi_insn_check.sv is assert(spec_rd_wdata == rd_wdata);: the value the core wrote to the destination register differs from the value the specification requires.

Read the failing check

riscv-formal includes a script, disasm.py, that disassembles a counterexample, but it needs a RISC-V GCC toolchain and the Verilog_VCD Python package, which the OSS CAD Suite does not include. The following script needs only Python's standard library. It reads the RVFI signals from the trace and prints one line per retired instruction. Save it as ~/formal/rvfi_trace.py:

rvfi_trace.py

# Print the instructions a riscv-formal counterexample retires, one per line.
# Usage: python3 rvfi_trace.py trace.vcd
# Reads the RVFI signals under rvfi_testbench.wrapper; standard library only.
# Names register-register and register-immediate ALU instructions; prints
# other instructions as their machine code in hexadecimal.
import sys

NAMES = {"rvfi_valid", "rvfi_order", "rvfi_pc_rdata", "rvfi_insn",
         "rvfi_rs1_addr", "rvfi_rs1_rdata", "rvfi_rs2_addr", "rvfi_rs2_rdata",
         "rvfi_rd_addr", "rvfi_rd_wdata"}
R_TYPE = {(0, 0): "add", (32, 0): "sub", (0, 1): "sll", (0, 2): "slt",
          (0, 3): "sltu", (0, 4): "xor", (0, 5): "srl", (32, 5): "sra",
          (0, 6): "or", (0, 7): "and"}

I_TYPE = {0: "addi", 2: "slti", 3: "sltiu", 4: "xori", 6: "ori", 7: "andi"}

def name(insn):
    if insn & 3 != 3:
        return "0x%04x" % insn          # 16-bit compressed instruction
    opcode, funct3, funct7 = insn & 0x7f, (insn >> 12) & 7, insn >> 25
    if opcode == 0x33 and (funct7, funct3) in R_TYPE:
        return R_TYPE[funct7, funct3]
    if opcode == 0x13 and funct3 in I_TYPE:
        return I_TYPE[funct3]
    return "0x%08x" % insn

ids, scope, now, seen = {}, [], {}, {}
def sample():
    if now.get("rvfi_valid") == 1 and now["rvfi_order"] not in seen:
        seen[now["rvfi_order"]] = dict(now)

for line in open(sys.argv[1]):
    t = line.split()
    if not t:
        continue
    if t[0] == "$scope":
        scope.append(t[2])
    elif t[0] == "$upscope":
        scope.pop()
    elif t[0] == "$var" and scope == ["rvfi_testbench", "wrapper"] and t[4] in NAMES:
        ids[t[3]] = t[4]
    elif t[0].startswith("#"):
        sample()
    elif t[0][0] in "01" and t[0][1:] in ids:
        now[ids[t[0][1:]]] = int(t[0][0])
    elif t[0][0] == "b" and len(t) > 1 and t[1] in ids:
        now[ids[t[1]]] = int(t[0][1:].replace("x", "0"), 2)
sample()

for order in sorted(seen):
    v = seen[order]
    print("%3d  pc %08x  %-10s  rs1 x%-2d = %08x  rs2 x%-2d = %08x  rd x%-2d = %08x" % (
        order, v["rvfi_pc_rdata"], name(v["rvfi_insn"]),
        v["rvfi_rs1_addr"], v["rvfi_rs1_rdata"], v["rvfi_rs2_addr"],
        v["rvfi_rs2_rdata"], v["rvfi_rd_addr"], v["rvfi_rd_wdata"]))

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

output

  1  pc 00000000  0x544d0bef  rs1 x26 = 00000002  rs2 x4  = 00000000  rd x23 = 00000004
  2  pc 000d0544  0x7e3b0be7  rs1 x22 = fffff846  rs2 x3  = 00000006  rd x23 = 000d0548
  3  pc 00000028  0xff6b9e63  rs1 x23 = 000d0548  rs2 x22 = fffff846  rd x0  = 00000000
  4  pc fffff824  0xfda49b03  rs1 x9  = 0000001c  rs2 x26 = 00000002  rd x22 = fffff846
  5  pc fffff828  add         rs1 x22 = fffff846  rs2 x22 = fffff846  rd x4  = fffff846

Each line shows the instruction's position in program order, its program counter, the instruction, and the registers it read and wrote, in hexadecimal. The script names register-register and register-immediate ALU instructions; it prints the others as their machine code.

Line 5 is the ADD that the check inspects: add x4, x22, x22. Both source values are 0xfffff846, so the specification requires 0xfffff846 + 0xfffff846 = 0xfffff08c (keeping 32 bits). The core wrote 0xfffff846, which is 0xfffff846 | 0xfffff846. The solver chose equal operands, the simplest case in which OR and addition differ. The four earlier instructions set up those register values.

How do you view the same trace in GTKWave?

Open it with gtkwave insn_add_ch0/engine_0/trace.vcd and add the rvfi_* signals under rvfi_testbench.wrapper. The script prints the same values as text.

Restore the original core

riscv-formal is a Git repository, so restore the original file with Git and confirm that ADD passes again:

$ cd ~/formal/riscv-formal/cores/nerv
$ git checkout nerv.sv
$ cd checks
$ sby -f insn_add_ch0.sby

output (excerpt)

Updated 1 path from the index
SBY  0:00:03 [insn_add_ch0] DONE (PASS, rc=0)