SymbiYosys tutorial · Chapter 9 of 10 · 20 min
Check a refactored design for equivalence with EQY
An equivalence check compares two versions of a design instead of checking one design against assertions. This chapter runs EQY on NERV, the RISC-V core from Chapter 7. It finds a bug injected into a refactored shifter, proves the corrected refactor equivalent to the original, and checks a synthesized netlist against its source.
What does an equivalence check prove?
Chapters 3 to 8 check a design against properties: assertions that you write. An equivalence check needs no properties. It compares two versions of the same design and proves that they behave the same: given the same inputs, they produce the same outputs.
The two versions are called gold and gate. The gold design is the known-good reference; the gate design is the version to be checked. The README of the example in this chapter names two uses: ensuring that a synthesis tool has not introduced functional changes into a design, or ensuring that a design refactor preserves correctness in all conditions
. This chapter does both.
How does EQY check two designs?
EQY is “a front-end driver program for Yosys-based formal hardware equivalence checking”. It does for an equivalence check what sby does for a property check: it reads a configuration file, runs Yosys and the proof engines, and reports one verdict. The OSS CAD Suite includes it. A run has four stages, which EQY reports as it goes:
- Read. Yosys reads the gold design and the gate design, each with its own script.
- Match. EQY pairs the nets that have the same name in both designs. A matched net is a point where the two designs must agree.
- Partition. EQY splits both designs into partitions: small pieces of logic whose inputs and outputs are matched nets. Each partition is named after the net it drives.
- Prove. For each partition, EQY writes a miter: a module that drives the gold and the gate copy of the partition with the same inputs and asserts that their outputs are equal. A strategy then proves the miter. The
sby strategy runs each miter as a SymbiYosys job in prove mode.
The designs are equivalent when every partition is proved. Because each partition is a separate proof, a failure names the part of the design where the two versions differ.
Copy the example out of the suite
The suite includes EQY's NERV example. Copy it into your project folder:
$ cp -r ~/tools/oss-cad-suite/examples/eqy/nerv ~/formal/eqy-nerv
$ cd ~/formal/eqy-nerv
The table lists the files in the folder and what each one is.
| File | What it is |
|---|
nerv.sv | The original NERV core: the gold design. |
nerv_change.sv | The refactored core: the gate design. Defining SHIFTER_BUG injects a bug. |
nerv_change_fail.eqy | Checks the refactored core, with the bug, against the original. |
nerv_change_pass.eqy | Checks the refactored core, without the bug, against the original. |
nerv_synth.v | A netlist of nerv.sv written by Yosys's synth command. |
nerv_synth.ys | The Yosys script that wrote nerv_synth.v. |
nerv_synth.eqy | Checks the netlist against nerv.sv. |
Makefile, README.md | Run the three checks; explain the example. |
What did the refactor change?
In nerv.sv, each of the six shift instructions (SLL, SRL, SRA and their immediate forms) has its own shift operation. nerv_change.sv moves all six into one shifter. Compare the two files:
$ diff nerv.sv nerv_change.sv
output
124a125,136
> // new shifter code
> function [31:0] bitreverse(input [31:0] arg);
> for (integer i = 0; i < 32; i++) bitreverse[i] = arg[31-i];
> endfunction
> wire [32:0] shift_t1 = {insn_funct7[5] && rs1_value[31], insn_funct3 == 3'b001 ? bitreverse(rs1_value) : rs1_value};
> `ifdef SHIFTER_BUG
> wire [31:0] shift_t2 = $signed(shift_t1) >>> (insn_opcode == OPCODE_OP_IMM ? insn[24:20] : rs2_value[5:0]);
> `else
> wire [31:0] shift_t2 = $signed(shift_t1) >>> (insn_opcode == OPCODE_OP_IMM ? insn[24:20] : rs2_value[4:0]);
> `endif
> wire [31:0] shift_out = insn_funct3 == 3'b001 ? bitreverse(shift_t2) : shift_t2;
>
316,318c328,330
< 10'b 0000000_001 /* SLLI */: begin next_wr = 1; next_rd = rs1_value << insn[24:20]; end
< 10'b 0000000_101 /* SRLI */: begin next_wr = 1; next_rd = rs1_value >> insn[24:20]; end
< 10'b 0100000_101 /* SRAI */: begin next_wr = 1; next_rd = $signed(rs1_value) >>> insn[24:20]; end
---
> 10'b 0000000_001 /* SLLI */: begin next_wr = 1; next_rd = shift_out; end
> 10'b 0000000_101 /* SRLI */: begin next_wr = 1; next_rd = shift_out; end
> 10'b 0100000_101 /* SRAI */: begin next_wr = 1; next_rd = shift_out; end
328c340
< 10'b 0000000_001 /* SLL */: begin next_wr = 1; next_rd = rs1_value << rs2_value[4:0]; end
---
> 10'b 0000000_001 /* SLL */: begin next_wr = 1; next_rd = shift_out; end
332,333c344,345
< 10'b 0000000_101 /* SRL */: begin next_wr = 1; next_rd = rs1_value >> rs2_value[4:0]; end
< 10'b 0100000_101 /* SRA */: begin next_wr = 1; next_rd = $signed(rs1_value) >>> rs2_value[4:0]; end
---
> 10'b 0000000_101 /* SRL */: begin next_wr = 1; next_rd = shift_out; end
> 10'b 0100000_101 /* SRA */: begin next_wr = 1; next_rd = shift_out; endThe new shifter performs right shifts directly, and left shifts by reversing the bits of its input and of its result (bitreverse). Every shift instruction now takes its result from shift_out.
With SHIFTER_BUG defined, the register form of a shift takes its shift amount from rs2_value[5:0], six bits, instead of rs2_value[4:0]. The RISC-V specification states that SLL, SRL and SRA shift “by the shift amount held in the lower 5 bits of register rs2”. When bit 5 of rs2_value is 1, the buggy shifter therefore shifts 32 places further than the specification allows.
Read the .eqy file
$ cat nerv_change_fail.eqy
output
[gold]
read_verilog -sv nerv.sv
prep -top nerv
memory_map
[gate]
read_verilog -sv -DSHIFTER_BUG nerv_change.sv
prep -top nerv
memory_map
[collect *]
group regfile*
join imm_*
join insn*
[strategy sby]
use sby
depth 2
engine smtbmc bitwuzla
The table explains each section of the file.
| Section | What it does |
|---|
[gold] | The Yosys script that reads the gold design. prep -top nerv prepares it for the check with nerv as the top module, and memory_map turns the register file into flip-flops. |
[gate] | The same script for nerv_change.sv. -DSHIFTER_BUG defines the macro that injects the bug. |
[collect *] | Groups bits that must be proved together. group regfile* puts every register-file bit into one group; each join line keeps all bits of each matching multi-bit net together. |
[strategy sby] | Proves each partition with SymbiYosys, at depth 2, with the engine smtbmc bitwuzla. EQY copies the engine line into each generated job file. |
Run the check and find the bug
$ eqy -f nerv_change_fail.eqy
output (last lines)
EQY 3:27:36 [nerv_change_fail] Warning: Failed to prove equivalence for 1/44 partitions:
EQY 3:27:36 [nerv_change_fail] Failed to prove equivalence of partition nerv.next_rd
EQY 3:27:36 [nerv_change_fail] summary: Elapsed clock time [H:MM:SS (secs)]: 0:00:22 (22)
EQY 3:27:36 [nerv_change_fail] summary: Elapsed process time [H:MM:SS (secs)]: 0:00:27 (27)
EQY 3:27:36 [nerv_change_fail] DONE (FAIL, rc=2)
As with sby, -f removes the work folder of an earlier run first. EQY proved 43 of the 44 partitions. The one it could not prove, nerv.next_rd, computes next_rd: the value an instruction writes to its destination register. The verdict is FAIL, and EQY exits with return code 2.
Read the failing partition's counterexample
EQY writes a SymbiYosys job for each partition, in nerv_change_fail/strategies/<partition>/sby/. This is the job of the failing partition:
$ cat nerv_change_fail/strategies/nerv.next_rd/sby/nerv.next_rd.sby
output
[options]
mode prove
depth 2
expect pass,fail,unknown,timeout
[engines]
smtbmc bitwuzla
[script]
verilog_defaults -add -D CHECK_OUTPUTS
read_verilog -sv ../../../../../partitions/nerv.next_rd.sv
read_rtlil ../../../../../partitions/nerv.next_rd.il
hierarchy -top miter; proc
async2sync
formalff -clk2ff -ff2anyinit gate.nerv.next_rd
setundef -anyseq gate.nerv.next_rd
flatten -wb; dffunmap; opt_expr -keepdc -undriven; opt_clean
xprop -formal -split-ports -assume-def-inputs miter
It is a prove task at depth 2, with the engine from the .eqy file. Its script reads the partition's miter, a module named miter. The expect line accepts every verdict, so the job itself ends with rc=0; EQY reads the verdict and reports the failure. The job's summary shows where the proof failed:
$ grep -E 'summary|DONE' nerv_change_fail/strategies/nerv.next_rd/sby/nerv.next_rd/logfile.txt
output
SBY 3:27:28 [nerv.next_rd] summary: Elapsed clock time [H:MM:SS (secs)]: 0:00:00 (0)
SBY 3:27:28 [nerv.next_rd] summary: Elapsed process time [H:MM:SS (secs)]: 0:00:00 (0)
SBY 3:27:28 [nerv.next_rd] summary: engine_0 (smtbmc bitwuzla) returned FAIL for basecase
SBY 3:27:28 [nerv.next_rd] summary: counterexample trace [basecase]: nerv.next_rd/engine_0/trace.vcd
SBY 3:27:28 [nerv.next_rd] summary: failed assertion miter._witness_.assert_flatten___po_next_rd__assert_________________partitions_nerv_next_rd_sv_86_assert_2976 at ../../../../../partitions/nerv.next_rd.sv:86.37-86.49
SBY 3:27:28 [nerv.next_rd] DONE (FAIL, rc=0)
The base case fails: the miter's assertion that the gold and gate outputs are equal fails at step 0. yosys-witness prints the input values of the trace, from the witness file trace.yw next to trace.vcd:
$ yosys-witness display nerv_change_fail/strategies/nerv.next_rd/sby/nerv.next_rd/engine_0/trace.yw
output
Reading Yosys witness trace 'nerv_change_fail/strategies/nerv.next_rd/sby/nerv.next_rd/engine_0/trace.yw'...
*** RTLIL bit-order below may differ from source level declarations ***
=== Initial State ===
#0 __pi_insn_funct3[2:0] = 101
#0 __pi_insn_funct7[6:0] = 0000000
#0 __pi_insn_opcode[6:0] = 0110011
#0 __pi_insn_rs1[4:0] = 11111
#0 __pi_insn_rs2[4:0] = 11111
#0 __pi_pc[31:0] = 11111111111111111111111111111111
#0 __pi_rs1_value[31:0] = 11111111111111111111111111111111
#0 __pi_rs2_value[31:0] = 11111111111111111111111111111111
EQY names the inputs of a partition with the prefix __pi_ and its outputs with __po_. Read the values as an instruction, with the case statement of nerv.sv:
insn_opcode 0110011 is OPCODE_OP, the register-register instructions. insn_funct7 0000000 with insn_funct3 101 selects SRL, a logical right shift.rs1_value and rs2_value are both 0xFFFFFFFF. The lower five bits of rs2_value are 31, and bit 5 is 1.- The gold design shifts
0xFFFFFFFF right by 31 places. The result is 0x00000001. - The gate design uses six bits and shifts by 63 places. The result is
0x00000000.
trace.vcd in the same folder shows the two results as __po_next_rd__gold (1) and __po_next_rd__gate (0). The example's README shows a different counterexample, an SLL instruction found by an earlier release; both show the same bug.
Remove the bug and prove equivalence
The pass job differs from the fail job in one line: it reads nerv_change.sv without SHIFTER_BUG.
$ diff nerv_change_fail.eqy nerv_change_pass.eqy
output
7c7
< read_verilog -sv -DSHIFTER_BUG nerv_change.sv
---
> read_verilog -sv nerv_change.sv
$ eqy -f nerv_change_pass.eqy
output (last lines)
EQY 3:27:57 [nerv_change_pass] Successfully proved designs equivalent
EQY 3:27:57 [nerv_change_pass] summary: Elapsed clock time [H:MM:SS (secs)]: 0:00:21 (21)
EQY 3:27:57 [nerv_change_pass] summary: Elapsed process time [H:MM:SS (secs)]: 0:00:29 (29)
EQY 3:27:57 [nerv_change_pass] DONE (PASS, rc=0)
Every partition is proved, so the refactored core behaves like the original. The proof needs no assertion about shifts: the original design serves as the specification.
Check a synthesized netlist against its source
The third job checks nerv_synth.v, a netlist that Yosys's synth command wrote from nerv.sv. A netlist describes the design as individual logic gates and flip-flops instead of behavioural code: in nerv_synth.v, each gate is an assign statement such as assign _00038_ = ~(imem_data[1] & imem_data[0]);. The script and the netlist's first line show how it was made, and with which Yosys release:
$ cat nerv_synth.ys
$ head -1 nerv_synth.v
output
read_verilog -sv nerv.sv
synth -top nerv
write_verilog nerv_synth.v
/* Generated by Yosys 0.21 (git sha1 e6d2a900a, clang 10.0.0-4ubuntu1 -fPIC -Os) */
$ cat nerv_synth.eqy
output
[gold]
read_verilog -formal nerv.sv
hierarchy -check -top nerv
proc
memory -nomap
prep -top nerv
memory_map
# only keep FF outputs, avoids partitioning on signals that were changed by optimizations
rename -hide t:$dff %co x:* %% w:* %D
[gate]
read_verilog -formal -icells nerv_synth.v
prep -top nerv
[collect *]
# grouping all of the register file makes things a lot faster
group regfile*
# would be among the unused signals of the regfile partition which fails without this
bind dmem_wdata
[strategy sby]
use sby
depth 2
engine smtbmc bitwuzla
The two comments in the file give the reasons for its changes from the refactor check: the rename -hide line keeps only flip-flop outputs as named signals, because optimization changes the others, and bind dmem_wdata is needed for the register-file partition to be proved. Run the check:
$ eqy -f nerv_synth.eqy
output (last lines)
EQY 3:29:10 [nerv_synth] Successfully proved designs equivalent
EQY 3:29:10 [nerv_synth] summary: Elapsed clock time [H:MM:SS (secs)]: 0:01:12 (72)
EQY 3:29:10 [nerv_synth] summary: Elapsed process time [H:MM:SS (secs)]: 0:01:29 (89)
EQY 3:29:10 [nerv_synth] DONE (PASS, rc=0)
The netlist is equivalent to its source. Had synthesis changed the design's behaviour, a partition would fail, and its trace would show inputs on which the source and the netlist differ.