Formal verification is used at several points of a chip project, by different people, for different reasons. A designer may run a quick formal check on a block on the day it is written. A verification engineer may spend weeks proving the rules of a cache controller. And every netlist goes through an equivalence check before it is sent to manufacturing. This article follows a block through the flow and shows where formal fits, who does it, and what it costs.
7 min read | Beginner to Intermediate
What You'll Learn
- Describe where formal verification is used in a chip project
- Explain the difference between designer formal and formal sign-off
- Choose which blocks of a design are good candidates for formal
- Name the common commercial and open-source formal tools
Formal Across the Flow
While the RTL Is Written: Designer Formal
The earliest use is by the designer. A new block has no testbench yet, but its rules are fresh in the designer's mind. A few assertions and an assumption about the reset are enough for a formal tool to start looking for bugs. Within minutes it shows counterexamples for mistakes such as a counter that wraps at the wrong value, a missing case in a state machine or a FIFO that accepts a write when it is full.
This is cheap and fast, because the counterexamples are short and point straight at the cause. It is sometimes called bug hunting, because the goal is to find bugs early, not to prove everything. The assertions written here stay in the code and are reused later.
Quick Check
Q: Why can a designer run formal before any testbench exists?
Show Answer
Formal needs no stimulus. The tool chooses the inputs itself, so a few assertions and an assumption about the reset are enough to start.
During Block Verification: Formal Sign-Off
For the most critical blocks, a verification engineer goes further. The goal is to prove every important rule of the block, not just to find a few bugs. This needs a written plan of the properties, careful assumptions about the inputs, and often techniques to keep the problem small enough for the tool. The result is reported as the status of each property: proven, bounded to a depth, or failed.
Good candidates for this level of effort share a few traits:
- Control logic with many corner cases: arbiters, FIFOs, interrupt controllers, cache coherence, credit and flow control.
- Rules that are easy to state and hard to test: no deadlock, no data loss, mutual exclusion.
- Blocks of moderate size, with interfaces that can be described by assumptions.
Poor candidates are large data paths with deep arithmetic, such as a floating-point unit, and whole subsystems. They are verified mainly by simulation, or with special formal techniques covered later in this tutorial.
Together With Simulation
Formal and simulation share the assertions. A property that a formal tool proves is also compiled into the simulation, where it fires if a test ever breaks it. Formal covers the rules of the block, and simulation covers the full function, the integration and the long scenarios. Teams decide block by block which method carries the main load, and the verification plan records it.
After Synthesis and Changes: Equivalence
Once synthesis has turned the RTL into a netlist, an equivalence check confirms that the two match. The same happens after the netlist is changed, for example to insert test logic, to fix timing, or to correct a late bug by hand. These checks are routine on every project, and they are almost always formal.
Who Does What
| Stage | Who | Goal | Typical effort |
|---|---|---|---|
| RTL writing | Designer | Find bugs early | Hours per block |
| Block verification | Verification or formal engineer | Prove the key rules | Days to weeks per block |
| Synthesis and ECO | Implementation team | Netlist matches RTL | Automated, every run |
| Sign-off | Verification lead | Report proof status and coverage | Part of the verification review |
Quick Check
Q: A team has a 64-bit floating-point multiplier and a 4-input arbiter. Which one is the better first candidate for formal property checking?
Show Answer
The arbiter. It is control logic with clear rules and tricky orderings, and it is small. The multiplier has deep arithmetic, which is hard for a formal tool, and is usually verified with simulation against a reference model.
The Tools
The most widely used commercial formal tools are Cadence Jasper, Synopsys VC Formal and Siemens Questa Formal. They read the full SystemVerilog and SVA languages, include the apps, and handle large designs. On the open-source side, SymbiYosys runs Yosys and a choice of solvers. It is the engine in ChipVerify Lab. The ideas of this tutorial, properties, assumptions, counterexamples, depth and proofs, are the same in all of them.
Running It in ChipVerify Lab
The lab is set up for the first stage: write a block, add a few properties, and run a formal check in a minute. The examples of the following chapters follow that workflow, and later chapters show proofs and equivalence checks with the same engine.
Common Mistakes
Mistake #1: Starting formal at the end of the project
Formal is cheapest when the block is new and small and its rules are fresh. Started late, it finds bugs that are expensive to fix, on blocks that have grown complex.
Mistake #2: Aiming formal at the whole chip
Formal tools work on blocks. Pick the critical control blocks and prove their rules, and leave the full-chip function to simulation.
Practice Exercise
Challenge: Plan the Formal Work
This is a pencil and paper exercise. A small chip has these blocks: a UART, a 4-entry FIFO between two parts of the logic, a round-robin arbiter for a shared memory, a 32-bit multiply-accumulate unit, and the top level that connects them. For each block, say whether you would use formal, simulation, or both, and give one property you would prove with formal where it fits.
Hint
Look for control logic with clear rules and moderate size. Deep arithmetic and the full top level are better served by simulation.
Solution
FIFO: formal, for example "no write is accepted when full, no read when empty". Arbiter: formal, for example "at most one grant at a time" and "a request is granted within 4 cycles". UART: both, formal for the frame control, such as "busy stays high from start until the stop bit", and simulation for the full transfer. Multiply-accumulate: mainly simulation against a reference model. Top level: simulation for the integration, plus an equivalence check after synthesis.
Summary
- Designers use formal early to find bugs in new blocks without a testbench.
- Verification engineers prove the key rules of critical control blocks, and report proof status at sign-off.
- Equivalence checking confirms that every netlist matches its RTL after synthesis and changes.
- Formal and simulation share assertions and divide the work block by block.
- Commercial tools are Jasper, VC Formal and Questa Formal; SymbiYosys is the open-source engine used in ChipVerify Lab.
