Why must you run logic equivalence checking after every ECO?

Short Answer

Every ECO edits the netlist, and any edit can change function by mistake: a wrong library cell, a buffer on the wrong pin, a dropped inverter or a patch that does not match the new RTL. Timing and physical checks do not look at logic, so only equivalence checking proves the post-ECO netlist still computes what it should. It is quick for small ECOs and it is the only check that catches these bugs before silicon.

Technical Explanation

• Timing ECOs should not change function, but tools and people can still break it. size_cell (PT) and size_cell (ICC2) only accept functionally equivalent cells, but a scripted change_link (ICC2) only checks that pin names and directions match, so it can swap in a cell with a different function. That, an inverter pair split across the wrong net, or a hand edit to a pin name all pass timing and fail silicon.
• Functional ECOs deliberately change function, so the check proves the change matches the new RTL, not just that the netlist changed.
• The reference and implementation differ by ECO type. For a timing ECO the reference is the netlist before the ECO; for a functional ECO it is the new RTL.
• Formality reads the reference with read_verilog -r (FM) and the implementation with read_verilog -i (FM), sets each top with set_top (FM), pairs compare points with match (FM) and proves them with verify (FM).
• Results are PASS when all compare points are equivalent, FAIL when some are not, and INCONCLUSIVE when some were not verified or were aborted. Only PASS counts.
• report_failing_points (FM) lists the compare points that failed, which usually lead straight to the edited cone. Unmatched points also need a look, because a register renamed by the ECO can hide a real change.
• The implementation netlist should be written from ICC2 after the ECO, so the check covers exactly what goes to tapeout, including any hand edits made after the PT change list.

What To Check

• The ECO type, and therefore the correct reference design.
• Unmatched compare points after match (FM), before running verification.
• The final status: PASS, FAIL or INCONCLUSIVE.
• Failing points from report_failing_points (FM), traced back to the ECO edits.

Healthy, Suspicious & Hard-stop Results

• Healthy (illustrative): PASS with every compare point matched and equivalent, run on the netlist written after the last ICC2 edit.
• Suspicious (illustrative): INCONCLUSIVE on a few aborted points in a datapath the ECO touched; rerun with more effort or split the check before signing off.
• Hard stop: Any FAIL on a timing ECO, or a functional ECO verified against the old RTL. Do not tape out.

What The Interviewer Is Testing

• Choosing the correct reference for timing and functional ECOs.
• Can you walk through the Formality steps from reading designs to reporting failures?
• Treating INCONCLUSIVE as not yet passed.

Follow-up Question & Model Response

"If a timing ECO only resizes cells, can equivalence really fail?"

Candidate Model Response: Yes. size_cell (PT) and size_cell (ICC2) themselves only accept functionally equivalent cells, but resizes are often scripted or hand-edited in ICC2 with change_link (ICC2), which only checks that pin names and directions match. A cell with a similar name and the same pins but a different function can slip through that way. Buffer insertion can also go wrong if the buffer is placed on the wrong pin or an inverter pair loses one half. The check takes minutes for a small ECO, while the bug it catches costs a respin.