Formal Equivalence Verification
Prove two models behave identically: combinational vs sequential equivalence, key-point mapping, RTL-to-netlist and RTL-to-RTL flows, constraints, don't-cares and mismatch debug.
What you will learn
- Distinguish combinational, sequential and transaction-level equivalence.
- Explain key points, mapping and why state matching makes FEV scale.
- Set up an RTL-to-RTL equivalence check for a refactored or retimed design.
- Debug a mismatch and recognise setup problems: constraints, black boxes, don't-cares.
Lessons
- 8.1What does "equivalent" mean?Combinational, sequential and transaction-level equivalence.
- 8.2Key points and mappingWhy matching flops turns a sequential problem into many small combinational ones.
- 8.3RTL-to-netlist and netlist-to-netlistThe everyday use of FEV in the implementation flow.
- 8.4RTL-to-RTL equivalenceVerify refactoring and retiming without writing a single test.
- 8.5Running FEV and debugging mismatchesA practical checklist from setup to sign-off.
- ✎Chapter quiz (4 questions)