When Equivalence Fails

A failed equivalence check gives you one input vector and two different outputs. In a netlist with millions of gates, that is only the beginning: the difference has to be traced back to the gate, wire or register that causes it. This article shows a practical method: find which outputs differ and which agree, narrow the search to the logic only the failing outputs share, and evaluate that logic on the counterexample. It also lists the usual causes of false non-equivalence, which are as common as real bugs.

8 min read | Intermediate

What You'll Learn

• Use the list of proven and unproven outputs to localize a difference
• Narrow the search to the logic the failing outputs share
• Evaluate the suspect logic on the counterexample to find the wrong gate
• Recognize false non-equivalence from setup problems

Step 1: Which Outputs Differ?

The Yosys equiv flow checks every output pair separately and reports which ones it could not prove. For the hand-edited adder netlist from the combinational equivalence article:

  Of those cells 2 are proven and 3 are unproven.
  Unproven $equiv $auto$equiv_make.cc:258:find_same_wires$27: \s_gold [3] \s_gate [3]
  Unproven $equiv $auto$equiv_make.cc:258:find_same_wires$26: \s_gold [2] \s_gate [2]
  Unproven $equiv $auto$equiv_make.cc:258:find_same_wires$23: \cout_gold \cout_gate

Sum bits 0 and 1 are proven equivalent; sum bits 2 and 3 and the carry out are not. Commercial tools give the same kind of list, usually per compare point, which for a real netlist includes every register input as well as every output.

Step 2: Narrow the Cone

The bug must be in logic that feeds every failing output, and it is unlikely to be in logic that feeds only passing ones. For the adder, the failing outputs share the carry chain into bit 2, while bits 0 and 1 do not depend on it. That leaves a handful of gates: the carry logic of bits 1 and 2.

In a large design, this step turns a million gates into a few dozen. Tools help with schematic views of the cone and with "first difference" analysis on internal compare points.

Step 3: Evaluate on the Counterexample

The counterexample was a = 8, b = 6, cin = 0. Evaluate the suspect gates by hand or in a simulator:

The first signal whose value differs from what the function requires is _08_, and its gate is an OR where an AND belongs. That is the edit.

False Non-Equivalence

Not every failure is a design bug. Common setup causes:

• Test logic not disabled: scan multiplexers inserted into the netlist are not in the RTL. The scan-enable input must be tied off in the netlist check, or every register looks different.
• Unmatched or merged registers: synthesis merged two equal registers, or renamed them, and the tool paired them wrongly.
• Don't-care values: the RTL leaves some outputs unspecified (X), and synthesis chose a value. Options like -ignore_gold_x in Yosys treat X in the gold design as "anything allowed".
• Different reset or initial values: registers reset to different values in the two versions.
• Constant inputs: a mode pin that is constant in the chip is free in the check, exposing logic that never matters.

Running It in ChipVerify Lab

The example contains the adder RTL, a netlist with a different wrong gate, and the miter from the combinational equivalence article. The lab trace shows the inputs and both sums. Use the method of this article to find the gate.

Common Mistakes