Globalpress: Mentor weds formal and simulation verification techniques
Mentor Graphics has launched a product that mixes formal and simulation verification technologies in the Questa Verification Platform which aims to make it easier to perform formal verification analysis.
The key problem which verification is designed to solve – re-spins – hasn’t improved for eight years, says Harry Foster, Mentor’s Chief Scientist for Verification.
“Two third of the industry is behind schedule and one third of the industry lies,” says Foster, “70% of the industry requires two or more re-spins. That hasn’t changed since 2004.”
Each re-spin means a new mask-set and those cost $1m or more.
The Questa AutoCheck technology delivers fully automated formal checking analysis, while the Questa CoverCheck tool provides 100% code coverage closure.
The Questa Verification Platform has expanded clock-domain crossing (CDC) capabilities. It combines the two approaches to verification – simulation and formal. “It’s a beautiful example of how merging these technologies uses formal technology to improve simulation techniques,” says Foster.
Formal verification offers functional analysis of all possible design behaviour without the need to specify the test stimulus, enabling verification early in the design cycle, before creation of a simulation testbench. However, in the past, 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.
The Questa platform changes that by delivering a wide spectrum of formal applications that range from fully automatic formal checking with AutoCheck, a powerful, push-button technology that everyone can easily use, to property checking with custom coded assertions for advanced users.
The Questa platform contains verification solutions that blend simulation and formal-based technologies with common compilation and user interface features as well as the Unified Coverage Database (UCDB).
The Questa CoverCheck technology 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 handcrafted simulation tests to cover them. Questa 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 significantly 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 analyses RTL designs and automatically synthesizes assertions that are then processed by powerful formal engines to check for correct sequential design behaviour.
AutoCheck, designs are easily verified to be free from common functional errors without the need to write a testbench or assertions. In addition, performance improvements based on breakthrough formal engines and formal model optimizations deliver improved quality of results and a significant decrease in compute resource consumption.
This release also delivers Questa Formal Multi-Core, a new capability that enables multi-core and multicomputer distribution of formal jobs, further improving the throughput of formal analysis and optimizing the use of compute farm resources.
Questa CDC is used extensively by leading semiconductor design teams and it sets the bar for capacity, ease of use and quality of results. This release delivers additional performance gains, boosting the capacity of Questa CDC to match the complexity of today’s SoC designs.
Questa CDC also supports unlimited design sizes through hierarchical CDC analysis. It automatically generates highly accurate, block-level CDC interface logic models that enable chip-level CDC verification with full debug visibility.