Two teams implement the same block, or one tool rewrites it overnight. Simulation can compare them on a million vectors and still miss the one input corner where they disagree. Equivalence checking proves they agree on every input, every cycle, or hands over the exact input sequence where they differ. The statement it proves is narrow: the two implementations match each other. It never proves either one is correct, which is why this section ends with the pair every signoff needs: equivalence plus a property proof on the reference.
Topic | What it covers | After it you can... |
|---|---|---|
The miter, solver-aided comparison, constrained equivalence, reading a mismatch | Build a miter, state what a pass means, and diagnose a failing comparison. | |
Product machines, retimed twins, latency alignment, recoding and gating | Prove equivalence across retiming and recoding, and align latencies without fooling yourself. | |
One-to-one state correspondence, key points, unmapped state, limits of the method | List the assumptions behind a gate-level pass and triage a mismatch to setup or reality. | |
ECO flow, two arbiter implementations, why agreement is not correctness | Prove an ECO changed only what was intended and nothing else. |
Suggested order: top to bottom. The miter first, because every later topic reuses it. Sequential equivalence next, because retiming is where the one-to-one picture breaks. The assumptions topic then says exactly when the simple method applies, and the ECO topic puts the whole kit to work on a change you would actually sign off. Readers chasing one failure can start at its topic and follow the links back. For the synthesis-side flow of cones, key points and black boxes, see Equivalence Checking.
First, equivalence proves the netlist matches the RTL, not that the RTL is right: a bug present in both passes. Second, an assumption may be wrong: scan left enabled, a constant tied differently on the board, or a mode never compared.