Running FEV and debugging mismatches
Setup checklist
- Models: exactly the right RTL files, defines and parameters for the reference; the right netlist and cell libraries for the implementation.
- Black boxes: same modules black-boxed on both sides, with matching pin names.
- Constraints: test/scan pins, mode pins — each one justified.
- Mapping: review unmapped key points before trusting any "equivalent" verdict.
When the tool reports a non-equivalent point
| Step | Question |
|---|---|
| 1 | Is the failing compare point correctly mapped? A wrong mapping produces nonsense mismatches. |
| 2 | Does the counterexample use input values that are impossible in reality (e.g. scan enabled)? → missing constraint. |
| 3 | Does the difference involve X / don't-care values from the RTL? → check don't-care handling (below). |
| 4 | Is the logic cone of the point really different? → genuine bug (synthesis, ECO or RTL change). |
Don't-care space
RTL can explicitly say "I don't care": assigning 'x in a default branch, or a case that does not cover
all values. Synthesis is free to implement any value there. FEV therefore checks refinement: the implementation may
choose any value where the reference says X. If you compare two RTL versions where the reference is the more
specific one, the same difference shows up as a mismatch. Decide which model is the reference with this in mind.
Conditional equivalence
Sometimes two designs only need to agree under a condition — for example, a data output only matters when its valid is high. Express that as a qualified compare:
a_data_eq_when_valid: assert property (@(posedge clk) disable iff (rst)
valid_ref |-> data_ref == data_imp);
a_valid_eq: assert property (@(posedge clk) disable iff (rst)
valid_ref == valid_imp);Always keep the qualifier itself in an unconditional compare, otherwise a design that never raises valid would be "equivalent".