Accelerating Coverage Closure with Jasper

Jasper’s formal technology has advanced to the point that it can address a broad range of verification and design issues. With a strong foundation in fundamental proof technology and best-in-class capacity and performance, Jasper’s users now apply the tools and technology to address questions of connectivity, x-propagation, clock-glitch detection, protocol cache coherence, deadlock detection, property synthesis and more.

The added scope and breadth of use of Jasper’s tools and technology is leading users to demand a measurable and quantitative approach that will help correlate the results of formal proofs to verification closure, often expressed in terms of verification coverage. What is needed is a methodology that will correlate formal proof results with coverage. A second requirement is for a methodology that can integrate the coverage results from Jasper’s formal technology with other verification tools (simulation). A third requirement is the ability for Jasper tools to use external coverage data to address areas in the design that are not covered by other verification methodologies.

To address such needs, Jasper created a comprehensive coverage strategy. Jasper developed metrics that can be used to measure and correlate the results of formal proofs with corresponding coverage measurements. Specifically, Jasper’s formal users can see coverage results for complete and bounded proofs expressed in the same familiar coverage terminology they are used to.  In addition, Jasper integrated the coverage reporting mechanism with an industrial coverage database like UCDB so that users can view and review the coverage results in the context of a complete verification effort.

Coverage metrics from Jasper can be used to measure the completeness of users’ formal constraints and assertions.  Users can get answers to questions such as

1. Are there enough constraints, or is the design over constrained?
2. Are there enough assertions that cover the entire design?
3. Are any of the constraints unintentionally eliminating legal behavior?

Another powerful feature of Jasper’s coverage metrics is the ability to correlate proof results (for complete or bounded proofs) with design-based coverage information such as line coverage, expression coverage, branch coverage and unreachable cover targets.

Integration with a coverage databases, such as UCDB, leverages a familiar GUI and reporting mechanism and allows the user to view and comprehend the complete coverage results from simulation with Jasper’s formal tools. Jasper’s tools can also access the coverage data base, extract the cover targets that are yet unreached and direct the user on a path to add properties that can close the verification gap left open by other tools. Additionally, this integration provides two key benefits. First, it allows the user to combine coverage results from multiple methodologies for fast closure. Second, it can provide a direct measurement for return on investment for the use of Jasper’s tools and technologies.

To learn more, please see an in depth video presentation that outlines these usage models of Jasper Formal technology.  To view the seminar, go to www.jasper-da.com/coverage_closure_seminar.

Tags: Constraints, Coverage Closure

Category: Jasper

This entry was posted on Monday, August 6th, 2012 at 12:01 am. You can follow any responses to this entry through the RSS 2.0 feed. You can leave a response, or trackback from your own site.