"All assertions pass" can mean anything from "proven for all time, with every trigger reachable" to "checked for three cycles under an assumption that blocks every input". A formal report is only useful if each result carries its real status and the evidence that the check meant something. This article defines the statuses, explains formal coverage, and shows a report for a FIFO that a reviewer can trust.
8 min read | Intermediate
What You'll Learn
- Report each property with an exact status: proven, bounded, failed, vacuous or unknown
- Explain formal coverage and why passing assertions need it
- Write a status report that a reviewer can check
- Recognize the common ways formal results are oversold
The Statuses
- Proven: holds in every cycle from reset, by induction, PDR or complete BMC. The strongest result.
- Bounded (depth k): no failure within k cycles. Report k, and the reason it is meaningful.
- Failed: a real counterexample from reset. Each failure is either fixed, or waived with a reason.
- Vacuous: passes because a trigger never happens. Treat it as a finding.
- Unknown: the induction step failed and no bounded result was required. Usually reported as bounded instead.
Formal Coverage
A pass says nothing about whether the check exercised anything. Formal coverage answers that, in several layers:
- Cover properties: each intended behavior is reached, at which step. This is the minimum.
- Trigger coverage: the trigger of every implication is reachable, so no assertion is vacuous.
- Cone-of-influence coverage: which lines and registers of the RTL lie in the cone of at least one assertion. Logic in no cone is not checked by formal at all.
- Proof-core or mutation coverage: which parts of the design the proof actually depended on. Commercial tools compute this by checking whether a property still passes when a piece of logic is changed or removed. Logic that can be broken without any property failing is not really verified.
Cover properties and trigger coverage can be done with any tool, as this tutorial has shown. The last two layers are features of commercial tools.
Quick Check
Q: All assertions of a block are proven, but mutation coverage shows that the error flag logic can be changed without any property failing. What does that tell you?
Show Answer
No property checks the error flag. The proofs are real but incomplete: a property for the error behavior is missing from the plan.
A Status Report
For a 4-entry FIFO with the pointer flags of the synchronous FIFOs article and a tracked-value data check, results from the lab engine:
| ID | Property | Status | Evidence |
|---|---|---|---|
| F1 | Reference count never above 4 | Proven (k-induction, k = 1) | helper: count = wptr - rptr |
| F2 | full exactly at 4, empty exactly at 0 | Proven (k = 1) | same helper |
| F3 | Data order (tracked value) | Bounded, depth 10 | covers: magic leaves by step 2, full by step 5 |
| C1 | FIFO becomes full | Reached, step 5 | trace attached |
| C2 | Push and pop in the same cycle while full | Reached, step 5 | trace attached |
| A1 | Assumption: none on push/pop | n/a | inputs fully free |
The report states what was proven, what was only bounded, and why the bounded result is still meaningful. It lists the assumptions, here none, and the helper invariants. A reviewer can check each line.
Quick Check
Q: What should a reviewer ask about the row for F3?
Show Answer
Whether depth 10 covers every way the tracked word can travel through a 4-entry FIFO, including a full FIFO and simultaneous push and pop. The covers suggest yes, but a proof would remove the question.
How Results Get Oversold
- Bounded results reported as "pass" without the depth.
- No covers, so vacuous passes go unnoticed.
- Assumptions not listed, or not proven on the neighbor.
- Scaled-down parameters not mentioned: a proof for a 4-entry FIFO is not automatically a proof for 64 entries, unless the design is written so that the size is only a parameter.
- Waived failures without a reason.
Running It in ChipVerify Lab
The lab reports each run as PASS or FAIL within a depth, which is a bounded status. Keep a note of the depth with every result you record, and use meant-to-fail checks for the cover evidence, as the cover properties article showed.
Common Mistakes
Mistake #1: Reporting PASS without a status qualifier
Every pass is either proven or bounded at a depth. Say which.
Mistake #2: Counting assertions instead of coverage
A large number of passing assertions says nothing about how much of the design is checked. Report covers and cone or mutation coverage.
Mistake #3: Hiding the reductions
Cut points, black boxes and scaled parameters change what a result means. List them in the report.
Practice Exercise
Challenge: Review a Report
This is a pencil and paper exercise. A colleague reports for an arbiter: "Mutual exclusion: pass. Fairness: pass. All 12 assertions pass at depth 8. No issues." Write the questions you would ask before accepting it.
Hint
Think about status, depth, assumptions, covers and reductions.
Solution
Are the passes proven or bounded? Why is depth 8 enough: what is the worst-case wait, and is it inside the depth? Which assumptions were used, in particular for fairness, and are they proven on the requesters? Which covers were reached: a grant to every requester, a tie between all of them? Were any parameters reduced, such as the number of requesters? Without these answers, "pass" is not a sign-off result.
Summary
- Report each property as proven, bounded with its depth, failed, vacuous or unknown.
- Formal coverage shows that the checks exercised the design: covers, triggers, cone of influence, and proof-core or mutation coverage.
- A good report lists assumptions, helpers, reductions and the evidence for every bounded result.
- Results are oversold through missing depths, missing covers, hidden assumptions and unmentioned reductions.
