New formal-based technologies have been announced by Mentor Graphics Corp. with the company’s Questa Verification Platform that enables performance of traditionally very difficult formal verification analysis much more simply, widening accessibility of the tool in effect.
The company’s new Questa AutoCheck technology is capable of delivering fully automated formal checking analysis, while a CoverCheck tool is can deliver some 100 percent code coverage closure. The platform also offers expanded clock-domain crossing (CDC) capabilities.
This Formal verification tool is said to offer functional analysis of all possible design behaviours without the need to specify the test stimulus, enabling verification early in the design cycle, before creation of a simulation testbench.
Previously, the promise of formal verification was only realised by verification teams with formal analysis experts that had to expend a high amount of effort to achieve results. This platform now offers an alternative by delivering a wide spectrum of formal applications that range from fully automatic formal checking, a so called powerful, push-button technology that is described as being accessible to all, to property checking with custom coded assertions for advanced users.
The platform is described as offering many verification solutions that seamlessly blend simulation and formal-based technologies with common compilation and user interface features as well as the Unified Coverage Database (UCDB).
The company’s verification platform features a CoverCheck option that is said to enable 100 percent Code Coverage Closure.
This technology accelerates the process of code coverage closure. This 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 handcrafted simulation tests to cover them.
This process is simplified for non-expert users by enabling them to leverage formal methods to complete this process by automatically identifying the set of reachable and unreachable coverage bins.
Consequently, it significantly reduces the time required for code coverage sign-off. This solution also ensures higher design quality by preventing bugs from slipping through the verification process due to mistakenly ignored code coverage bins.
The AutoCheck feature analyses RTL designs and automatically synthesises assertions that are then processed by so called powerful formal engines to check for correct sequential design behaviour. Using this feature, designs can be easily verified and can be free from common functional errors without the need to write a testbench or assertions.
In addition, performance improvements based on formal engines and formal model optimisations are said to deliver improved quality of results and a significant decrease in compute resource consumption. This also enables multi-core and multicomputer distribution of formal jobs, which is said to further improve the throughput of formal analysis and optimise the use of compute farm resources.
Mentor Graphics
