Knowing how to write and prove properties is half of formal verification. The other half is deciding what to verify, how far to go, and how to report it so that a project can rely on the result. This chapter covers the methodology: the formal test plan, honest status reporting, sharing assertions with simulation, and the tools that are used in industry.
A formal test plan answers three questions before any property is written: which blocks get formal, what must be proven about each, and what counts as done. Without a plan, formal work tends to drift: a few easy properties get proven, the hard ones are postponed, and nobody can say what was actually verified. This article shows how to build a plan, with a worked example for a small subsystem.
8 min read | Intermediate
What You'll Learn
- Choose the blocks of a design that benefit most from formal
- Derive the list of properties for a block from its specification
- Define the assumptions, the depth and the goal for each block
- Write a plan that simulation and formal teams can share
Step 1: Choose the Blocks
Formal pays off most on blocks that are:
- Control-heavy: arbiters, FIFOs, flow control, state machines, interrupt and power controllers.
- Concurrent: many interfaces whose timing can interleave in many ways.
- Critical: a bug would be expensive, such as a deadlock in a bus fabric or a lost interrupt.
- Small enough: a few thousand registers in the cone of each property, or reducible to that with the techniques of Chapter 8.
Datapaths with wide arithmetic, full processors and whole subsystems are usually left to simulation, with formal used on their control parts. The formal in the design flow article gave the general picture.
Step 2: List the Properties
Go through the specification of the block sentence by sentence, and for each rule write one entry:
| ID | Rule (from the specification) | Kind | Technique |
|---|---|---|---|
| F1 | No push is accepted when full | assert, safety | invariant |
| F2 | Full exactly at 4 entries, empty exactly at 0 | assert, safety | reference count |
| F3 | Words come out in order, unchanged | assert, data | tracked value |
| F4 | The writer only pushes with valid data | assume | interface rule |
| F5 | The FIFO can become full and empty | cover | reachability |
The list grows from four sources: rules about outputs (assertions), rules the neighbors promise (assumptions), situations that must be possible (covers), and data integrity (tracked values). The writing good properties article gives the rules for each entry.
Quick Check
Q: Why does every assumption get its own line in the plan?
Show Answer
Every assumption must be justified by the specification and proven somewhere else, on the block that makes the promise. Listing them makes both of these visible and reviewable.
Step 3: Set the Goal
For each block, decide what "done" means:
- Bug hunting: bounded checks to a stated depth, with covers that show the depth reaches the interesting states. Cheap, good early in a project.
- Full proof: every assertion proven for all cycles, covers reached, assumptions proven on the neighbors. Needed for sign-off of critical blocks.
- Mixed: full proofs for the key properties, bounded results for the rest, with the reason documented.
Also record the depth required and why, as in the choosing a depth article, and any reductions: scaled parameters, cut points, symbolic values.
Step 4: Divide the Work With Simulation
The plan should say, for each feature, whether formal or simulation is responsible, and which assertions are shared. A typical split: formal proves the control rules of the FIFO and the arbiter; simulation covers the end-to-end data flow of the subsystem, with the same assertions enabled in the testbench. The formal and simulation together article explains how the sharing works.
Quick Check
Q: A plan lists 30 assertions for a block but no covers. What is the risk?
Show Answer
The assertions could all pass vacuously, because of an over-constraint or too little depth, and nobody would notice. Every block needs covers for its main activity and for the triggers of its implications.
A Worked Example
A small subsystem has a UART receiver, a 4-entry FIFO, a round-robin arbiter for three bus masters, and a 32-bit CRC unit. A reasonable plan:
- FIFO: full proof. Overflow, flags, data order with a tracked value, covers for full and empty, the helper invariant for induction.
- Arbiter: full proof. Mutual exclusion, validity, fairness within 3 cycles with a hold assumption, covers for a grant to each master.
- UART receiver: bounded, with scaled baud divider. Frame timing and the error flag formally; the full data path in simulation.
- CRC unit: simulation against a reference model, plus an equivalence check after synthesis. No property checking: the arithmetic is the whole function.
Running It in ChipVerify Lab
The plan is a document, not a run. The lab examples of Chapter 7 are a good template for the property lists: each one is a small plan in code, with its assumptions, assertions and covers next to each other.
Common Mistakes
Mistake #1: Starting to write properties without a list
Without a list from the specification, properties follow the RTL and the easy cases. Write the list first, then the properties.
Mistake #2: Leaving the goal open
"Run formal on the FIFO" is not a goal. State whether the result is a bounded bug hunt or a full proof, and what depth or proof status is required.
Mistake #3: Planning formal and simulation separately
Without a shared plan, both teams verify the same easy features and nobody verifies the hard ones.
Practice Exercise
Challenge: Plan a Timer Block
This is a pencil and paper exercise. A watchdog timer block has a 16-bit down counter loaded by software, a kick input that reloads it, an interrupt one cycle before expiry, and a reset output when it reaches zero. Software can lock the configuration until the next reset. Write the property list (with IDs, kinds and techniques) and state the goal and the depth strategy.
Hint
A 16-bit counter cannot be reached from reset within any bounded depth. Which technique from Chapter 5 or 8 helps?
Solution
Assertions: the counter only decreases by one per cycle unless kicked or loaded; a kick reloads it; the interrupt fires exactly one cycle before zero; the reset output fires exactly at zero and stays until the system reset; writes to the configuration have no effect once locked. Assumptions: software writes follow the bus protocol. Covers: interrupt, reset output, a write while locked. Goal: full proof by induction, with the 16-bit width scaled down by a parameter for the bounded checks, and start-anywhere runs for the expiry behavior.
Summary
- Choose blocks that are control-heavy, concurrent, critical and small enough.
- List properties from the specification: assertions, assumptions, covers and data checks, each with an ID and a technique.
- Set a goal per block: bounded bug hunt, full proof, or a documented mix.
- Record depths, reductions and the division of work with simulation.