Mentor upgrades Questa with formal

Mentor Graphics has made some improvements in its Questa functional verification platform that enable mainstream users to more easily deploy aspects of formal verification without even knowing that they are doing it. This has been a trend for some time now, where increasing amounts of formal technology are being deployed under the hood to perform tasks that have become somewhat routine requirements in the verification process. Mentor says that it now provides extensions such as AutoCheck that delivers fully automated formal checking analysis, and CoverCheck that provides 100% code coverage closure. In addition, they now offer expanded clock-domain crossing (CDC) capabilities.

The big advantage of formal verification is that it performs verification without the need of a testbench because it considers all possible input streams. However, adoption of this technology has been hampered because of its complexity and sometimes large compute and memory requirements

Mentor claims to have changed all that by delivering a wide spectrum of formal applications that range from fully automatic formal checking with AutoCheck, a push-button technology, to property checking with custom coded assertions for advanced users. In addition, they are using the recently standardized Accellera Unified Coverage Database (UCDB) to blend simulation and formal-based technologies.

CoverCheck accelerates the process of code coverage closure. Code coverage closure typically involves many engineering weeks of effort to manually review code coverage holes to determine if they can be safely ignored and if not, to generate hand-crafted simulation tests to cover them. CoverCheck makes it easy for non-expert users to leverage formal methods to complete this process by automatically identifying the set of reachable and unreachable coverage bins. Consequently, it reduces the time required for code coverage sign-off, bringing predictability to the schedule. CoverCheck also ensures higher design quality by preventing bugs from slipping through the verification process due to mistakenly ignored code coverage bins.

AutoCheck analyzes RTL designs and automatically synthesizes assertions that are then processed by formal engines to check for correct sequential design behavior. Using AutoCheck, designs are verified to be free from common functional errors without the need to write a testbench or assertions. This release also delivers Formal Multi-Core, a new capability that enables multi-core and multi-computer distribution of formal jobs, further improving the throughput of formal analysis and optimizing the use of compute farm resources.

This release delivers additional CDC performance gains, boosting the capacity of CDC to match the complexity of today’s SoC designs. CDC also supports unlimited design sizes through hierarchical CDC analysis. It automatically generates block-level CDC interface logic models that enable chip-level CDC verification with full debug visibility.

Brian Bailey – keeping you covered

---

If you found this article to be of interest, visit EDA Designline where you will find the latest and greatest design, technology, product, and news articles with regard to all aspects of Electronic Design Automation (EDA).

Also, you can obtain a highlights update delivered directly to your inbox by signing up for the EDA Designline weekly newsletter – just Click Here to request this newsletter using the Manage Newsletters tab (if you aren't already a member you'll be asked to register, but it's free and painless so don't let that stop you).