Formal integration enhances bug-hunting for Cadence

By Chris Edwards |  No Comments  |  Posted: June 8, 2015
Topics/Categories: Blog - EDA  |  Tags: , , , , , ,  | Organizations:

Following the acquisition of Jasper Design Automation last year, Cadence Design Systems is widening the target base of applications for formal verification, covering tasks from bug hunting through accelerated simulation to 'superlinting'.

Cadence has decided to shift the center of its formal verification strategy to JasperGold, building a number of elements from its existing Incisive environment into the tool.

Pete Hardee, director of product management for formal verification, said: "There is a rich set of engines in both tools. We are keeping the JasperGold engines but augmenting them with a couple of key engines that made a difference on the Incisive side."

"JasperGold is our main formal platform going forward. But we are not end of life-ing Incisive. That's still fully supported. But all of the new developments will be on the JasperGold platform."

Customers used to either of the environments will be able to use the approaches they feel familiar with, Hardee said: "We have a dual parser strategy going forward. It will allow current JasperGold customers to process the designs the way they always have. And in addition we've integrated the Incisive front end so that's easier for existing Incisive users."

The JasperGold front-end

Image The JasperGold front-end

Bug-hunting modes

Through the integration of JasperGold and Incisive and with addons for the recently launched Indago debugger, Cadence has made bug hunting a major focus of its recent efforts in formal verification technologies.

A 'random' bug-hunting mode is intended to find unwanted behavior in logic without having to create fully formed assertions to begin with.

"You don't need complete proof all the time to find bugs. You can use the formal engines to explore the state space," Hardee said.

Typically, the user sets a basic set of end-to-end properties that determine whether logic should or should not do something. As they explore the state space using the formal engine, the user can home in on bugs in the code.

"What you are typically doing is writing specific properties on what the behavior should be, but In the full expectation that you will not necessarily complete the proof. Along the way, by improving the properties, you will uncover the bugs," Hardee said.

"Another technique you can use is assertion-driven simulation and formal in combination, to get even deeper into the state space. You first explore with simulation then hand over to the formal engine to explore. I might not want to waste the engine's time completely verifying on a FIFO, so I might simulate its behavior and then hand over the rest to the formal engine," Hardee explained. "Then, I may want to go to a full proof."

Indago additions

As well as bringing the Visualize front-end from Incisive into JasperGold, elements of it will also appear in the Indago debugger.

"There are a couple of really good debug techniques in Visualize. It can find all the logic involved with a property, all the logic that got me to that state. It highlights only the logic that's part of the cone of influence. Then I can use the 'Why' button to let me look at the point of interest and show why that signal changed. Using these techniques, I can work back and see why the traces are the way they are.

"Then there are a couple of some powerful capabilities that are coming out in the more advanced debug app for Indago. One is 'quiet trace', which looks at relevant signals but not all the transitions. Quiet trace removes signal activity and take it down to the bare minimum of transitions involved [in reaching a certain state].

Hardee said: "Another addition is what-if analysis. If I edit the waveform, and I can do that on the fly, I can create a new constraint on the input at the point I edit it.Then it redraws the trace using the formal engines underneath.

"There are two main benefits. I can explore how a design operates. It's very useful for verification engineers in situations where the original designer is long gone. It's perfect for understanding how a block behaves. Or it can be used to confirm effects. 'What happens if I make that change to make that enabled' without going through the whole edit, recompile loop. It results in much, much quicker iterations.

"We think this is going to be a huge benefit, one that Jasper customers have already benefited from – this will be an app for Indago. We are taking formal technology and making it available under the hood of other tools."

Superlint flow

Hardee added: "One thing we had in Incisive was a flow for 'superlint', where it performed property creation from RTL. It could explore the potential for deadlock, livelock, range overflows, and simulation mismatches, that kind of stuff. We've recreated that flow with JasperGold and fully integrated it with Visualize.

"We have filters to grade by importance the properties that are created by the tool and use an interactive environment to link to the source code. It lets you create formal traces to debug without actually executing the design. It's very powerful linking this in with the Visualize environment."

A technique that now forms part of JasperGold is the ability to switch formal engines for different parts of a logic block that is being verified.

"The traditional approach is to try to prove a property using multiple different engines and see which one wins," Hardee claimed.

The Trident technology developed for Incisive instead will decide which engines to employ based on its understanding of the logic behavior.

"We believe this is unique to Cadence. Rather than just having one engine prove the whole property, it hands off the proofs between the engines depending where it is in the state space. This is now in JasperGold and is responsible for orchestrating some of the other formal engines," Hardee said.

Another piece of software that is new to JasperGold but was in Incisive before the merge is the unreachability app. "This is for formal verification-assisted closure with simulation," said Hardee.

The unreachability app looks at simulation traces and determines whether there are parts of the RTL that cannot be triggered from the simulation environment to help identify how coverage in a metrics-driven environment can be improved.

Leave a Comment

PLATINUM SPONSORS

Synopsys Cadence Design Systems Mentor - A Siemens Business
View All Sponsors