Formal verification in five easy lessons
Up until a few years ago, formal verification still consisted mostly of model checking with hand-coded properties, and thus was primarily used by academics or highly trained specialists at a few of the largest semiconductor companies.
Today there are several new automatic approaches requiring much less manual setup. Adoption of these approaches is fast moving formal verification from a narrow niche to the mainstream.
This is my list of the top five formal applications in the industry (listed in order of least to most used).
#5. Connectivity Checking
Today’s SoC designs contain large numbers of design IP blocks interconnected through multiple on-chip bus fabrics and thousands of point-to-point connections.
Using dynamic simulation to validate these design assemblies involves the time consuming task of developing directed tests to toggle all the top level design signals, as well as the tedious debugging process to determine why signal values did not transition or propagate as expected.
On the other hand, formal tools can be employed to automatically highlight the areas where the expected connectivity behaviour doesn’t hold true while providing a much faster route to debug any problems.
A complete property set describing system-on-chip (SoC) interconnections can be automatically extracted from a specification that details the design assembly requirements. In most cases this specification is already pre-existing, so the required effort is minimal.
#4. X-state Verification
The synthesis interpretation of X as don’t care can result in silicon that behaves differently than observed in RTL simulation, where X is interpreted as unknown.
The unknown RTL simulation semantics of X has two often discussed pitfalls: x-pessimism and x-optimism. X-optimism is the most worrisome as it can mask true design behaviour by propagating a deterministic value through the design, when in reality various possible values will be seen in silicon. Due to power and area constraints, not all storage elements in a design can be reset directly. Hence, X-states are expected to exist in the design during the initialization phase.
Moreover, X-states can arise in RTL simulation due to a number of other events, such as bus driver value conflicts, out of range indexing and activation of an explicit X-state assignment.
The benefits of a formal approach are two-fold. Firstly, formal can automatically pinpoint the sources of X-states in the design that may have otherwise been masked by X-optimism in RTL simulation.
Secondly, it can exhaustively evaluate all possible design behaviors to determine if X-states can be propagated to corrupt known values. Properties to check for X-state propagation to storage elements or design outputs can be generated automatically, making the setup effort for this process very minimal.
#3. Code Coverage Closure
According to a 2012 study of functional verification by Wilson Research Group and Mentor Graphics, code coverage is a metric used by 70% of today’s project teams with the goal of providing a clear, quantitative, objective measure for assessing their progress towards completeness. Designers do not have to instrument their code with coverage collectors, as these are automatically generated in simulation.
Thus, coverage results can be obtained with low effort, but interpreting those results and achieving closure is a lengthy process that involves a lot of manual intervention. Each uncovered point in the code must be reviewed to determine if it is safe to ignore or if the test environment must be enhanced to cover it, typically through writing directed tests.
Due to design reuse, not all IP block modes or functions are expected to be covered. In addition, certain coding styles lead to branches of code that are never expected to be traversed. Formal analysis can find and report these unreachable goals and improve the accuracy of the code coverage metrics.
It can demonstrate how to hit the reachable ones, and in so doing, provide a guide for the process of generating additional tests to cover them in simulation. As with simulation, formal infers the coverage targets automatically from the code, so there is very little effort required to get started.
#2. Automatic Formal
Here’s a question that verification engineers tasked with model checking have asked for years – what if the properties for commonly occurring RTL functions could be automatically generated? Well, that’s precisely what automatic formal tools do.
Such tools automatically generate properties for RTL elements such as registers, FSMs and memories. Then, they find a variety of issues such as counter overflow, FSM deadlock and out of range memory addressing.
Simulation debug can be very costly in terms of time and engineering resources. Filtering out a whole class of bugs that can be found through automatic formal verification before simulation saves time.
#1. Clock-Domain Crossing Verification
It is not uncommon to find designs with hundreds of asynchronous clocks and tens of thousands of CDC signals.
As data moves through the device, it must be safely transferred across the clock domain boundaries. RTL simulation does not model the silicon behaviour of CDC signals.
However, automated CDC tools make it easy to use static analysis to perform comprehensive CDC verification.
CDC tools use static analysis to find all the clock domains and clock domain crossing signals and check for correct synchronization of those signals. They alert the designer to missing synchronisers as well as occurrences of synchronisers with errors, such as glitch generating combinational logic that drives a synchronizer input.
They also report topological CDC issues such as redundant synchronization and divergence/reconvergence of synchroniser signals.
Formal verification is ascendant. Better tools are making it easier all the time to abstract away the complexity of the technique and a wealth of resources exist to help you get started. If you haven’t considered formal verification lately as complement to traditional verification methods and a means to accelerate verification closure, it’s time to do so.
Roger Sabbagh is a Mentor Graphics product manager specialising in formal-based technologies.
I suggest you might start by following the blog of Harry Foster, Mentor Graphics chief verification scientist and resident formal expert.
Tags: automatic approaches, interconnections, narrow niche, state verification