Cadence combines its own, and acquired Jasper, formal tools

June 09, 2015 // By Graham Prophet
Cadence has announced its next-generation formal verification platform. Combining the formal methods previously incorporated in Cadence’s Incisive tools with the technology it purchased with Jasper, the designation selected going forward is the JasperGold Formal Verification Platform

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,