A formal verification run completes, the results appear green, and the property list shows several passing or proven properties.
It is tempting to treat this as sign-off. However, a successful tool run does not automatically mean that the design is fully verified.
Before accepting a formal verification result, engineers should examine the following five areas.
1. Check whether the properties represent the intended behaviour
A property can pass while checking the wrong behaviour.
For example:
property p_req_grant_busy; @(posedge clk) (req && gnt) |-> ##1 busy; endproperty assert property (p_req_grant_busy);
This property checks that busy is asserted one clock cycle after req and gnt are simultaneously high.
But is that the intended protocol behaviour?
The expected relationship between request, grant and busy must come from the design specification. The property must also account for the design's reset and clocking behaviour.
A passing result is meaningful only when the property correctly represents the requirement.
2. Review the assumptions
Formal verification explores behaviours permitted by the constraints.
An assumption that is too restrictive can prevent the tool from exploring important scenarios.
For example, an assumption that unnecessarily prevents requests during certain conditions may hide a design defect.
Every assumption should have a clear justification based on the environment contract or verification boundary.
3. Check for vacuous proofs
An assertion may pass because its triggering condition never occurs.
Consider:
assert property (@(posedge clk) (req && gnt) |-> ##1 busy );
If req && gnt never becomes true, the implication can pass without checking the expected behaviour.
A corresponding cover property can help establish whether the triggering condition is reachable:
cover property (@(posedge clk) req && gnt );
Coverage analysis should also examine whether important scenarios are reachable under the configured assumptions.
4. Understand the proof status and verification depth
Not every successful run represents an unbounded proof.
A bounded model-checking result may establish that no counterexample was found within the explored depth. That is different from proving the property for all legal executions.
Engineers should distinguish between:
- Proven properties
- Bounded results
- Failed properties
- Unreachable properties
- Inconclusive or unknown results
The report should clearly identify the verification method and its limitations.
5. Review counterexamples, coverage and reproducibility
A failed property should be investigated rather than simply excluded.
A counterexample may indicate a real RTL defect, an incorrect property, an incomplete assumption or a modelling issue.
The final review should include:
- RTL revision and configuration
- Property and assumption versions
- Formal tool settings and run status
- Counterexample analysis
- Reachability and vacuity checks
- Reviewer comments and unresolved limitations
Conclusion
A green formal verification result is useful evidence, but it is not sufficient by itself.
Reliable verification depends on correct properties, justified assumptions, meaningful proof results, coverage analysis and reproducible evidence.
The objective is not simply to obtain passing properties. It is to establish that the intended design behaviour has been checked under the correct conditions.
