Open side-bar Menu
 The Breker Trekker
Tom Anderson, VP of Marketing
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:

  • 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.

Related posts:

Tags: , , , , , , , , , , , , , , , ,

Leave a Reply

Your email address will not be published. Required fields are marked *


You may use these HTML tags and attributes: <a href="" title=""> <abbr title=""> <acronym title=""> <b> <blockquote cite=""> <cite> <code> <del datetime=""> <em> <i> <q cite=""> <strike> <strong>

S2C: FPGA Base prototyping- Download white paper

Internet Business Systems © 2016 Internet Business Systems, Inc.
595 Millich Dr., Suite 216, Campbell, CA 95008
+1 (408)-337-6870 — Contact Us, or visit our other sites:
TechJobsCafe - Technical Jobs and Resumes EDACafe - Electronic Design Automation GISCafe - Geographical Information Services  MCADCafe - Mechanical Design and Engineering ShareCG - Share Computer Graphic (CG) Animation, 3D Art and 3D Models
  Privacy Policy