Coverage Closure with Proof: Formal Reachability and UNR Analysis
An uncovered point is not automatically a verification gap. It may be unreachable—but that conclusion should be proven, not assumed.
Near the end of a verification cycle, uncovered points usually fall into different categories:
- A test has not exercised the point
- The point is reachable but still uncovered
- The point is structurally impossible to reach
- The available analysis cannot determine the answer
Treating every uncovered point the same creates unnecessary tests. Waiving them without evidence creates a different risk.
Formal reachability provides a stronger path to closure.
Three outcomes instead of two
vWIZ-Coverage combines simulation coverage with formal unreachability analysis to classify coverage points as:
COVERED
Simulation reached the point
UNREACHABLE
Formal analysis proved the point cannot occur
OPEN
The point is reachable or remains undetermined
Every uncovered point retains its formal verdict and the evidence supporting it.
Only points proven unreachable are retired from the coverage target. Reachable and undetermined points remain in the denominator and continue to count against closure.
This keeps unknowns visible instead of silently converting them into exclusions.
Refine the denominator—not the numerator
Formal analysis does not create coverage hits.
If three points are proven structurally dead, those points may leave the target denominator. The number of covered points does not increase.
Raw coverage
↓
Formal reachability analysis
↓
Proof-refined coverage
The movement from raw coverage to proof-refined coverage remains visible and traceable.
Every denominator change should be connected to formal evidence—not hidden behind a modified percentage.
Simulation evidence must win contradictions
Formal results should not be accepted blindly.
Consider this conflict:
Formal verdict : UNREACHABLE
Simulation hits: 48
A point reached during simulation cannot also be unreachable.
A reliable evidence-join process must reject the contradictory formal bundle, preserve the existing coverage database and identify the offending point.
This independent check is essential. Otherwise, formal analysis becomes another source of claims instead of an arbiter of evidence.
Proof versus waiver
A manual waiver says:
We believe this point cannot happen.
Formal reachability says:
Here is the evidence that this point cannot happen.
That difference matters during reviews, audits and signoff. Proof-refined coverage can be re-derived from the raw data, formal verdicts and exclusion history.
The takeaway
Coverage closure should distinguish between:
What simulation covered
What formal analysis proved impossible
What still remains unknown
A point should leave the coverage target only when the evidence earns that decision.
👉 Explore the complete formal reachability and UNR-closure workflow on WIOWIZ
#verification #formalverification #semiconductor #vlsi
Top comments (0)