Formal verification, which found its sweet spot in block-level verification at RTL some years ago, has since been deployed in an ever-broadening spectrum of scenarios. From architectural verification to protocol certification, and even to post-silicon debugging, formal tools have proved themselves an invaluable weapon in the verification team’s arsenal in the struggle to eradicate design errors.
Formal tools are extremely powerful, making comprehensive sweeps through a given state space to root out bugs. Unfortunately, they can also take a lot of time in the process, forcing verification engineers to decide between the breadth of their formal coverage and their schedule. It may or may not be possible to make formal proof engines execute faster in an absolute sense, but it is certainly possible to divvy up their work amongst multiple CPUs and gain time that way.
That’s what Jasper Design Automation has done with JasperCore, its latest formal tool. JasperCore incorporates a capability called ProofGrid, which enables the tool to distribute a high-level proof across multiple processors on a multi-threaded machine.
The application of distributed processing to formal verification has a number of implications. Most obviously, if a user is trying to execute many formal proofs at the same time, these can be farmed out to multiple processors. “Jasper has many patented formal engines, some of which are better at some kinds of proofs than others,” explains Holly Stump, Jasper’s vice president of marketing. “ProofGrid technology allows you to distribute these engines across machines.”
ProofGrid enables users of both the new JasperCore, as well as Jasper’s flagship JasperGold product, to take advantage of today’s low-cost computing resources to make formal verification highly scalable. It allows for parallel processing of proof jobs on local machines, clusters, or server farms. Multiple proof engines are tracked using a unified console, making for increased verification productivity as users are freed from manually separating and dispatching multiple single runs and then collecting the results for each one.
Both JasperCore and JasperGold have been rearchitected to deliver faster proofs while consuming a smaller memory footprint. A key element to the rearchitecture is a new design traversal algorithm that enables the proof engines to focus on the part of the design that’s most relevant, making the process of debugging that much faster.
Another new feature in the latest iteration of JasperGold (and of ActiveDesign, Jasper’s design and reuse tool) is QuietTrace, a visualization and debugging capability for RTL development that helps designers literally see through the noise in waveform displays. QuietTrace works with Jasper’s Visualize, which automatically generates and manipulates waveforms from RTL without a testbench, to not only display those waveforms but to highlight which of them are relevant to specific behaviors in the design.
JasperCore is available now, as are updated versions of JasperGold and ActiveDesign.
Jasper Design Automation