OneSpin creates debugging environment for formal verification tool

It seems as if every advance in verification technology begets a new problem. A case in point, according to OneSpin Solutions director of product marketing Michael Siegel, is the growing use of assertion-based formal verification. As engineers become more comfortable writing assertions, they naturally write more complex ones. And as the assertions grow more complex, engineers turn to hierarchical organization to speed and simplify the job of creating the assertion set. Hierarchy is wonderful, avoiding redundant work in creating the set, reducing the chance of errors, and improving reusability.

But hierarchy also makes the assertions much more difficult to debug. The problem comes, Siegel said, when the formal analysis tool finds a counterexample to an assertion. "The counterexample isn’t the end of verification," Siegel said, "it’s the start of debugging. Is the problem an error in the assertion, or an error in the design itself, or is it perhaps a missing constraint that allowed the tool to examine an inappropriate range of input conditions? With simple assertions, you can often look at the assertion and see what happened. But with complex, hierarchical assertions, you simply can’t tell by looking at the top-level code."

Unfortunately, the information you need to look below the surface isn’t usually sitting there in front of you on the screen. A text display can only list a possible sequence of states that violates the assertion—not exactly what went wrong or, more importantly, why. To learn more, engineers must have additional information. What did this failur look like in the time domain? Exactly which root clause in the assertion was violated? What line of the RTL code did the violating? And if all else fails, the engineer must return to the time domain: what do the waveforms look like on the logic cone fanning into the violating signal?

OneSpin today introduced a new tool package to answer these three questions. RootCauseAnalyzer—right up there for longest unpunctuated product name of the year—works with the more complex levels of OneSpin’s tool suite to dig out the causes behind the counterexamples.

For the three kinds of information the engineer needs, RootCause provides four tools. The first, WaveformAnalyzer, presents the counterexample as a waveform instead of a text display, showing the state variables in the clock cycles leading up to the counterexample. The second, StructuralAssertionAnalyzer, traces back through the assertion source-code, with hierarchy if necessary, to identify the specific clause in the assertion that was violated and show the values associated with objects defined in the clause at the point of violation. So rather than knowing that a bus read cycle failed to perform the proper bus-release sequence somehow, you know the sequence of events in the bus handshake that occurred out of order.

The third tool, ActiveCodeAnalyzer, digs into your RTL source instead of your assertion source. It shows what RTL code was active at the point in state space where the counterexample occurred, and lets you manually step through clock cycles to explore the behavior of the code and variables in the region of the problem. Finally, the fourth component looks not at the code space but at the signal cones. TemporalFaninAnalyzer examines the variables in the logic cone leading to the failure and shows you the signal dependencies, in time and logic hierarchy, leading to the point of failure.

The result, according to Siegel, is an enormous reduction in debug time. Rather than simply proving that once again your design didn’t work, RootCauseAnalyzer provides in-depth views into the guts of the design so you can explore what the design actually did do, and why it produced a counterexample. As a bridge between the obscure, timeless, state-space world of formal analysis, the software-like world of RTL, and the concrete reality of cycle-accurate waveforms, the new toolset lets designers turn the problem over in their minds until they see into the solution. It is a significant step across the gap between how mathematicians visualize designs and how engineers actually work.