Mentor Graphics 0-In Formal v3.0 brings new level of automation to formal verification

WILSONVILLE, USA: Mentor Graphics Corp. has announced the immediate availability of the 0-In Formal tool version 3.0, the industry's most advanced solution for the formal verification of complex IC designs.

New capabilities in the 0-In Formal tool deliver greater ease of use through automation, more rapid coverage closure through coverage ‘reachability’ checks and the integration with the Questa® Unified Coverage Database (UCDB), and higher performance and capacity due to improvements to the underlying verification engines.

Formal verification is one of the technologies required by today’s complex IC design teams to combat the mounting challenge of verifying the functionality of their designs.

The 0-In Formal tool enables users to find and fix many bugs before simulation even begins, which enables them to focus simulation on achieving coverage of required behavior much sooner. Unlike simulation, which tests one particular scenario at a time, the 0-In Formal tool explores all possible scenarios in parallel, to thoroughly verify that no errors can possibly occur. At times, despite the best efforts in verification, design errors escape to silicon.

The 0-In Formal tool speeds diagnosis and correction of such errors by enabling users to quickly locate the error in the HDL model and verify that a proposed fix makes the design work correctly.

The 0-In Formal tool also provides improved support for mixed-language design through tighter integration with the Questa® platform. This is achieved through a common user interface, common front end, meaning the use of the same compilation flow for both the Questa platform and the 0-In tools, and the common back end, namely the fact that both the Questa platform and the 0-In tools write to the UCDB.

The integration with the Questa platform front end has improved support for design and verification language features in VHDL and SystemVerilog as well as for assertion language features in PSL and SVA. In addition, automatic checks in the 0-In Formal tool can detect a large number of typical errors automatically, with no need for the user to write assertions.

The 0-In Formal tool also delivers the ability to verify more types of behavior through the addition of ‘liveness’ properties such as “from any state, the design will eventually reach the reset state.”

In addition, the automatic identification of unreachable coverage points and integration with the UCDB allows the tool to automatically exclude unreachable coverage points from coverage calculations to achieve coverage closure more quickly.

An improved use model includes enhanced support for visualization and debug of formal verification results, and new and improved verification engines provide higher performance and capacity, which enables faster and more complete verification of more complex designs.

“Mentor Graphics has put some impressive improvements in version 3.0 of the 0-In Formal proof engine,” said Dr. Shaun Feng, MTS design engineer at AMD. “Compilation is very fast and enables AMD to prove all of our properties. The new release is also able to analyze latches very effectively, even when clock and data are intermixed.”

“Formal verification experts will appreciate the improved performance of our leading proof engine technology and the support of liveness properties,” said John Lenyo, general manager, Design Verification Technology (DVT) division. “By eliminating the need to write assertion properties, the automated verification checks place the power of our formal verification technology into the hands of all verification engineers, not just the formal experts.”