Equivalence Interview Questions

Combinational equivalence pairs the flops of the two designs and compares the logic cone in front of each pair, with no unrolling. It suits RTL against a synthesised netlist, because synthesis mostly keeps the flops. Sequential equivalence lets the state differ and asks for equal outputs over time from reset. You need it after retiming, pipelining, state recoding or clock-gating changes.

Matching flops cuts both designs into small cones between key points, so each comparison is combinational and needs no unrolling. If two flops are paired wrongly, their cones compute different functions. The tool then reports a mismatch that is a mapping error, not a design bug. Debug starts at the smallest failing cone and the key points that feed it.

Then combinational LEC cannot pair those flops, because they now hold different functions. Their cones fail or stay unmapped. The retimed region needs sequential equivalence, which compares outputs over time from reset. That region then gets its own line in the sign-off.

Expect it. Equivalence of unlike multipliers grows exponentially with width on every solver. BDDs for the middle product bit are exponential for every variable order. Change the question instead of the machine. Compare at register boundaries, or split the proof into partial products and the adder tree, each of which is easy to check.

Probably not. Treating key points as free inputs throws away the relations between them. So the tool can pick combinations the real design never produces. A real difference has a consistent counterexample that is reachable from the inputs. Check that before calling it a bug. Otherwise, fix the mapping or add a constraint.

Build a miter of the old and new RTL and check conditional equivalence. Outputs must match whenever the bug's condition is false. Inside that condition, the new design must meet the spec. Write the condition from the bug report, never from the diff, or a wrong fix defines its own condition. A counterexample on inputs the spec forbids means a missing assumption, not a bad fix.

Both say where the check applies. A condition that is too wide hides real differences, exactly as an over-constraining assumption hides bugs. So it needs the same discipline. It needs a written source in the bug report or the spec. It also needs a review by someone who did not write the fix.

Inside the excluded region the old and new designs may differ freely, and the check says nothing. So a second, accidental change to another opcode in that group passes. Write the condition from the bug report, so it covers only the failing case. Then check the new design inside it against the spec.

The regression samples the input space at the points its tests reach, and it takes hours or days. The miter covers every input in the region where the old and new designs must agree. For a block-level fix, it usually takes minutes. The regression still matters for what the miter does not state. That is the behaviour inside the bug condition and the system around the block.

AXI allows WRAP bursts of only 2, 4, 8 or 16 transfers, so length 3 cannot occur; add that rule as an assumption, citing the spec. Add only what a counterexample demands: in the lesson the alignment assumption turned out unnecessary, because the check passes without it.

Every late RTL change carries a miter against the last signed-off RTL. Its condition comes from its bug report, and a second engineer reviews it. The block's formal regression and RTL-to-netlist LEC rerun on the new netlist. The ECO is closed only when all three are clean and the condition is attached to the change record.