Electronicdesign 1614 Xl davemaliniack
Electronicdesign 1614 Xl davemaliniack
Electronicdesign 1614 Xl davemaliniack
Electronicdesign 1614 Xl davemaliniack
Electronicdesign 1614 Xl davemaliniack

Formal Verification Reaps Benefits Of Distributed Processing

July 27, 2009
Jasper Design Automation's JasperCore formal tool incorporates a capability called ProofGrid, which enables the tool to distribute a high-level proof across multiple processors on a multi-threaded machine.

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

www.jasper-da.com

Sponsored Recommendations

Understanding Thermal Challenges in EV Charging Applications

March 28, 2024
As EVs emerge as the dominant mode of transportation, factors such as battery range and quicker charging rates will play pivotal roles in the global economy.

Board-Mount DC/DC Converters in Medical Applications

March 27, 2024
AC/DC or board-mount DC/DC converters provide power for medical devices. This article explains why isolation might be needed and which safety standards apply.

Use Rugged Multiband Antennas to Solve the Mobile Connectivity Challenge

March 27, 2024
Selecting and using antennas for mobile applications requires attention to electrical, mechanical, and environmental characteristics: TE modules can help.

Out-of-the-box Cellular and Wi-Fi connectivity with AWS IoT ExpressLink

March 27, 2024
This demo shows how to enroll LTE-M and Wi-Fi evaluation boards with AWS IoT Core, set up a Connected Health Solution as well as AWS AT commands and AWS IoT ExpressLink security...

Comments

To join the conversation, and become an exclusive member of Electronic Design, create an account today!