Open side-bar Menu
 Guest Blogger
Rob van Blommestein
Rob van Blommestein
EDA Consortium Communications Chair and Director of Corporate Communications at Jasper Design Automation.

Accelerating Coverage Closure with Jasper

August 6th, 2012 by Rob van Blommestein

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

Related posts:

Tags: ,

Category: Jasper

Leave a Reply

Your email address will not be published. Required fields are marked *



TrueCircuits: IoTPLL

Internet Business Systems © 2018 Internet Business Systems, Inc.
25 North 14th Steet, Suite 710, San Jose, CA 95112
+1 (408) 882-6554 — Contact Us, or visit our other sites:
TechJobsCafe - Technical Jobs and Resumes EDACafe - Electronic Design Automation GISCafe - Geographical Information Services  MCADCafe - Mechanical Design and Engineering ShareCG - Share Computer Graphic (CG) Animation, 3D Art and 3D Models
  Privacy PolicyAdvertise