Jasper, OneSpin seek broader audience for formal verification tools
Not just for verification experts anymore: New tools try to attract designers at early stages of the design process.
By Ron Wilson, Executive Editor -- EDN, January 21, 2009
Formal property-checking tools—EDA tools that mathematically determine the truth of a set of properties for a given design in order to prove that a design will do what the designer intended—are reaching out for a wider market. Two announcements Monday, one by Jasper Design Automation and another by OneSpin Solutions, show the different ways in which vendors of these tools are striving to create more seats.
Initially seen as almost an academic curiosity by many verification engineers, formal tools have earned a valuable place in the verification flow for many design teams. The tools can state definitively, without using simulation or test vectors, whether a particular property is true—and if it is false what the counterexamples are—for a given block of digital RTL. Ideally, then, the design team would only have to establish a complete set of properties to cover the design requirements for a block and then use a formal tool to prove that the block meets the properties. This would be a sufficient proof of correctness for the entire block, and would eliminate the need for any further verification of the block, giving 100% functional coverage.
But limitations in the tools and the unfamiliarity of the theory have both hampered the widespread adoption of formal techniques. Early on, the tools, even when working correctly, presented such daunting user interfaces that it's only a slight exaggeration to say that the tool designers themselves were the only people who could use them effectively. Tool suppliers have been working hard on the user interface, making it less dependent on a PhD in mathematical logic and more accommodating of the way digital designers think, even adding such utilities as waveform input.
The tools are also limited in their capacity. "Even the tools with the best capacity are targeted for modules, or in some cases subsystems, not for a whole chip design," explained Michael Siegel, director of product marketing at OneSpin. Adding more complexity to the problem, the capacity of the tools is not a clear function of the amount of code or the apparent complexity of the block, but rather of the size of the state space that the tool must analyze. "These tools are most useful for structures in which the tool is not going to be chewing on the whole state space," said Kathryn Kranen, CEO of Jasper. "Most of the time there are better ways to verify a mathematical function block, for example."
The result has been that formal property-checkers have become invaluable, but at very specific points in the design. Many teams would not think of declaring a cache controller, interrupt controller or bus arbiter ready without formal analysis, for example. But few would attempt to use the tools on a DSP multiply-accumulator. And for the most part, formal tools today find use at specific points in the verification flow, by a few experts, with specific sets of properties chosen to cover gaps the verification coverage left by simulation of specific blocks. Deriving properties from design requirements has never been easy, obvious, or automated.
This niche is an important one in the industry, but vendors say it understates the real utility of formal tools. Their argument is not that the tools should be used for a wider range of blocks, but that they can be valuable to a wider range of team members, and not solely for increasing verification coverage. Both Jasper and OneSpin are now backing up these claims with major new products.
Five easy pieces
The more sweeping of the two announcements comes from OneSpin, which has introduced a new tool suite in five distinct pieces. The pieces are graded in their demands on the user and their place in the design flow, ranging from tools for use by formal-tool novices early in the code-generation process to tools intended for seasoned verification managers during the verification-closure process. The entire suite goes under the name 360 MV.
The first level in OneSpin's program is called MV Inspect. This set of tools uses a preprocessor to scan the user's RTL and identify properties implied by the code, from a predefined library of checks. For example, the preprocessor might assert that a block of code can be reached, or that a signal will eventually toggle. These properties MV Inspect then proceeds to verify. "This is a step beyond a syntactic analysis like lint," Siegel explained. "We are inspecting the properties of the code, not its syntactic correctness or completeness. But we do not require the user to write any assertions, or even know how to write assertions." The point is to catch obvious errors—things that are clearly wrong without even referring to the design intent—early, with a simple, automatic tool.
At the next level, MV Check, OneSpin checks the intent, rather than the structure, of the RTL. For this step, the designer—and this would normally be the block designer, not a member of the verification team—writes simple assertions in OVL, SystemVerilog, OneSpin's property language, or simply using VHDL Assert statements. These are not compound-complex, page-long dissertations, but simple statements about how the RTL must function, covering such issues as the integrity of data types and functional sequences of events. MV Check then validates these assertions formally against the RTL. "This is not so much a verification step as it is a sanity check for the designer," Siegel said.
In these first two steps, the tools have been simplified and streamlined for use by the design engineers. The idea has been to filter out errors that could be caught early, before the RTL moves into verification. But at the third level, MV Verify, the game gets serious. "At this level, more experienced verification engineers write the more involved assertions that they derive from the design requirements," Siegel said.
These assertions are too complex for something like OVL, so the assumed language is now SystemVerilog. And the subject isn't simple checks, it is exhaustive descriptions of an arbitration protocol, an interrupt handler, or the like. Deriving such assertions from the design documents is a nontrivial exercise, Siegel admits. But he points out that other than a difference in orientation, it is not fundamentally more difficult than creating enough directed-random tests to cover the RTL.
Also at this level, verification engineers may drill down into the sequential operation of transactions and interfaces using a timing-diagram-input tool called a Design Operations checker. This process requires timing-level understanding of the design and some sophistication with formal verification, but it is assisted by a timing-diagram-assertion library OneSpin introduced at DAC last year.
The final two levels, MV Assure and MV Certify, are more intended to assure complete coverage of the block than to test properties. Assure's Automatic Gap Detection in essence makes assertions about the completeness of the assertions: testing whether there are input scenarios that have not been covered by the assertion set. Certify, with its Gap-Free Verification, adds the concept that not only have all input sequences been covered, but all outputs are completely specified. "You can show that if all the input sequences are covered and all the outputs are deterministic, the assertion set is sufficient to act as a gold reference for the design," Siegel said.
A vital additional tool in Certify acts as a proof-based debugger for assertions. "Often most of the effort in using a formal tool goes into manually figuring out why an assertion has failed," Siegel said. "This tool provides you with the temporal fan-in of the assertion—the events that proceeded the failure—and shows what specific part of the assertion failed. This can be an enormous time-saver in troubleshooting an assertion."
By splitting 360 MV into phases, OneSpin has reduced the learning necessary for any one level to about a one-day training program. You enter the levels at the point you need for your work and based on your skills, and learn the concepts one-by-one instead of being dumped into a new way of thinking, a new skill set, and three new languages. In this way, the company hopes to attract RTL designers to using the first two levels early in the design flow, and to attract more verification generalists to use the higher levels.
Waveforms and iterations
The announcement from Jasper also focuses on formal verification for designers, as opposed to verification experts. "RTL coding has always been iterative," argued Kranen. "Designers don't just sit down, write a perfect block and send it off to verification for approval. They write a block—often intending it only as a placeholder for use by the physical verification team—then they try it out, see where it's broken, and repair it.
"The problem with this iterative approach is that for many designers, the only tool they have to try out their new RTL is a full—or nearly complete—RTL test bench and time-consuming simulation. What we have with Behavioral Indexing is a waveform-based way for designers who are not experts in formal verification to quickly create properties and test them against the RTL so that they can continue to refine their code."
Behavioral Indexing works on the notion of a behavior as a temporal relationship between states in a timing diagram. To specify a behavior, you create a timing diagram, click on states and specify the necessary relationship between them—as in, "this data must appear more than 2 but less than 6 nanoseconds after this Ready edge"—and name the relationship. The tool then stores the behaviors—typically there may be hundreds of such relationships for a single block, Kranen said—and combines them with other known properties for the block.
Then the magic: Jasper's formal engine analyzes the RTL and shows as waveforms the conditions that are consistent with the specified behaviors. This may confirm your original thinking, it may show that the RTL is not doing what you wanted, or it may show that the RTL is doing something you did not want. Or, if you are having a particularly hard day, the tool will report that there is no way the RTL can produce the behaviors you have specified.
The package can also flag when a defined behavior is present in a waveform. Through these capabilities, the set of behaviors, together with predefined property sets from a library of standard bus behaviors, in effect becomes executable documentation for the block. The set also provides a clear list of things to check during a code review—vital to later reuse of the block as well as for getting design management off your back.
Going further, the Jasper tool provides implication analysis: testing the assertion that a particular change made to the code did not impact the defined behaviors. This capability can save enormous numbers of iterations of the "Now, how did what I just wrote break that over there?" sort, particularly when a designer is working on someone else's code.
In addition to extending the value of formal property-checking into the early stages of RTL creation, Behavioral Indexing may facilitate a very different attitude toward code generation. If you can quickly identify which behaviors your RTL is messing up, it doesn't make sense to spend a lot of time trying to perfect the code on the first pass. It may be much more productive to write a full block to a first-order approximation, get it to the rest of the team so they can see what the pins, size, and approximate performance are, and then start refining away on the areas that aren't working yet. Painful as it might be to purists, this may be an important approach to block design.
Another area—but one not directly discussed by either company in their presentations—is the increasing difficulty of adapting third-party IP into a new design. Inevitably, it turns out that "working" IP is working only in a slightly different context—not in the way you intend to use it. In fact it's never been tried with the input sequences you have in mind. The availability of formal property-checking tools for designers, rather than verification engineers, could potentially spot these incompatibilities in the IP almost as soon as you unwrap the package—assuming you license the RTL and not just encrypted data. This ability could have another major impact on overall design time.
