This checklist condenses the tutorial into the steps a formal verification task goes through, from a new block of RTL to properties you can sign off. Use it as a review guide for your own work and for others': every item is something that, when skipped, has produced a false sense of security in a real project. Each item links to the article that explains it.
7 min read | Intermediate
What You'll Learn
- Walk through a formal task in the right order
- Review a property set for completeness and correctness
- Check that a run was meaningful, not just green
- Decide when a block is done
1. Before Writing Properties
- The block is a good formal candidate: control-heavy, concurrent, critical, and small enough, or reducible. (A formal test plan)
- Every size in the RTL comes from a parameter, so the block can be shrunk. (Shrinking the problem)
- The specification is at hand, sentence by sentence, including the interface rules of the neighbors.
- The goal is set: bounded bug hunt to a stated depth, or full proof.
2. Writing Properties
- Every property comes from the specification, not from the RTL. (Writing good properties)
- One idea per assertion, with a clear name.
- Invariants for ranges, one-hot, mutual exclusion and consistency. (Invariants)
- Multi-cycle rules with the right implication:
|->or|=>. (Sequences and implication) - Handshake rules for every interface. (Handshake properties)
- A data property for every block that stores or moves data. (Data integrity)
- A progress rule with a bound for every block that must answer. (Safety and liveness)
- Every
$pastguarded against the first cycles. ($past and friends)
Quick Check
Q: A property set for a FIFO has overflow and underflow rules and nothing else. Which checklist items does it miss?
Show Answer
Flags against the specified depth, a data property such as a tracked value, covers for full and empty, and, for a proof, the count helper invariant.
3. The Environment
- Reset assumed in the first cycle, and free afterwards. (Reset and initial state)
- Every assumption traced to the specification and as weak as possible. (Why assumptions are needed)
- Every assumption proven on the neighbor or validated in simulation. (Assume-guarantee)
- No assumption on an output or internal signal of the design.
- No initial values that hide a missing reset in an ASIC design.
4. Running
- The depth is derived from the design and confirmed by covers. (Choosing a depth)
- Every trigger and every main behavior is covered, and every cover is reached. (Cover properties, Vacuity)
- No over-constraint: covers for legal-but-unusual situations are reachable. (Over-constraining)
- Every counterexample read backwards to its cause, and the fix rerun. (Debugging)
- Slow runs reduced with depth, parameters, cut points or smaller properties, not just retried. (Performance)
5. Proving
- Induction attempted for every key property. (Induction)
- Step failures checked for unreachable start states. (Unreachable states)
- Helpers added one at a time, as assertions, never assumptions. (Strengthening)
- Formal-only registers in the step have no initial values. (FIFO capstone)
6. Reporting
- Each property marked proven, bounded at a stated depth, failed, or vacuous. (Proof status)
- Assumptions, helpers, cut points and scaled parameters listed.
- Covers reported with the step at which they were reached.
- The shared assertions enabled in simulation. (Formal and simulation)
- After synthesis or netlist edits, an equivalence check. (Equivalence)
Quick Check
Q: A block's report says "all 25 assertions proven". Which three checklist items would you verify first?
Show Answer
That covers were reached (no vacuity), that the assumptions are justified and proven elsewhere (no over-constraint), and that no reductions such as cut points or scaled parameters change what "proven" means.
Running It in ChipVerify Lab
Every item above has a lab example in this tutorial. The capstones of this chapter apply the whole list to a FIFO, an arbiter and a UART transmitter.
Common Mistakes
Mistake #1: Using the checklist only at the end
Items 1 to 3 shape the work. Checking them after the properties are written means rewriting.
Mistake #2: Treating green as done
A run with no failures is item 4 at best. Items 4 to 6 decide whether it means anything.
Practice Exercise
Challenge: Review a Lab Example
This is a review exercise. Pick any lab example from Chapter 7, open it, and go through sections 2 to 5 of the checklist. Write down every item it does not meet, and decide whether that matters for the block.
Hint
Most Chapter 7 examples focus on one bug. Look especially at covers, data properties and proofs.
Solution
For example, the round-robin arbiter example of the arbiters article has safety and fairness rules and a hold assumption, but no covers and no proof. Both are added in the arbiter capstone: covers for a grant to requester 3, all four requests and the 4-cycle wait, and a k-induction proof with k = 5. The hold assumption still needs to be checked on the requesters.
Summary
- Prepare: candidate block, parameters, specification, goal.
- Write: from the specification, one idea per assertion, with data and progress rules.
- Constrain: reset, justified and proven assumptions, nothing on outputs.
- Run: derived depth, reached covers, no over-constraint, debugged counterexamples.
- Prove and report: induction with helpers, honest statuses, listed reductions, shared assertions, equivalence after synthesis.
