Key points and mapping
Comparing two large sequential designs directly is hard. Combinational FEV avoids it with a simple observation: if both designs have the same state elements, and every state element and output is driven by equivalent logic, then the designs are equivalent — by induction over the cycles.
The tool therefore:
- Identifies key points in both models: primary inputs and outputs, flops, latches, black-box pins.
- Maps key points of the reference model to those of the implementation — by name, by structure, or by functional analysis (names change during synthesis).
- For each mapped compare point (outputs, flop inputs), checks that its combinational logic cone is equivalent, treating mapped key points as shared inputs.
Typical mapping problems
| Symptom | Usual cause |
|---|---|
| Unmapped flops in implementation | Flops added by synthesis/DFT (scan, clock gating, retiming), or renamed beyond recognition |
| Unmapped flops in reference | Flops optimised away (constant, duplicate, unused) — usually fine, but check |
| Inverted mapping | Synthesis stored the inverse of a signal (phase inversion); tools usually detect it |
| One-to-many mapping | Register duplication for timing — several implementation flops map to one reference flop |