InFormal Chat


SNUG Silicon Valley 2019: Formal Verification Update

Like last year, we had number of papers presented at our annual SNUG event last month. We had a track dedicated to formal verification, which had 3 papers from customers and 1 tutorial from Synopsys. In a parallel track on AI/ML, we had an additional tutorial from Synopsys where we discussed how formal is best suited to make use of machine learning techniques.

Coming back to the formal verification track, Qualcomm presented a paper on how reset and clock related issues contribute to a significant number of design issues. We all know static verification is best suited for finding clock and reset issues, but here presenters talked about why reset connectivity itself is critical to IP based designs and how formal is best suited to check reset connectivity issues.

Broadcom extended the discussion with a presentation on connectivity checking, which talked about how connectivity checking can be scaled up for a SoC design and how coverage can be leveraged for connectivity checking signoff. Coverage is becoming essential to formal verification because tracking and closing coverage provides the confidence engineers/project managers need to tape out the designs.

The third paper was presented by Palo Alto Networks and spanned formal usage from beginners to experts. The presenter started with how formal can be better explained to new users coming from a simulation background; what are the typical sweet spots for formal and how various formal apps can be used to address specific class of verification problems. In particular, how a formal testbench can be constructed to check legal behavior of the designs and find bugs which may not be possible to find with simulation or may take much more effort. To expand the discussion on formal property checking, the presenter also talked about various abstraction techniques that can be used to improve convergence and accelerate performance. In the end, there were pointers to verification metrics that can be used for formal signoff. This presentation had something for everyone, folks who are starting with formal as well folks who want to maximize the ROI on formal efforts.

This year’s Synopsys tutorial talked about why formal regressions is a good idea, as well as the key considerations that should be kept in mind when setting up formal regressions, which included a brief discussion on formal apps best suited for regression, various formal verification metrics etc. ROI on formal regressions not only requires optimum use of compute resources but also methods/mechanism to store and track progress. VC Formal provides the infrastructure and technologies to setup the regressions, store and track progress and on top of everything it provides ML technologies to accelerate the regression runs.

I would like to take this opportunity to thank all presenters for taking the time out to share their experiences and the attendees that make SNUG a huge success.

For SNUG proceedings, please visit HERE or reach out to your Synopsys contact.

Share and Enjoy:
  • Digg
  • Facebook
  • Google Bookmarks
  • LinkedIn
  • Twitter