Formal verification is the use of mathematical analysis, rather than test vectors, to prove that a chip design meets its specification. A formal tool takes the RTL and a set of properties (assertions about how the design must behave) and either proves each property holds for every possible input sequence and reachable state, or returns a counterexample trace that shows exactly how it fails. In semiconductor engineering it is used to find corner-case bugs that simulation misses, and, with careful planning, to sign off whole blocks.
Key takeaways
- Simulation checks the scenarios you thought of. Formal checks all of them, within the limits of the properties, constraints and proof depth you give it.
- Formal verification comes in two main forms: property checking (model checking) of RTL against assertions, and equivalence checking between two versions of a design.
- A formal result is only as good as its properties and constraints. Over-constraining can hide real bugs behind a clean proof.
- Formal signoff needs planning, reviews and metrics: test plan, property review, coverage, proof status, constraint validity, proof depth and functional coverage.
What is formal verification?
Formal verification is a powerful and essential technique for ensuring the correctness and quality of semiconductor designs. Unlike simulation or emulation, which rely on testbenches and test vectors to exercise the design, formal verification uses mathematical analysis to exhaustively check the design against user-specified properties. These properties can be assertions that describe the intended behaviour of the design, constraints that control the analysis, or cover points that measure how well the analysis exercises the design.
Formal verification can find subtle and corner-case bugs that may escape simulation or emulation, and can provide a higher level of confidence in the design functionality. However, formal verification also requires careful planning, rigorous reviews, and comprehensive metrics to achieve a quantifiable measure of functional verification completeness.
Formal verification is therefore an essential part of semiconductor development. By following the steps of formal signoff discussed in this article, semiconductor developers can gain confidence that their designs are correct and of high quality, and that they are ready for fabrication.
Why exhaustive matters: a quick calculation
Consider a simple 64-bit adder. It has 128 input bits, so 2 to the power 128, roughly 3.4 x 10^38, input combinations. Even at an optimistic one billion simulated vectors per second, covering them all would take around 10^22 years. A formal tool does not enumerate values one by one: it reasons about the logic symbolically, using techniques such as SAT solving and binary decision diagrams, so it can prove a property for all values at once. Sequential designs add the dimension of time, which is where proof depth, discussed below, comes in.
Types of formal verification
| Type | What it checks | Typical use |
|---|---|---|
| Property checking (model checking) | RTL against assertions written in SystemVerilog Assertions (SVA) or PSL | Control logic, arbiters, FIFOs, protocol interfaces, cache coherence |
| Combinational equivalence checking | Two netlists or RTL and netlist implement the same logic, register by register | Signoff after synthesis, scan insertion, ECOs |
| Sequential equivalence checking | Two designs give the same outputs when registers or timing differ | Clock gating, retiming, pipeline changes |
| Formal apps | Targeted, often automatic checks | Connectivity, X-propagation, register maps, unreachable code, security paths |
A small example
Here is a two-requester round-robin arbiter with three properties: a safety assertion that the grants are never both high, an assertion that a grant is only given to a requester that asked for it, and a cover point that checks both requesters can ask at the same time.
module arb (input logic clk, rst_n, req0, req1, output logic gnt0, gnt1);
logic last; // 1 = last grant went to requester 1
always_ff @(posedge clk or negedge rst_n)
if (!rst_n) begin gnt0 <= 0; gnt1 <= 0; last <= 1; end
else begin
gnt0 <= req0 & (~req1 | last);
gnt1 <= req1 & (~req0 | ~last);
if (req0 & (~req1 | last)) last <= 0;
else if (req1) last <= 1;
end
a_onehot: assert property (@(posedge clk) disable iff (!rst_n) !(gnt0 && gnt1));
a_gnt0: assert property (@(posedge clk) disable iff (!rst_n) gnt0 |-> $past(req0));
a_gnt1: assert property (@(posedge clk) disable iff (!rst_n) gnt1 |-> $past(req1));
c_both: cover property (@(posedge clk) req0 && req1);
endmoduleA simulation testbench would check these only for the stimulus it happens to generate. A formal tool proves them for every input sequence from reset. If a later change broke the priority logic, the tool would return a short waveform showing the failing sequence, which is often easier to debug than a long simulation failure.
The seven steps of formal signoff
Finding bugs with formal is one thing. Claiming that formal has completed the verification of a block is another, and it needs evidence. The seven steps below can help semiconductor developers achieve this goal.
Step 1: Review the test plan and the specification
The first step is to ensure that the test plan accurately reflects the intended functionality of the design as described in the specification. The test plan identifies the design features that need to be verified and how they will be verified. The formal verification team will use the test plan to write properties that check and cover these features. If the test plan is incomplete or inconsistent with the specification, then the properties may also be incomplete or incorrect.
Step 2: Review the properties and the formal results
The second step is to have the design engineers review the properties and the formal results. The design engineers have deep insight into their own RTL code and the intended behaviour of the design, so they can verify that the properties are correct and sufficient, and that the formal results are consistent with their expectations. They can also provide feedback on how to improve or optimise the properties or the formal analysis.
Step 3: Check property coverage
The third step is to check how well the properties cover the design. Property coverage measures how much of the design functionality is specified by assertions and cover points. Tools typically measure it structurally, for example by checking which parts of the logic fall inside the cone of influence of at least one assertion. A high property coverage indicates that the design has been thoroughly checked and exercised by formal verification. A low property coverage may indicate that some design features are missing from the test plan or that some properties are too abstract or too specific.
Step 4: Check proof status
The fourth step is to check the proof status of each property. The proof status indicates whether formal verification has been able to prove or disprove a property, or whether it has reached a limit in terms of time, memory or sequential depth.
| Status | Meaning | What to do |
|---|---|---|
| Proven | The property holds for all possible inputs and reachable states of the design | Check it is not vacuous, that is, that its trigger can actually occur |
| Disproven (counterexample) | The tool found a trace where the property fails | Decide whether it is a design bug, a wrong property or a missing constraint |
| Bounded (inconclusive) | The property holds up to a certain number of cycles, or within certain assumptions, but is not fully proven | Compare the bound with the depth needed to reach the relevant behaviour (step 6) |
Step 5: Check constraint validity
The fifth step is to check whether any constraints used in formal verification are valid. Constraints are assume properties that restrict the input space or state space of formal analysis. They can help reduce complexity, improve performance, and avoid false failures. However, constraints must be carefully written and reviewed to ensure that they do not over-constrain or under-constrain the design. Over-constraining may lead to invalid proofs where some bugs are masked by unrealistic assumptions. Under-constraining may lead to invalid counterexamples where some failures are caused by unrealistic inputs. A practical check is to prove the same assumptions as assertions on the neighbouring block, or in simulation, so they are known to match real behaviour.
Step 6: Check sequential depth
The sixth step is to check whether formal verification has analysed the design at sufficient sequential depth. Sequential depth measures how many clock cycles are needed to reach a certain state or behaviour in the design. Formal verification can prove properties at any sequential depth, but it may take longer or require more resources as the depth increases. Therefore, a reasonable target depth should be set for each bounded property based on its complexity and relevance. A target depth should be large enough to cover all possible scenarios of interest, such as filling a FIFO to full, but not so large that it causes unnecessary overhead. Reaching each relevant cover point gives a useful lower bound on the depth needed.
Step 7: Check functional coverage
The seventh and final step is to check how well formal verification has exercised the design functionality. Functional coverage measures how many cover points have been hit by formal analysis. Cover points are properties that specify interesting or critical states or behaviours in the design. A high functional coverage indicates that formal verification has explored a large portion of the design space and has not missed any important cases. A low functional coverage may indicate that some cover points are unreachable or too difficult for formal verification, or that some scenarios are missing from the test plan. An unreachable cover point is also a strong hint that a constraint is too tight.
Published signoff methods from EDA vendors and conference papers use broadly similar checks, sometimes with different names and extra steps, such as identifying the minimum logic each proof actually depended on (the formal core) and injecting faults into the design to confirm that the assertions catch them.
Common mistakes
- Treating a full set of passing proofs as signoff without checking for vacuity, over-constraints and coverage.
- Accepting bounded proofs without comparing the bound with the depth the design needs.
- Applying formal to large datapath blocks first, where proofs struggle, rather than to control-heavy blocks where it pays off quickest.
- Letting the verification engineer write all properties without design review, so misunderstandings of the specification go into both RTL and properties.
FAQ
Does formal verification replace simulation?
Not on a full chip. Formal is strongest on blocks of moderate size and on specific questions. Simulation and emulation are still needed for system-level behaviour, software and performance. Many teams sign off selected blocks with formal and use simulation elsewhere.
What language are properties written in?
Most commonly SystemVerilog Assertions, defined in IEEE 1800. PSL (IEEE 1850) is also supported by many tools, especially in VHDL flows.
What is a counterexample?
A waveform trace from reset that shows a sequence of inputs which makes a property fail. It is usually short, which makes it quick to debug.
Is equivalence checking formal verification?
Yes. It mathematically proves that two representations of the design, for example RTL and the synthesised netlist, behave the same, and it is a standard signoff step in every ASIC flow.
Your comments will be moderated before it appears here.