Connectivity Checking Is A Perfect Fit For Formal Verification

Formal verification has traditionally been regarded as an advanced technique for experts to thoroughly verify individual blocks of logic, or perhaps small clusters of blocks. However, if you talk to anyone involved in the field these days, you’ll find that the majority of formal users are running applications (“apps”) targeted for specific verification problems. Further, many of these apps, notably connectivity checking, are being run at the full-chip level on very large designs. We’d like to use this month’s post to explore the links between these two extremes, looking at what has changed and what is likely to happen going forward.

Let’s acknowledge that the traditional view of formal verification is rooted in reality. Formal techniques exhaustively analyze all possible behavior for the design being verified. This stands in sharp contrast to simulation, which exercises only a tiny fraction of possible behavior by running specific tests. If no test triggers a design bug, the bug will not be found. If the bug is triggered but no change in results is observed, the bug will not be found. Given a sufficiently robust set of properties to describe intended behavior, formal tools can not only find all bugs but also prove that there are no more bugs to be found.

Analyzing all possible behavior is a mathematically complex problem. The number of possible states for even a small design is far more than the number of atoms in the universe. Formal algorithms don’t consider these states one by one, unlike simulation. However, the larger the design the more analysis is needed. Sequential depth is also a factor in complexity. There are regular breakthroughs in the power and performance of formal algorithms, so users now run on large blocks and clusters unimaginable just a few years ago.

Other factors have also fostered wider adoption of formal verification. The broad deployment of standardized description formats, especially the SystemVerilog Assertions (SVA) subset, has reduced the level of expertise needed to write formal properties. It is now possible to flag by model-based mutation coverage those parts of the design not covered by assertions. Formal tools now have more automation and simulation-like debug features, also enabling use by design and verification engineers who are not formal experts. However, it remains rare for entire chip designs to be completely verified formally.

In contrast, many formal apps are routinely run at the full-chip level. About 15 years ago, EDA tool developers began applying formal techniques to specific verification problems. The goal remained finding all bugs and proving that all bugs had been found, but only those bugs related to the problem being addressed. Connectivity checking is a verification challenge that is addressed very well by a formal app.

Analyzing clock domains and power domains are two other verification tasks also amenable to an app solution. All three of these apps must be run on the full chip, since it is only at this level that all design information is available. Running on the complete chip is possible since only a small portion of the design is relevant to the problem at hand. Unrelated logic is trimmed away while building the formal model to speed analysis.

Connectivity has proven to be a particularly popular app because a modern SoC contains complex subsystems built with thousands of instances of highly configurable modules and IP blocks. Programmable elements provide flexibility and adaptability, while multiplexed I/O pads allow user control of which protocols run on which pins. A connectivity-checking app automatically ensures that the design meets the connectivity specification, which can be defined using simple tables in a spreadsheet. This specification shows all desired connections, including any gating conditions or delays (register levels) on the paths. The app finds any design errors and, once these are fixed, proves that the design matches the specification.

We are now seeing that ever-increasing chip size and complexity is making formal apps even more valuable, especially connectivity checking. Multi-billion gate SoCs may have tens of thousands of module instantiations and more than one-million complex connections that need to be verified. There is no chance that simulation or manual techniques will suffice. We view connectivity checking as an ideal application of formal verification. We continue to invest in it to ensure that we can handle the biggest designs in the world. It took a couple of decades for formal verification to achieve mainstream status, and we certainly do not want to lose ground now.