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.
