Equivalence questions test what proof means. Simulation samples vectors while equivalence reasons over all inputs.
Question | Precise answer | Follow-up probe | Common wrong answer |
|---|---|---|---|
What does formal equivalence check between RTL and netlist? | That both produce identical outputs for identical inputs from identical states, without simulating vectors. | What breaks the proof first after an ECO? | Passing simulation proves equivalence. |
What is the first step when equivalence fails on one output? | Localize the failing cone and compare boundary values, then check for a constraint or an unreachable state explaining it. | When do you blame the tool? | Re-run synthesis with more effort. |
ECO questions test whether a late change earns its risk. Small cones with fresh proofs pass, and anything else waits.
Question | Precise answer | Follow-up probe | Common wrong answer |
|---|---|---|---|
When is a functional ECO safe to accept? | When the change is local, re-verified by equivalence against the new RTL, and re-timed; risk grows with cone size. | What must be rechecked after any ECO? | A small ECO needs no re-verification. |
What separates a netlist tweak from an RTL change with re-synthesis? | A tweak edits mapped cells directly and stays local; an RTL change re-runs the flow and can move unrelated logic. | Which one risks wider timing movement? | Both carry the same risk. |
Close any verification answer with the handoff list. Each item below is a check, not a claim.
Equivalence of the final netlist against the final RTL is clean.
Constraints cover every clock, with each exception recorded and reviewed.
Quoted areas and slacks trace to runnable steps with stated EXAMPLE parameters.
The ECO log names each change, its cone, and its fresh proof.
Equivalence against the updated RTL and timing on the touched paths.
Some untested input exposes a real difference or a bad constraint; localize the cone and compare boundary values.