Formal Verification, by Everyone and for Everyone

You might still be skeptical of the idea that formal verification can be used by everyone. After all, there is a deep-rooted perception in the industry that formal verification is for the elite few formal experts with Ph.Ds.

This might have been true in the early days of formal technology. The formal tools’ capacity was limited and the use model was not mature. So the aid of someone who actually understood the algorithms “under the hood” was important to help the tool solve the tasks at hand.

However, things have changed dramatically in the last decade. Formal technology has evolved such that formal tools can solve more problems, and more easily than before. At the same time, formal methodology has been developed so that formal can truly be used by anyone eager to learn new things. Formal Ph.Ds are still desirable in EDA R&D teams, but they are no longer required on the application side.

Formal technology has been used in four distinct use-models today, namely automatic formal, formal apps, assertion-based verification and End-to-End formal, as shown in the picture below.

Oski is bullish on expanding the understanding of the pyramid so verification engineers can implement End-to-End formal technologies and methodologies to accomplish their verification goals.

It is easy to understand how anybody can use automatic formal, or formal apps. But when it comes to End-to-End formal, where formal verification can be used to replace simulation and achieve sign-off, questions arise: Can everyone learn to do End-to-End formal verification? Doesn’t that require experience and knowledge both in design and formal verification?

As a dedicated formal verification services company, Oski is proof that End-to-End formal can be learned and used by everyone. Every day our team of formal engineers works on many active customer projects, finding corner-case bugs, achieving sign-off. These engineers don’t have Ph.Ds and some are fresh graduates from college with no previous experience in formal or design. Yet through our internal trainings and working on real world problems, they learn and become formal experts, in time.

The key to their successes relies on two facts:

1.     With a systematic formal sign-off methodology, they learn how to apply End-to-End formal in a predictable and systematic manner. There are processes to follow, so they know what to do.

2.     They benefit from the critical mass of formal expertise we have in-house. Having somebody experienced to guide them, especially in the early days of the training, is critically important. One can probably learn how to use a formal tool, but that doesn’t mean one can learn how to use formal effectively to solve real problems. The latter benefits a great deal from working with someone who knows how.

Today, the benefit of formal is fairly easy to understand. Obviously, companies pushing the limit and designing large, complex SoCs need all the tools at their disposal to solve the verification challenges we face today. Formal helps by catching corner-case bugs that are hard to find using simulation, and provides exhaustive proofs to establish correctness of the design. For IP companies, using formal to verify configurable IPs offers assurances that the IP will work correctly under all possible configurations. Even for companies that are doing smaller designs where current simulation-based methodology may seem sufficient, formal can improve verification efficiency and productivity, as some design blocks are better suited for formal than simulation.

On Sept 23, Oski CEO Vigyan Singhal will join Anders Nordstrom from Synopsys to deliver a tutorial on the topic of “From Formal Apps to End-to-End Formal Verification – Formal Analysis for Everyone” at Synopsys User Group (SNUG) in Austin, TX. In the tutorial, Vigyan will discuss what End-to-End formal is, and how End-to-End formal can achieve formal sign-off, by everyone and for everyone.  Hope to see you there!