Combinational Equivalence

Synthesis turns RTL into a netlist of gates. Optimizations, technology mapping, test insertion and hand-made fixes all change that netlist. An equivalence check proves that the netlist still computes exactly what the RTL computes, for every input. This article explains how, using a 4-bit adder, its gate netlist from Yosys, and a hand-edited netlist with one wrong gate.

9 min read | Intermediate

What You'll Learn

• Explain what combinational equivalence checking proves and when it applies
• Build a miter that compares two designs with one formal question
• Run an equivalence check with Yosys, and as a property check in the lab
• Read the counterexample of a failed equivalence check

The Miter

An equivalence check connects the two designs, called gold (the reference) and gate (the implementation), to the same inputs and compares every output. The combined circuit is called a miter. Its single output, often called trigger, is 1 whenever any output pair differs. The formal question is: can trigger ever be 1?

If the answer is no, the designs are equivalent for every input. If yes, the solver returns the input that makes them differ.

Combinational Equivalence

When both designs have the same registers, as RTL and its synthesized netlist usually do, the check can compare the logic between registers only. Each register output becomes an input of the miter and each register input becomes an output. The question is then purely combinational: one frame, no unrolling. This is why equivalence checking scales to whole chips with millions of gates: each cone between registers is checked separately, and most are small.

Registers are matched by name or by structure. When synthesis renames or merges registers, the tool has to find the pairs first, and when it moves registers across logic (retiming), the check becomes sequential, as the sequential equivalence article shows.

The Example: an Adder and Its Netlist

module add4 (input [3:0] a, input [3:0] b, input cin, output [3:0] s, output cout);
  assign {cout, s} = a + b + cin;
endmodule

Yosys synthesizes it into 20 gates, written out as a netlist module add4_gate. A part of it:

assign _06_ = _03_ | _05_;          // carry into bit 1
assign _07_ = a[1] ^ b[1];          // propagate of bit 1
assign _08_ = _06_ & _07_;          // carry passes through bit 1
assign _09_ = _02_ | _08_;          // carry into bit 2
...
assign s[1] = _06_ ^ _07_;

The check with Yosys builds the miter and asks the SAT solver to prove that trigger is always 0:

read_verilog rtl.v
read_verilog gate.v
proc
miter -equiv -flatten -make_outputs -ignore_gold_x add4 add4_gate miter
hierarchy -top miter
sat -verify -prove trigger 0 -show-inputs -show-outputs miter

Solving problem with 326 variables and 853 clauses..
SAT proof finished - no model found: SUCCESS!

"No model found" means the solver found no input that makes the outputs differ. The netlist is equivalent. Yosys also has a dedicated flow, equiv_make, equiv_simple and equiv_status, which matches internal signals as well and reports "Equivalence successfully proven!" for this netlist.

A Hand Edit Goes Wrong

Late in a project, small netlist fixes are made by hand, called engineering change orders (ECO). Suppose an engineer edits one gate and types an OR instead of an AND:

assign _08_ = _06_ | _07_;          // was: _06_ & _07_

The same check now fails:

SAT proof finished - model found: FAIL!

  Signal Name             Dec       Hex           Bin
  --------------- ----------- --------- -------------
  \gate_cout                1         1             1
  \gate_s                   2         2          0010
  \gold_cout                0         0             0
  \gold_s                  14         e          1110
  \in_a                     8         8          1000
  \in_b                     6         6          0110
  \in_cin                   0         0             0
  \trigger                  1         1             1

For a = 8, b = 6 and no carry in, the RTL gives 14 and the netlist gives 2 with a carry out. The when equivalence fails article shows how to trace such a difference back to the wrong gate.

Running It in ChipVerify Lab

The lab panel runs property checks, so an equivalence check becomes a property: a wrapper instantiates both versions, connects their inputs, and asserts that the outputs match. That wrapper is exactly a miter:

module add4_miter (input [3:0] a, input [3:0] b, input cin);
  // the same inputs drive both versions
  wire [3:0] s_rtl, s_gate;
  wire       c_rtl, c_gate;
  add4      u_rtl  (.a(a), .b(b), .cin(cin), .s(s_rtl),  .cout(c_rtl));
  add4_gate u_gate (.a(a), .b(b), .cin(cin), .s(s_gate), .cout(c_gate));
`ifdef FORMAL
  // the outputs must always be equal
  always @(*) assert (s_rtl == s_gate && c_rtl == c_gate);
`endif
endmodule

The example contains the RTL, the edited netlist and the miter. Run it with the top module add4_miter: it fails in step 0, with inputs that make the two adders disagree. Correct the gate and it passes.

Common Mistakes