Engineering Change Orders (ECOs) are often introduced late in the design cycle to address functional, timing, power or implementation issues.
Even a small RTL modification can affect behaviour that was previously verified.
Two important verification activities in this process are Logic Equivalence Checking (LEC) and Formal Property Verification (FPV).
They address different verification questions.
What does LEC check?
LEC checks whether two design representations are logically equivalent under the configured comparison setup.
For example, after a functional ECO is implemented in the netlist, an equivalence flow can compare the patched netlist against the updated RTL. For a change intended to preserve function, such as a timing or implementation ECO, it can compare the revised design against the approved reference.
The comparison depends on the selected reference and revised designs, matching strategy, constraints, configuration and tool setup.
LEC helps establish whether the change preserves the intended equivalence relationship.
What does FPV check?
Formal Property Verification checks whether a design satisfies specified functional properties under the configured assumptions.
These properties may describe:
- Protocol behaviour
- Control sequencing
- State-machine transitions
- Reset behaviour
- Arbitration requirements
- Data integrity conditions
- Safety and progress requirements
FPV checks the specified requirements. It does not automatically establish that every possible functional requirement has been captured.
Why one does not replace the other
Consider an ECO that changes arbitration logic.
LEC can establish that the patched netlist is equivalent to the updated RTL under the configured comparison conditions. It cannot establish whether the updated RTL is itself correct.
If the intended requirement is that a requester must not be starved under specified fairness conditions, that requirement needs a formal property checked on the updated design.
Conversely, a revised design may satisfy selected FPV properties while still differing from its intended implementation in a way those properties do not cover. Equivalence checking catches that class of difference.
The two checks provide complementary evidence.
A practical ECO verification sequence
A disciplined ECO flow can include:
- Identify the exact RTL change and its purpose.
- Run the required simulation regression.
- Run LEC between the appropriate design representations, such as the patched netlist against the updated RTL.
- Re-run affected formal properties.
- Review assumptions and configuration changes.
- Run STA and other affected implementation checks.
- Document results against the correct RTL revision.
The exact sequence may vary depending on the ECO type and project methodology.
Maintain traceability
For each ECO, record:
- Reference and revised RTL revisions
- ECO description
- LEC configuration and result
- Relevant FPV properties and results
- Simulation regression status
- STA and implementation status
- Open issues and review comments
Conclusion
LEC and FPV answer different questions.
LEC checks equivalence between design representations under a configured comparison setup. FPV checks specified functional requirements under a formal model.
Using both where appropriate provides stronger verification evidence for late-stage RTL changes.
