You don’t have to take my word for it: Machine Learning has a place in Formal Verification
Just over a year ago I wrote a blog about the impact of machine learning (ML) algorithms to boost Formal Verification performance . The data for that blog was firsthand experience on a set of complex benchmarks. The data was amazing and quite convincing, but when I wrote that blog the reader needed to “trust” me as the data could not be shared publicly.
I did hear from some with skepticism whether the ML data could *really* improve formal verification performance. After all, Formal Verification is an NP-C problem and last I checked no-one has won the millennium prize for solving the problem. Indeed, the use of ML does not break the complexity of the formal problem, but does allow the results to be reached much faster given the previous run information that is harvested. The most important part of this technology is that you don’t need mountains of data before you can see the benefit. We have many cases where even after the first run, there is an amazing boost in performance.
Now, after over a year, we have a customer on the record collaborating with my observation and confirming the amazing performance. On Aug 27th, 2018, ST and Synopsys announced a 10X performance in formal property verification with machine learning technology. Here is just an excerpt.
“The newly introduced VC Formal Regression Mode Accelerator app consistently delivered an order-of-magnitude performance improvement along with improved convergence of additional inconclusive properties for the most complex SystemVerilog Assertions on our design blocks, said David Vincenzoni, R&D Design Manager at STMicroelectronics.”
Thank you to those of you who didn’t dismiss my original blog. For those who want more information, please reach out to any of us in the VC Formal team at Synopsys. We will be more than happy to discuss this breakthrough technology.
