Bringing Formal Verification into Mainstream

Formal verification can provide a large productivity gain in discovering, analyzing, and debugging complex problems buried deep in a design, which may be suspected but not clearly visible or identifiable by other verification methods. However, use of formal verification methods hasn’t been common due to its perceived complexity and the expertise and effort required in preparing the design and testbench for formal verification. However, with growing design complexity formal verification is fast becoming an essential part of verification methodologies to catch those bugs prone to be missed by simulation or other verification engines even after a large number of cycles.

Not all designers or verification engineers have requisite expertise to prepare the design code for applying formal verification. A few expert engineers, who have acquired a good level of expertise about formal verification by using it over the years, are usually preoccupied with many other tasks and cannot be employed for the huge benefit formal verification can provide by applying it on large SoCs at the enterprise level. This results in ‘ad hoc’ formal verification by a few experts. The real potential of formal verification remains underutilized in an organization.

What if we had an intelligent methodology with an intelligent, high capacity, and easy-to-use tool which could automate things to leverage formal verification? We could utilize the skills of those formal verification experts to a large extent in formalizing the methodology and making the formal verification available for all designers and verification engineers without needing much of their expertise in introducing formal verification constructs into the design code.The formal verification could best complement simulation and other verification engines for faster verification closure of large SoCs.

I am very much impressed with VC Formal, the brand new tool for formal verification launched by Synopsys. This tool makes it very easy for a verification engineer to setup a design for formal verification, run, and debug it in quick steps.

In addition to formal property checking, VC Formal provides various apps which require minimal setup and are quick and easy to execute. They are all seamlessly integrated with the Synopsys verification and debug environment. For example, VC Formal and its apps use the same design parser and compiler as VCS, do quick analysis of code, report about ‘unreachable code’, and generate formal goals for code coverage. The apps include solutions like Formal Coverage Analyzer, Connectivity Checking, Sequential Equivalence Checking, and so on.

Recently, an app-based approach for formal verification has become very popular and is employed in a few tools in the market; however its effectiveness and success lies in the ease-of-use, tool capacity and performance, and effective interface with simulators and the debug system. VC Formal has large capacity and high performance which can be leveraged for exhaustive analysis required for hard-to-catch bugs, and of course for quick checks and analysis.

For debug, VC Formal uses Verdi, the most familiar debugging platform in the verification community. This provides design view, verification task management, progress status, waveforms, constraint generation, etc. on a single platform already familiar to design and verification teams, thus making it very effective for reproducing and debugging deep-rooted problems.

What is more important in a formal verification system is a strong methodology to define the flow keeping in mind the particular designs and their users, what to apply where and in which circumstances. This can be best done by experienced formal verification experts who can define the strategy to identify the design blocks which can be most effective for formal verification. Simple code coverage or any criteria other than verification closure cannot be an effective measure for formal verification. The formal strategy and methodology for a particular design flow can be best realized by a strong tool with high capacity, speed, strong formal engines with intelligent algorithms, and easy debugging.

Talking to Prapanna Tiwari, Senior Manager, Formal Verification Product Marketing at Synopsys, I learnt that VC Formal employs some brand new technologies that build an optimized formal model for faster operation such as SoC level connectivity checking or deep bug hunting in case of corner cases, among many others. Also, there are many usability features provided for effective interaction with designers to improve their productivity significantly.

Prapanna says the core engines in VC Formal were developed by a team of experienced professionals with deep expertise in formal verification. The GUI has been put through to realise a defined formal methodology most effectively. The tool is already in use with major design houses who have realized significant improvement in the time to verification closure of their designs.

There is an on-line webinar– Increasing Verification Closure Effectiveness with Formal Verification, first delivered live in the last week by Dr. Sean Safarpour, Formal Verification CAE Manager at Synopsys. Dr. Safarpour has presented in great detail about how to go about formal verification in general, the app engines and capabilities of VC Formal, the GUI, and debugging features with Verdi.

Also, Dr. Safarpour has explained setting up of a formal testbench, assertion setup and debug, and analysis of over-constraints through a real example. It’s worth attending this on-line webinar to learn about formal verification in general and specifics of VC Formal.

More Articles from Pawan