The Breker Trekker
Tom Anderson, VP of Marketing
Tom Anderson is vice president of Marketing for Breker Verification Systems. He previously served as Product Management Group Director for Advanced Verification Solutions at Cadence, Technical Marketing Director in the Verification Group at Synopsys and Vice President of Applications Engineering at … More »
Beginning with the End in Mind: Graphs and Formal
June 30th, 2014 by Tom Anderson, VP of Marketing
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:
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!
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