Unified, coverage-driven assertion-based verification, including a full automated apps library
Formal assertion checking has traditionally been hard to adopt, and has been viewed as a tool for specialists only. This has significantly changed with automation of recurring verification tasks using formal apps, as well as the widespread adoption of assertion languages, and vastly increased capacity of formal tools. Today a huge number of point tools for formal verification is available, each covering different formal use models.
OneSpin 360 DV-Verify™ goes beyond that by providing a unified, coverage-driven assertion-based verification flow, and including a full verification app library, as well as means for easy design exploration, all in one tool.
Formal Verification with DV-Verify
DV-Verify can be employed as a fully functional, coverage driven Assertion-Based Verification (ABV) capability, a design exploration, “what-if” analyzer, and an automated, targeted problem solver. It has been designed to augment existing verification environments, enabling the discovery of bugs elusive in simulation-only solutions, while providing an extreme ease-of-use experience.
DV-Verify Use Models
DV-Verify may be utilized in multiple stages of the Design Verification flow. OneSpin 360 DV-Verify is the only unified, coverage-driven assertion-based verification system available today that comes complete with a full App library for multiple use models.
- Agile Design Exploration: Early validation of design operations without writing stimulus for quick design iterations
- Metric-Driven Assertion-Based Verification (ABV): Comprehensive assertion-based verification with unique observation coverage
- Quantify Fault Observation Coverage: Effective measure of verification progress and coverage improvement
- Block Integration Validation: Scalable integration verification and functional analysis using automated flows
- OneSpin Formal Apps Library: Library of automated functions targeting recurring verification tasks
Agile Design Exploration
DV-Verify may be used in an exploration mode to trace design operation with a minimum of user interaction. The witness trace capability contained within the tool is able to take a minimum of information and provide a waveform trace of design behavior.
As such, a designer is able to quickly assess code operation, bring the design up, and perform ‘what-if’ analysis, at the push of a button without the hassle of simulation stimulus creation or setup. Optional assumptions about the code inputs, registers, clocks and reset can be easily input to further refine the analysis. The trace maybe be output as simulation test vectors and applied into any simulator. There is no requirement for expertize in writing assertions.
Metric-Driven Assertion-Based Verification (ABV)
The combination of a fully functional, high-performance formal property analyzer with a unique assertion coverage evaluator eliminates the guesswork from quality assertion generation. The ABV solution makes full use of the OneSpin technology platform to provide a high convergence rate while maximizing performance and capacity. DV-Verify includes the unique OneSpin Quantify Coverage technology. This “Observation Coverage” approach to understanding verification quality provides the clearest achieved coverage metrics, as well as visibility into “dead code” and other potential issues.
In this mode, DV-Verify can be used alongside a regression simulation environment to analyze complex verification scenarios and accelerate the overall schedule. DV-Verify will exhaustively check the design against assertions to either find a violation of those assertions or prove the assertions to hold under all conditions, something impossible to accomplish with simulation.
Automated Targeted Apps
Using the Apps Library, DV-Verify may be used as a fully automated issue solver for a range of challenging verification problems. The DV Apps library is packaged as part of DV-Verify, which provides an engineer with access to Connectivity and Register Checking, X-Propagation Analysis, Scoreboarding and Protocol Compliance Checking. In addition, full access to DV-Inspect through token licensing is provided with the three code analysis Apps associated with that product. Finally, DV-Verify is used as a platform for additional Specialized Apps for the Safety Critical and C++/SystemC Solutions. All of these Apps may be used with no requirement for creating assertions.
360 DV-Verify’s comprehensive standards compliance allows an easy integration into existing flows. Designs in VHDL, Verilog, SystemVerilog, SystemC and C++, or any combination of these, are supported.
Design setup in DV-Verify is straightforward, allowing its quick and easy adoption into existing flows. For example, existing HDL scripts may be reused and arbitrarily loaded into the tool. The system will take care of appropriate file ordering and automatically detect clocks and reset signals, thus saving time in the definition of these key inputs usually required in most tools. All these mechanisms provide the easy, push button approach with minimal or no user interaction.
With 360 DV-Verify’s network distribution, computationally expensive tasks can be parallelized over a network, accelerating execution. All results are collected in one central place for easy analysis. In essence, the only visible difference between running checks sequentially on a single machine or distributed over the network is the significantly reduced runtime due to parallel execution. This mechanism may be extended by leveraging cloud-based servers through the OneSpin Cloud solution.
In verification, engineers spend most time in debug. Inspect includes a comprehensive, ergonomic debug environment that incorporates various displays including standard waveform windows with signal coloring to highlight cause of failure, a source code window with active value annotation, and active driver tracing that allows accelerated root cause analysis. In addition, the various apps have more specialized displays, such as an FSM analysis tool that highlights problem states. The debugger uses a highly ergonomic Graphical User Interface (GUI) that makes code manipulation a snap.
OneSpin 360 DV features witness creation that further eases the understanding of issues. On detection of a problem, the formal platform will create a signal time trace that demonstrates a sequence of events that leads to the problem. This ease of use feature makes the formal process easy to understand by leveraging a familiar waveform approach to visualize issues. Further more the trace may be output as simulation stimulus from reset that allows the problem to be recreated using a standard simulator for further analysis if necessary. This allows an easy connection to the simulation flow and the automatic creation of directed tests.
OneSpin 360 DV features token-based licensing. This is a flexible licensing structure that allows local and immediate remixing of different products in the OneSpin DV family using the same license set. This feature allows for different capability to be employed at alternative phases of the development process using the same licenses, and aids with the introduction of the various products.
DV-Verify will operate on both Linux and Windows platforms.
OneSpin 360 DV-Verify is a powerful and flexible capability that significantly reduces verification time and effort in multiple phases of an IC development project. It is a complete tool that is easy to use alongside existing simulation-based flows. DV-Verify is in use at many companies and has been leveraged on 100s of design projects.