Comprehensive assertion-based verification with unique observation coverage
A thorough and complete test of all blocks in an IC is absolutely essential. A single bug in a production IC will be expensive to fix and can cause catastrophic product failure in the field. Block level verification has traditionally made use of complex stimulus systems, employed across multiple batch mode simulation runs. Even with this verification horsepower, it often proves hard to achieve verification closure, especially when based on simulation code coverage metrics.
OneSpin’s metric-driven verification solution provides formal assertion-based verification, including a unique, accurate formal code coverage analysis that integrates with simulation coverage results.
Combining Formal Verification and Simulation
Random stimulus methods and the Unified Verification Methodology (UVM) have improved the ability to produce effective test vectors, but with a corresponding increase in verification environment complexity. Current UVM simulation solutions have significant drawbacks, including an inability to efficiently set up complex scenarios to ensure that all block functionality is tested. This leads to a decelerating, asymptotic coverage progress curve that rarely reaches 100%.
Formal verification solutions that operate in a complementary manner to simulation can solve this coverage issue. As a formal tool maintains the entire state-space of the block under test, the complexity of creating certain test scenarios is reduced. Assertions are used to express functional properties to be either proven or disproven, and in this manner the most complex scenarios are fully investigated.
A number of companies today employ methodologies where the verification test plan is examined to understand which test scenarios are better served by simulation with UVM testbenches, and those that benefit from a formal approach using assertions. The tools are applied as appropriate and coverage information collected to understand overall progress. Using this two-pronged approach, complex scenarios are analyzed earlier in the process and bug free coverage is achieved more rapidly.To enable a closed loop, metric-driven verification solution, OneSpin’s Quantify technology, a precise coverage mechanism that makes use of an “Observation Coverage” algorithm, is applied.
In order to execute a variety of scenarios in a reasonable timescale, and to contain the entire block under test, a superior level of formal technology is required. OneSpin’s 360 DV-Verify award winning product contains a highly optimized formal model and leverages a broad range of formal algorithms to ensure the design is tested as quickly and efficiently as possible. In addition, the solution contains advanced debug and ease-of-use features that simplifies tracking and debugging problems.
Coverage for Formal Verification
To enable a closed loop, metric-driven verification solution, OneSpin’s Quantify technology, a precise coverage mechanism that makes use of an “Observation Coverage” algorithm, is applied.
The observation coverage algorithm analyzes the code to ensure that any change will trigger at least one assertion, providing both an overall measure of coverage, as well guidance to particular coverage holes.
The solution makes use of token based licensing for local product remixing, and can operate in a parallel processing mode for enhanced performance.
- 360 DV-Verify Product
- Quantify Coverage App
- Presentation: From Requirements to Sign-off using Quantify
- White Paper: Reducing Verification Risk with Formal-Based Observation Coverage
- Article: How Formal MDV Can Eliminate Verification Uncertainty