Beginning with the End in Mind: Graphs and Formal

I’ve written about formal analysis rather frequently in this blog, although I do not consider Breker’s products to be formal in nature. There are several reasons for this. After ten years working with formal tools, I remain personally interested in that market. I also see interesting parallels between the adoption of formal and graph-based technologies. Further, whenever we cover formal analysis we get a great response. Clearly our readers like the topic as well.

I’m returning to formal this week because of a provocative comment made by one of our customers at DAC a few weeks ago. Wolfgang Roesner from IBM participated on the show floor in a Pavilion Panel called “The Asymptote of Verification.” Among several astute observations about the attributes of graph-based scenario models, he made a comparison with formal analysis that I found especially perceptive.

Wolfgang described how a graph improves on constrained-random stimulus by starting with the desired goal and tracing back through the graph the path necessary to achieve that goal. The test case, which is guaranteed to hit the goal, is simply the reverse of this path, starting with the appropriate input conditions. Although I don’t recall him using the exact words, this is what we have called “beginning with the end in mind” for several years now.

Wolfgang’s insight is that this process is conceptually similar to formal analysis, which also starts with a goal, either an assertion that should never be violated or a coverage target that should be hit. Formal traces backward through the design to construct a path to hit the goal or proves that the goal cannot be reached. This sets up a simple and instructive comparison between the two technologies:

• Formal assertion: engine either generates a “counter-example” trace showing how the assertion can be triggered or proves that it can never be triggered
• Formal coverage: engine either generates a trace showing how the coverage point/group/cross can be reached or proves that it is unreachable
• Graph coverage: engine either generates a trace showing how the coverage goal/path/cross can be reached or proves that it is unreachable

There are some important differences as well. Formal analysis traces the actual design, so it requires the RTL to be complete or nearly so and it has capacity limitations. Analyzing only the scenario model allows graph-based verification to handle designs of arbitrary size and complexity. Graphs target high-level system coverage that reflects actual end-to-end use cases. Formal typical operates on design-level coverage or even code coverage.

The panel on which Wolfgang appeared was specifically arranged to compare and contrast static verification, formal analysis, and graph-based verification. Everyone verification team uses static techniques, even if only linting, and formal is becoming mainstream. Graphs are still somewhat of a specialty technology, but part of Wolfgang’s argument is that they’re easy to understand since people are already used to formal tracing backward from goal to inputs.

I found this to be a valid point, and another indication that graph-based verification is no longer regarded as an exotic technology. In fact, I think that graphs are easier to build and use than many of the complex assertions design and verification engineers write for formal analysis. With Accellera already looking at standardization, I believe that it’s just a matter of time before scenario models are in the flow for most if not all SoC projects.

I’m working on some other ways to visualize the unique properties of graphs and will share them in future posts as they coalesce. Please stay tuned!

Tom A.

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

Tags: Accellera, assertions, Breker, coverage, EDA, formal, functional verification, graph, mentor, portable stimulus, pwg, reuse, scenario model, SoC verification, standards, test generation, working group

This entry was posted on Monday, June 30th, 2014 at 2:46 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.