Static Timing Analysis (STA) uses timing constraints to evaluate whether a design meets its timing requirements.
SDC constraints can define clocks, input and output delays, false paths, multicycle paths and other timing relationships.
These constraints have a direct impact on which paths are analysed and how timing requirements are evaluated.
A timing exception may be correct, but its functional justification should be understood.
What is a timing exception?
A false-path constraint tells STA not to analyse a selected path for timing.
A multicycle-path constraint changes the timing relationship used for a selected path.
Such exceptions are necessary in certain designs. For example, a path may be functionally inactive under a particular operating mode, or a destination may capture data only after multiple clock cycles.
However, an incorrect exception can cause an important timing path to be excluded or analysed with an inappropriate requirement.
Where can formal verification help?
Formal verification can check selected functional assumptions that justify a timing exception.
For example, suppose a path is expected to be inactive in a particular operating mode.
A formal property can check whether the relevant control condition prevents the path's functional activation under the specified circumstances.
Similarly, for a multicycle relationship, formal properties may check selected protocol or control requirements, such as:
- When data is launched
- When data is expected to be captured
- Whether the required control mode is active
- Whether relevant data remains stable
- Whether reset and mode transitions are handled correctly
The properties must be derived from the actual design specification and timing intent.
An important distinction
Formal verification does not validate an entire SDC file automatically.
It does not replace STA, and a passing formal property does not prove that a timing exception has been applied to the correct endpoints.
For example, STA must still evaluate:
- Clock definitions
- Clock relationships
- Startpoint and endpoint selection
- Exception scope
- Setup and hold requirements
- Timing reports and path coverage
A common same-clock multicycle example uses a setup relationship of two cycles and a corresponding hold relationship of one cycle. This is not a universal rule; the correct values depend on the timing intent, clock relationship and constraint methodology.
A combined review approach
A useful review process can include:
- Identify the timing exception and its affected paths.
- Understand the functional reason for the exception.
- Identify the relevant RTL control signals and operating modes.
- Define formal properties for the selected functional conditions.
- Review the assumptions and reachable scenarios.
- Review the SDC exception scope and timing reports in STA.
- Record the relationship between the functional evidence and timing analysis.
Conclusion
Formal verification and STA address different aspects of design correctness.
Formal verification can provide evidence that selected functional conditions behind timing exceptions are satisfied. STA evaluates the timing consequences of the constraints.
Using both forms of analysis can improve confidence in timing intent, provided their responsibilities and limitations remain clear.
