Cadence combines its own, and acquired Jasper, formal tools
Cadence says that while the benefits derived from applying formal methods are highly application-dependent; it is seeing “up to 15X performance gain versus previous solutions”, and that JasperGold, now integrated within the System Development Suite, finds bugs typically three months earlier than existing verification methods. The formal analysis engines are now integrated with Cadence’s Indago debug platform, automating root-cause analysis and on-the-fly what-if exploration. The performance metric is, essentially, the number of formally-expressed properties completed (or disproved) in a given time.
A Cadence spokesman commented that broadening the use of formal methods is about both performance and usability, and notes in particular the integration of formal methods into the debugging process to use the techniques more generally. The “classic view” of formal methods is that of forming a complete and rigorous proof that (to take the case of logic equivalence checking) one representation of a desired function is identical in every respect to another: that one does exactly the same, no more or less, than the other. Completeness is not essential to get value from the tools, Cadence says. The traditional view of the tools’ output is that they might tell you that you have, or do not have, equivalence – and might be of limited help in revealing why not, should the test have failed. Cadence says that in its latest implementation the software can – in effect – stop when it encounters a bug and tell the user, ‘this is a bug that in itself would prevent reaching completeness’. There is also the possibility of grading issues found by the formal engines according to whether they are ultimately of importance to the functioning of the system.
Expansion of the use of the underlying formal ‘engines’ extends beyond assisted debug into formally-assisted simulation; a range of engines can be applied to a problem, or individual mathematical engines can ‘hand-off’ problems to each other. A further dimension is formal-assisted emulation, where assertion-based approaches augment a [hardware-] accelerated techniques.
The JasperGold platform aims to improve design quality and efficiency by integrating a comprehensive set of features into one solution, including:
• Design compilation and formal engine technologies from Incisive Formal Verifier and Incisive Enterprise Verifier, including the Trident multi-cooperating engines. This enables easy migration for existing Incisive customers and up to 15X performance improvement for both bug-hunting and proof convergence modes.
• The next-generation JasperGold platform has been fully integrated with the Cadence System Development Suite’s Incisive simulation and Palladium emulation platforms, and with vManager tool to enable comprehensive metric-driven verification. This results in an up to three-month schedule reduction through formal-assisted verification closure.
• JasperGold Visualize and QuietTrace technologies have been integrated with the Indago debug platform to further expand analysis and on-the-fly what-if exploration, helping reduce root-cause debug time – Cadence says by, “up to 5-100X”.
“As long-time customers of Incisive formal and simulation solutions, we are impressed with the next-generation JasperGold platform,” stated Mark Dunn, executive vice president at Imagination Technologies. “As well as improved debug and ease-of-use, we’ve achieved a significant increase in performance compared to Incisive Enterprise Verifier, as measured by proof convergence in a given time.”
Cadence adds that the users who are most advanced with formal methods are using it as a main methodology for verification at the block (that is, functional block for an SoC) level. That is extending, the company concludes, up to chip level, with examination of, for example, top level connectivity of a design.
Cadence; https://cadence.com/news/jaspergold
If you enjoyed this article, you will like the following ones: don't miss them by subscribing to :
