Based on more than 250 engineer-years of development, a formal verification tool purports to detect all functional errors in complex digital IP blocks. The tool, 360 Module Verifier (360 MV), is the initial product from Munich-based startup OneSpin Solutions, a spinoff built around Infineon’s verification group. Aimed at block-level formal verification as opposed to full-chip signoff, 360 MV verifies peripherals, processors, and subsystems with up to a few hundred thousand lines of RTL code.
The tool requires no change to established design flows and smoothly integrates into chip-level functional simulation. It enables verification engineers to verify functional compliance between the transaction and register-transfer levels to produce the extreme quality needed for risk-free reuse of IP components, especially processor cores. Its rigorous, automatically checked termination criterion eliminates the time-consuming and expensive regression testing that merely estimates achieved quality levels. Using IP verified with OneSpin’s “true functional sign-off” methodology, SoC design teams can proceed to chip integration and chip-level functional simulation knowing that the individual modules are free of functional errors.
The goal of verification is to drive errors to the functional module’s output, where they can be observed. There’s three ways in which bugs in RTL code escape detection. One way is when the set of test vectors that’s used to exercise the design fails to find the errors, i.e. unstimulated errors. Formal verification, in and of itself, closes this hole by applying all possible test vectors at the input to the design. So let’s assume that formal verification succeeds in driving all errors to the output where they can be observed. In typical verification flows, small code blocks called monitors observe the output to watch for unexpected behaviors. But an incomplete set of monitors can let errors slip through undetected. 360 MV closes this loophole by guaranteeing that it will furnish a complete set of monitors with which to observe the output. That’s the second way in which bugs get away from verification engineers.
Now, what happens if all bugs are driven to the output, and there are monitors there to pick them off, but they still are not recognized as errors? All too often, the engineer who wrote a given section of RTL code is also the same engineer who wrote the monitor. Perhaps he misunderstood or misinterpreted the functional specification for the IP block in the same way twice. As a result, the error is masked; the monitor repeats the same error as the RTL. These are known as “faulty accepted errors.” The only way to catch such errors is by invoking the functional specification. 360 MV achieves this by raising the level of abstraction of the monitors to the same level as the functional specification, which usually is expressed at the transaction level. By doing so, the tool is able to compare what the monitor should do to what the specification should do.
The only catch here is the assumption that the functional specification itself is correct. But by comparing the specification to the RTL code written to express it, 360 MV often turns up instances in which part of the code has not been described by the specification. It also finds instances in which behavior is described ambiguously in the specification, or even incorrectly.
360 MV is available now. A one-year license costs 175,000 Euros ($222,655 as of May 7).
OneSpin Solutions
www.onespin-solutions.com