OneSpin launches industry's first comprehensive solution for automatic metric-driven formal assertion-based verification coverage analysis and measure

MUNICH, GERMANY, TOKYO, JAPAN & SUNNYVALE, USA: OneSpin Solutions, an EDA company that provides innovative formal assertion-based verification solutions, today announced Quantify MDV, the industry’s first formal metric-driven verification (MDV) solution that automatically and comprehensively analyzes and measures formal verification progress and quality in register transfer level (RTL) designs.

This breakthrough enhancement to the flagship OneSpin 360 MV product family provides precise feedback throughout a project, enabling verification engineers for the first time to answer three key questions quantitatively and accurately:
* How good are my assertions?
* How good are my constraints?
* How much of my verification plan has been completed?

Quantify MDV gives engineers and project management the comprehensive metrics they need to determine exactly how far along they are in their formal verification – without the need for simulation. For the first time, they can assess remaining project time and effort based on accurate measurement rather than educated guesswork. Quantify MDV is available now and OneSpin will demonstrate it at the 2011 Design Automation Conference in San Diego, California, Booth #1505, June 5-10, 2011.

No more guesswork or mystique
Quantify MDV removes uncertainty about formal verification progress and quality by comprehensively analyzing and tracking RTL code and assertions throughout the design space. It identifies both verified and unverified RTL code, showing engineers at a glance exactly where to put assertions to fill the verification holes.

It also analyzes constraints to identify over-constraining, thus eliminating the need to simulate assertions to detect over-constraining; and it identifies redundant code and verification code, as well as dead code, which is impossible to cover. Quantify MDV’s formal verification metrics can be integrated with testbench metrics to give full visibility into overall verification progress.

According to OneSpin president and CEO, Peter Feist: “Prior to Quantify MDV, engineers had no formal verification metrics that accurately quantified verification progress. Crude metrics such as assertion density don’t really measure verification progress or quality; they simply leave engineers guessing about how much of the design has really been covered. Now they don’t have to guess. Also, engineers now can integrate formal metrics with their testbench coverage, giving them full transparency. With a simple keystroke and no learning curve for our new, automated solution, OneSpin puts effective metrics into the hands of engineers and project management, eliminating what was, until now, a significant barrier to formal becoming a mainstream methodology.”

Engineers can use Quantify MDV at any stage in the project – from early verification of RTL sub-blocks to complete block and inter-block connectivity verification, to block design handoff. At any point, they can trade off accuracy and runtime – for example, to find unverified RTL code quickly in the early stages, while opting for greater accuracy as the project progresses to sign-off.

Quantify MDV enables formal verification to be integrated into the verification team’s overall MDV flow by outputting formal metric data in HTML format and for the Unified Coverage Database (UCDB). Verification engineers now can view both formal and testbench progress metrics simultaneously in an integrated report. They also can program Quantify MDV’s output to be compatible with other database formats, enabling the solution’s use in a broad range of verification flows.

“Every member of the verification team can be proficient using the automated Quantify MDV,” Feist added. “It eliminates the mystique, automatically removes uncertainty and reduces engineering effort while delivering superior verification metrics. No one has to be a mathematical genius or have special expertise to use it for accurate assessment of verification progress and quality.”

Quantify MDV supports the industry-leading assertion standard, SystemVerilog Assertions (SVA), for both structural and operation-based assertions. Engineers can use OneSpin’s Timing Diagram Assertion Library (TiDAL) to convert functional timing diagrams to operational SVA. Design language support includes SystemVerilog, Verilog and VHDL.

Quantify MDV is available now as part of the standard 360 MV product line, which starts at $25,000 for a one-year time-based license.