Formal Verification: Where to use it and Why?
In short: Formal verification uses mathematics to prove a design property is always true, for every possible input, instead of checking a few cases with simulation. It pays off most when you apply it function by function, not block by block: pick the parts that are hard to cover in simulation, carry the most risk, or suit formal well (like arbiters, decoders, and interfaces). Good methodology and tool choice matter as much as the design itself.
As tools and methods improve, formal functional verification now applies to far more areas than before. If you understand what makes an area a good fit for formal, you can pick not just which blocks are good candidates but which functions inside a block give the best return on the time you invest. Today, formal is often most valuable applied partially inside a block, on the functions with the highest payoff. This post explains where to use formal verification and why, with real examples.
A simple way to picture it
Think of two ways to check that a locked door is truly safe. Simulation is like sending a hundred people to try the handle at different times: if none get in, you feel fairly confident, but you never tried every person or every moment. Formal is like a mathematician proving that, given how the lock is built, no key except the right one can ever open it, for all time. When you can get that proof, it is far stronger than any number of trials. But some doors are too oddly shaped to prove anything about, and there formal is the wrong tool. The skill is knowing which doors to prove and which to keep testing by hand.
Three reasons to use formal verification
There are three goals when reaching for a formal tool:
- Do what simulation cannot, such as proving a property holds for every input, not just the ones you happened to test.
- Do the same job faster, reaching a result more quickly than a simulation campaign would.
- Add another path to full coverage, complementing your existing tools and methods.
Whatever the goal, the return on effort has to be worth it. That is why you choose targets carefully rather than applying formal everywhere.
Identify high-risk areas
Not all blocks and functions carry equal risk. Consider an L2/L3 Ethernet switch built from an earlier L2-only design. Some blocks (the MAC, CSR, PCI, and memory interface) are legacy code with little risk. The new L3 block is verified heavily at block level because system-level coverage for all the different L3 traffic is hard, and new code is always more exposed to bugs.
The ingress parses the L2 and L3 headers and runs the checks (CRC for L2, checksum for L3) to decide whether to drop a packet. L2 parsing is old, low-risk code; L3 is new, higher-risk code. Even within one block, some functions cause only a small performance dip if wrong, while others cause major system failures. Late specification changes add risk too: because the L3 block supports many policies, a late change to add a policy could break existing working functions. Applying formal here, to prove new functions and re-check existing ones, is attractive.
To choose formal targets, weigh three factors: how hard the function is for other methods, the risk the function carries, and how well the function suits formal. In this example the L3 block is a good candidate for full formal, the ingress block is a good candidate for partial formal, and the CSR block is the lowest priority. Fixing block-level bugs with formal before system-level simulation saves time, because bugs found at the system level cost far more to fix. For the underlying property language, see our assertions guides.
Blocks that are difficult to verify with simulation
- Many input possibilities: the bridge must handle every packet length and type, varied arrival times, and flow control from egress. Simulation struggles to reach high confidence across so many inputs.
- Many configurations: the switch can have any number of active ports, different policy thresholds, and various external memory sizes. Verifying every mode fully is not practical, so teams pick a few representative modes, and formal can cover the rest.
- Standard protocols to another chip: a standard protocol is general and carries many requirements, and a normal testbench does not exercise them all. Formal can close that gap.
Applying formal: properties beat a reference model
Many areas once thought unsuitable for formal are now the main targets, thanks to better engines and, above all, better methodology. Consider a reordering buffer that holds transactions to and from memory and follows two rules: if a newer entry is in the same burst as the oldest entry, it is reordered to combine with it; if a newer entry is in the same row as the oldest entry, it is reordered to sit next to that transfer.
One obvious approach is to build a reference model that keeps a queue and predicts the output. That has real drawbacks:
- The reference model is about as complex as the design, so the problem doubles in size.
- A cycle-accurate model can end up too close to the implementation to catch its bugs.
- Any spec change forces a major rework, because the functions are interdependent.
- Proving the reference model itself is correct is hard, so building and maintaining it can cost as much as the design.
A better approach is to write properties that check the reordering directly. One strategy:
- Register the last entry entering the queue (call it E1) and the number of outstanding entries (N1).
- If the exiting entry is of the same row and burst, the next entry out should be E1.
- If the exiting entry is of the same row, the next entry out should be E1 or another entry with the same row and burst.
- If the exiting entry is not of the same row, the next entry out should not be E1 unless N1 is 1.
- No entry should exit after E1 if N1 is 0.
This breaks one big problem into several small properties. When the spec changes, most properties still apply; you simply add or remove a few. Good planning and methodology are what make formal succeed.
Which functions suit formal, and which do not
Arbiters and decoders
Formal applies well to arbiters, though few handle complex schemes correctly. If a port’s priority rises on some events and falls on others, one giant property gets very complicated. Instead, split the arbiter into two functions: the arbitration based on current priorities, and the events that raise or lower priority. Verified by separate properties, each becomes a simple problem. Step up one level and an arbiter is really a kind of decoder with a small sequential depth (few cycles to reach all its states).
This leads to a common myth.
Myth 1: decoders are not suitable for formal. Arbiters are a classic sweet spot for formal, and since an arbiter is a form of decoder, the myth breaks down. The key is to apply formal to the decoder in isolation. If a decoder is very implementation-specific and not an area of concern (for example, one that just decodes an address to hit or miss), it may not need formal. If it is complex and you can specify it differently from the implementation (like a scrambler or an 8b10b decoder), formal is worthwhile. But for overly complex logic such as digital filters or floating-point algorithms, the properties are too hard to state, so formal is not the right fit at the functional level.
Interfaces
Interfaces are another sweet spot: they have a lot of concurrency but are not sequentially deep, and their properties are straightforward. Many standard protocols use a master/slave relationship, which maps neatly to a constraint/assertion pair, so one set of constraints and assertions can verify both the master and the slave.
Newer interfaces use packets and cells to carry commands and data, which pushes the sequential depth high and makes properties harder to model, because the handshake is now between packets rather than signals. Engineers often avoid these, but they are not that different from signal-handshake interfaces.
Packet-based designs and data transport
In the Ethernet design of Figure 1 there are three interface levels. The physical layer is a traditional interface, but L2 and L3 are not: to get their control information you must parse the packet headers, so one handshake that used to take a few cycles now spans a few packets, or hundreds to thousands of cycles. That seems impractical for formal, which leads to another myth.
Myth 2: packet-based design is not suitable for formal because of its sequential depth. Good methodology and tools solve this. Do not combine inter-layer protocols into one property set. When you verify L2, you clearly need the physical layer to capture the packet, but there is no reason to fold the L3 header and payload analysis into the L2 properties. Careful partitioning removes most of the states tied to L3 or the payload, especially if the tool can analyse the effective cone-of-influence beyond the traditional computation. The modeling layer of the property also matters, though the detail is beyond this article.
Now extend interfaces to a cause-and-effect relationship. Naming and listing such behaviours simplifies an otherwise complex design. Interrupt handling, for instance, is the cumulative handling of individual interrupts, so it can be enumerated. Instruction handling is often complex, but you can still verify the most important functions like exception handling and branch prediction, which the processor architecture usually describes clearly.
Myth 3: avoid formal for data-transport blocks. Data transport appears in many designs, and engineers often think formal does not apply because it involves storage elements and large sequential depth. The simplest start is local assertions along the datapath, which gives value in small steps. Better still, verify the whole path without breaking it down when you can, because that means far fewer properties and frees you from inventing implementation-specific checks along the path. Recent methodology makes end-to-end data-transport properties both possible and desirable: the sequential-depth issue is handled with the packet-based approach above, and storage elements, usually not the concern, can be abstracted away.
One caution: liveness properties
Data-transport checks usually look for wrong or corrupted data at the output. But if the data never comes out, there is no violation to catch, so you also need to state that data should eventually appear. That is a liveness property, and liveness is one area not recommended for formal:
- Liveness usually needs fairness constraints. Flow controls along a datapath can, in theory, be asserted forever, so you must add fairness so they are released from time to time, and finding all such spots is tedious.
- Most formal tools do not support liveness, and those that do have too little capacity to be useful.
- The practical fix: model most liveness properties as safety properties, which tools verify effectively. With the right methodology you can still ensure correctness.
Formal fit at a glance
| Function or block | Fit for formal | Why |
|---|---|---|
| Arbiters | Strong | Small sequential depth; split priority logic from the arbitration scheme into simple properties. |
| Decoders (in isolation) | Strong | A form of decoder; good when you can specify it differently from the implementation. |
| Simple address decoders | Low | Very implementation-specific and often not an area of concern. |
| Digital filters, floating-point | Poor | Properties are very hard to state and the logic is too complex at the functional level. |
| Interfaces (signal handshake) | Strong | High concurrency, low sequential depth, straightforward properties. |
| Packet or cell interfaces | Workable | High sequential depth, but careful partitioning and cone-of-influence analysis make it practical. |
| Data transport (safety) | Workable | Verify end-to-end; abstract storage elements; use safety properties. |
| Liveness (eventually) checks | Poor | Needs fairness constraints; poor tool support; model as safety properties instead. |
Conclusion
To get the most from formal verification, judge applicability by the type of function inside a block, not by the design type. Weigh three things: how hard the function is for other methods, the risk it carries, and how well it suits formal. Remember that methodology and tool choice matter as much as the design. And avoid all-or-nothing thinking: most blocks have at least some functionality that fits formal. With good planning (including test planning), the right methodology, and the right tool, formal functional verification pays off. For where formal sits next to simulation-based checking, see our assertions and functional coverage guides.
Expected result, in plain words
This is guidance, not a single tool run. When you target the right functions, the practical result is that formal proves the chosen properties hold for all inputs (or returns a counterexample waveform you can debug), and it does so before system-level simulation where fixes are costly. Results depend heavily on your property set, constraints, and tool capacity, so confirm proofs, bounds, and any assumptions on your own formal tool. This material follows the EETimes article “Formal verification: where to use it and why”.
Frequently asked questions
What is formal verification?
Formal verification uses mathematics to prove that a design property holds for every possible input, rather than checking a limited set of cases through simulation. When a proof succeeds, it is far stronger evidence than any number of simulation runs.
When should you use formal verification?
Use it to do what simulation cannot (prove a property is always true), to reach a result faster than a simulation campaign, or to add another route to full coverage. Target functions that are hard to cover in simulation, carry high risk, or suit formal well.
Which blocks are good candidates for formal verification?
Arbiters, decoders applied in isolation, and signal-handshake interfaces are classic sweet spots. New or high-risk blocks with many configurations, like a new L3 Ethernet block, are also strong candidates.
Where is formal verification a poor fit?
Overly complex logic such as digital filters or floating-point algorithms, very implementation-specific address decoders that are not a concern, and liveness (eventually) properties, which need fairness constraints and have weak tool support.
Why are properties better than a reference model for formal?
A reference model is about as complex as the design, can drift too close to the implementation, needs major rework on any spec change, and is hard to prove correct. Writing several smaller properties is more maintainable and survives spec changes better.
Can formal verification handle packet-based designs despite deep sequential behaviour?
Yes. Do not combine inter-layer protocols into one property set. Careful partitioning and cone-of-influence analysis remove most of the irrelevant states, so packet and cell interfaces become practical for formal.
How do you apply formal to arbiters?
Split the arbiter into two functions: the arbitration based on current priorities, and the events that raise or lower priority. Verifying each with separate properties turns one complicated problem into two simple ones.
How do you handle liveness properties in formal verification?
Because most tools support liveness poorly, model most liveness checks as safety properties, which tools verify effectively. With the right methodology you can still ensure the data eventually appears at the output.
