Do Graph-Based Scenario Models Qualify as Formal?

Recently on this blog, a series of related posts from Breker, Jasper, and OneSpin discussed formal analysis and its potential for playing a greater role in the verification process. We think that it’s important for The Breker Trekker to address topics in verification beyond our own technology and to provide occasional commentary on technology and the world of EDA in general. However, this recent focus on formal has caused some readers to wonder whether we consider ourselves to be in the formal market.

The short answer is “no” but there is some overlap in the technologies that we use and the techniques employed for formal analysis. Regular readers know that the foundation for our products is a graph-based scenario model that captures both the intended behavior of your SoC design and your system-level test plan. We can automatically extract system coverage from this model, with the model and coverage interacting in interesting ways. Let’s consider to what extent this is formal technology.

For a start, it’s perfectly valid to refer to a graph as a formalism or even as a formal model. You create the scenario graph using a simple C/C++ syntax and a precise set of rules that make it possible for our “solver” to traverse the graph efficiently and completely. You can also specify constraints to trim off portions of the graph for areas of the design not ready for verification or to bias our solver down certain paths rather than others as we generate test cases  from the graph.

The words “solver” and “constraints” are common to formal analysis and graph-based verification. This is where things can get a bit confusing. You might hear these two terms and assume that Breker somehow proves assertions on the graph or about the graph. This is not the case. You may keep existing assertions active during simulation or emulation of the Breker-generated test cases but we do not interact directly with them.

Further, there is no notion of proof of correctness in graph-based verification. We do not generate proofs that assertions or other forms of checkers can never be violated. However, as part of our system coverage we can analyze a graph and report the nodes that are unreachable. This is very valuable since it helps you determine when over-constraining has trimmed off parts of the graph that should have remained active.

Formal analysis can also report that certain types of coverage points are unreachable, typically code coverage and assertion coverage, perhaps with some simple forms of functional coverage as well. This is analogous to graph node reachability in some ways, and when people use the phrase “provably unreachable” the line between formal and graphics gets blurry indeed.

But the basics remain different. Our solver walks the graph in order to generate test bases to compile and run in the SoC’s embedded processors. We don’t prove correctness but we can generate an arbitrarily large set of test cases to verify for correctness. As we have discussed in an earlier post, we begin with the end in mind so we know with 100% confidence that each test case we generate will exercise the path we intended.

We provide system-level path coverage so than you know precisely which realistic use cases have been exercised and which have not. Formal provides no intrinsic form of coverage although you can derive some metrics by knowing how much of the design is covered by the assertions that have been proven.

Finally, one of the key strengths of a graph is that it is a compact representation that can be analyzed thoroughly. There is no practical limit to the size of design that can be represented in a graph: 10³⁰⁰ paths are not uncommon for a complete SoC scenario model. This presents no challenge to our solver; we can easily find unreachable nodes and generate as many test cases as you have time and resources to run. Since TrekSoC-Si generates test cases for hardware platforms, it’s fair to say that we have even more verification capacity than simulation.

Although formal’s advocates have argued strongly for its ability to eventually displace most simulation, today formal analysis has capacity limitations. Proving 100% of the assertions on a full SoC remains a challenge except for a few particular applications.

The bottom line is that formal and graphs do have some overlapping terminology and technology, but are really addressing different aspects of the verification problem. We do not consider ourselves competitors of formal EDA vendors, and would like to thank Jasper and OneSpin again for their guest posts and the lively debate they’ve generated.

Tom A.

The truth is out there … sometimes it’s in a blog.

Please visit us today at www.brekersystems.com

Tags: Breker, EDA, emulation, formal analysis, functional verification, graph, jasper, OneSpin, scenario model, simulation, system coverage, test generation, TrekSoC, TrekSoC-Si, use cases

This entry was posted on Tuesday, January 21st, 2014 at 5:52 pm. You can follow any responses to this entry through the RSS 2.0 feed. You can leave a response, or trackback from your own site.