There’s little doubt that adopters of formal verification have reaped benefits from their efforts. Those who have taken the plunge consistently report that assertion-based verification translates into gains in both productivity and quality.
But there’s a catch, as those same adopters of formal will readily admit: Formal verification requires quite a bit of know-how to really take advantage of it. The lack of that know-how has stymied a lot of would-be adopters over the years.
To ease the path to full adoption of formal techniques, OneSpin Solutions has come up with a step-by-step approach to comprehensive assertion-based formal verification. With six different levels of adoption, OneSpin’s offerings provide graduated entry points into formal verification that match various levels of proficiency (see the figure).
The bare-bones approach to formal is to simply apply automatic checking, or autochecks, which requires no expertise in formal verification whatsoever. It’s the easiest application of formal and requires no expertise. The tool simply extracts the assertions from the design and exhaustively verifies them. Autochecking requires no testbench, yet still performs exhaustive verification of many checks. It can be performed as soon as there is register transfer level (RTL) code for a functional block.
A second level is verification of implementation intent. For this level, the user must write simple SystemVerilog assertions to check microarchitecture or implementation aspects of the design. Here, one can check for simple implementation aspects, such as ensuring that signals rise or fall in relation to one another in proper fashion. Again, no testbench is needed. The sweet spot for this level of formal checking is verification of block-to-block connectivity.
Next is the functional requirements level, where the focus is on specification compliance. This level calls for a bit more expertise from users, who must write more complex assertions to capture functional requirements expressed in the specification. These are verified exhaustively with formal techniques. At this level, the user can find deep bugs within the design that are difficult to pin down otherwise.
At the fourth level are design operations. An example of formally verifying for design operations might involve a cache controller; the user writes assertions that describe the intended behavior of the read and write operations. Verifying all operations in this manner is a highly efficient functional verification strategy and can reduce or eliminate the need for module or subsystem-level testbenches.
A fifth level of formal verification available from OneSpin is automatic gap detection, which allows users to automatically find input scenarios not yet specified by any assertions. In the foregoing example of a cache controller, if there were no assertion describing what happens on a cache miss, the tool would discover that and automatically write an assertion for it. This allows a further increase in the quality of overall verification. Automatic gap detection turns up and corrects coverage gaps that are elusive in simulation using coverage data. It’s worth noting that these gaps are also hard to turn up using traditional formal methods; it’s one thing to have a set of assertions, but it’s another to know how good they really are.
The sixth and final level is what OneSpin terms “gap-free” verification. This implementation of formal verification guides the user all the way through verification planning, execution, and application of a whole set of gap-detection checks. These checks not only determine that all possible input scenarios have been described in the assertions, but also that all possible outputs have been described in the assertions.
Some would-be adopters of formal are frightened off by the prospect of writing SystemVerilog assertions. Actually, writing them isn’t so difficult, but writing them so they hold in simulation can sometimes be challenging. Sometimes the assertion has errors, and sometimes the design. Which is it? To address this aspect of successful adoption of formal techniques, OneSpin has developed a proof-based assertion debugger that can help find the root cause of assertions that fail to trigger properly.
These six entry/exit points for formal verification map to OneSpin’s 360 MV product family, which ranges in price from $20,000 for the 360 MV Inspect tool, corresponding to the auto-checking level of formal analysis, to $180,000 for the fully loaded 360 MV Certify product.
OneSpin Solutions GmbH