Formal verification and Static Timing Analysis are different verification activities.
Formal verification explores logical behaviour under a defined model. STA evaluates timing paths against clocks and timing constraints.
Although their objectives differ, both depend on an accurate understanding of the design configuration.
Differences in assumptions, clocks, reset conditions or operating modes can create gaps between their results.
Why configuration consistency matters
Consider a design with multiple operating modes.
A particular clock or functional path may be active only in one mode. Formal verification may analyse the design under one mode configuration, while STA may evaluate a different timing scenario.
If the two configurations do not represent the same intended operating conditions, their results may not be directly comparable.
Similar issues can arise with:
- Clock definitions and relationships
- Reset behaviour
- Clock-gating conditions
- Operating modes
- CDC and RDC assumptions
- Timing exceptions
- Parameter and define settings
Formal and STA constraints are not interchangeable
Formal verification uses assumptions and constraints to define legal behaviour and reduce the state space.
STA uses timing constraints such as clocks, input/output delays and timing exceptions to evaluate timing requirements.
These are different models.
A formal assumption cannot directly replace an SDC constraint, and an SDC constraint does not automatically establish a functional property.
The objective is to keep the underlying design intent consistent where the two analyses overlap.
A practical alignment process
A joint review can include:
- Confirm the RTL revision and design configuration.
- Review clocks, resets and operating modes.
- Identify the timing exceptions relevant to functional behaviour.
- Identify formal assumptions related to the same conditions.
- Check whether the assumptions are justified by the specification.
- Review the relevant SDC paths and timing reports.
- Record any differences between the formal and STA configurations.
Not every timing exception requires a formal property. Formal checks should be selected where they provide meaningful evidence for the functional conditions behind the exception.
Why traceability matters
A useful sign-off record should identify:
- The design revision
- The operating mode
- The relevant formal properties and assumptions
- The SDC revision
- The applicable timing scenarios
- The results and unresolved limitations
This makes it easier to understand whether the formal and timing analyses were performed against consistent design intent.
Conclusion
Formal verification and STA should remain separate technical disciplines, but their assumptions and configurations should be reviewed together where relevant.
A consistent understanding of clocks, resets, modes and timing intent helps reduce gaps between functional verification and timing sign-off.
