Two adders leave two different tools and land in the same netlist. The synthesis report says they match, but the report is a claim, not a proof. This topic builds the proof: the miter that turns equivalence into one safety property, the solver technique that scales it, the constrained form that weakens it honestly, and the reading discipline for the day the comparator fires.
Lesson | After it you can... |
|---|---|
Build a miter from two blocks, prove it, and read the mismatch trace. | |
Explain how shared structure and candidate signatures make a big miter solvable. | |
State a constrained result exactly and prove every mode. | |
Tell a real mismatch from a setup difference and minimise the trace. |
Suggested order: top to bottom. Build the miter, learn why it scales, learn the weaker constrained form, then practise reading failures. The synthesis-side flow this complements lives at Combinational Equivalence.
Two copies are two independent choices to the solver: it could drive them differently and report a mismatch no real stimulus can produce. Shared wires force one stimulus into both cones, so every counterexample is replayable.