Posted by Ravindra Aneja on June 2, 2017
Sean talked about it in his blog Progression in formal verification – last decade.., Formal verification has come a long way but in most of the first meeting with potential new customers, these are still the most commonly asked questions:
Well, answer to all these questions depends on what are critical verification problems that user is struggling with and of course benefits are proportional to the efforts user puts-in. This is pretty much true to everything you do, take health management for an example.
Like most working professionals in bay area, I try to go to gym few times in a week. Now, there are many options in a gym and these options require certain level of dedication, discipline and effort to achieve personal health goals one may have. The gym I go to has options like cardio, yoga, Zumba dancing, basketball court, swimming pool and regular exercising equipment. Now, everyone coming to this gym has his/her own goals. Someone like me who has been going there for some time, I follow my own routine and it works for me. Folks who have very specific health goals like weight management, preparing for professional sport etc. take advantage of professional trainers. Point is that same gym infrastructure caters to different needs of different customers, but achieving specific goals require certain level of effort.
Same concept applies to formal. Formal provides the same infrastructure to cater to various applications to address various complex verification problems. These applications require different level of discipline and effort and of course the more effort you put in the harder verification problems you can address.
Let us take few examples here to describe correlation between verification complexity and the effort required to address it.
Code coverage has been an integral part of signoff criteria for simulation based verification. Verification teams have been tracking this verification metrics for years and we all know the struggle it takes to close on last 10-15% goals. It is just too expensive to manually analyze each and every remaining coverage goal to decide if this goal is really reachable or not. Formal App called FCA (stands for Formal Coverage Analyzer) caters to this specific problem. As part of this App, formal reads-in simulation coverage database to identify the remaining coverage goals, performs formal analysis and then generates exclusion for unreachable coverage goals. User can review these exclusions and if these exclusions are harmless, then these coverage goals can be ignored. This App requires relatively small amount of effort and verification team can close the coverage gap relatively quickly.
Now, let us go to other end of the graph and talk about property verification. This caters to verification problems where design team have critical functionality with lots of control logic involved and it is very hard to verify many concurrent functions using simulation based verification. This is where traditional verification methods may not scale and it is a sweet spot for formal. Since verification complexity and benefits are higher, it also requires relatively more effort and expertise.
In future blogs, we will discuss a bit more about these specific applications and what does it take to signoff using formal methods. Stay tuned……….