Synopsys held their first VC Formal Special Interest Group (SIG) event in Israel on February 18. The meeting was attended by over 55 engineers, both current Formal users, and those interested in learning about how Formal Verification can contribute to their projects.
The event opened with an academic lecture by Prof. Orna Grumberg from the Technion, on “Automated Program Repair”, and included different tutorials by Synopsys staff, on Datapath Verification, Formal Signoff and Security Verification.
Additionally, the event featured 3 use cases of how different companies introduced Formal into their verification flow. What makes these 3 cases interesting, in our view, is that they beautifully demonstrate the methods that companies have used to introduce the new technology into their processes, each using a different paradigm:
Yael Tenne, Formal Verification Team Leader at Xsight Labs, a stealth-mode startup, presented “The good, the bad and the ugly…” in Formal Verification. Yael did a great job reviewing the best practices on how to add Formal as “part of a verification puzzle” and how to work with other dynamic verification and design engineers to achieve the best results. It’s worth mentioning that she has over 20 years of experience in the field at very “Formal-oriented” companies – Marvell, Mellanox, and Intel.
Apparently, Xsight Labs management already recognized the benefits of the new technology from start. Thus, they invited Yael to join the company from the beginning and make Formal an integral part of the flow. This was the first user paradigm.
Asi Lifshitz, a senior verification engineer at Microsoft, showcased a second model: He and his team didn’t previously have a positive experience with Formal – in fact he had an unsuccessful evaluation 10 years ago! But they decided it’s the right time to try getting their feet wet again.
They had a very privileged setup: he emphasized the point that Microsoft is a rich company with plenty of EDA licenses, and that another group in Microsoft had just finished a big project, freeing up lots of VC Formal licenses.
Furthermore, his own group was in-between projects, so they had the time to go into a systematic evaluation process, that started with bringing in a Synopsys expert for a few days of training, and then involved taking a block that had already been verified in a previous project and re-verifying it “Formally”, with close support of a Synopsys expert.
Asi’s great presentation, featuring clips from blockbuster movies such as “Pulp Fiction”, “The Big Lebowski” and “Braveheart”, made a very compelling point of how to “most properly” introduce a new technology to your flow – and that indeed might be the best way if you have the time and resources available to do so.
However, two seasoned verification managers sitting at my table – one from an Israeli branch of a multinational giant and another at a mid-size Israeli company – shook their heads saying that they would never have the time to dedicate to such a lengthy process, let alone have the courage to ask their management for licenses before having justified to themselves that the technology would work for them.
Finally, Elchanan Rappaport, our own Formal Verification Lead at Veriest, discussed his experience introducing Formal Verification as a consultant to a start-up customer. Elchanan presented “A day in the life of the Formal Verification engineer”, paraphrasing the famous Beatles song. He told the story of his first day at that client, all the way from starting to write some properties about a protocol not documented well-enough (that happens, not only at startups), all the way to finding a very real and deep bug by the end of the same day.
In my view, this represents a third paradigm, where the customer didn’t have the bandwidth to learn the new methodology during the very aggressive time schedule of his project, but still wanted to benefit from the additional layer of verification enabled by formal and the speed with which one can get results – as exemplified by the “A day in the life” experience. Also, the customer could see the results before making major investments in staff, licenses and learning-curve. Moreover, when this project is complete, the company will have a production flow that includes Formal, as well as reference Formal IP, besides having leveraged Formal benefits throughout the project.
As a general note, I would say that Formal Verification still suffers from the image of something ultra-hard, that require some PhDs in Math to understand and use it. In fact, in a recent panel of Verification experts hosted by Veriest, one seasoned manager said he’s most scared about Formal Verification!
But with the advancement of the tools and availability of easy to use Formal apps, along with mounting evidence about the benefits of this methodology, one should at least consider including it in its arsenal of verification technologies. And depending on your company profile, one of the three models reviewed above can certainly help you achieve your goal. After all, as Benjamin Franklin once said,
“An investment in knowledge pays the best interest.”