( ESNUG 440 Item 4 ) -------------------------------------------- [03/03/05]
From: Kevin Normoyle <kbn=user domain=azulsystems spot gone>
Subject: One User's Hands-On Review of Jasper's Formal Verification Tool
Hi John,
I was thinking that, from what I read on ESNUG, that people really don't
understand what's good and bad when it comes to formal verification. And
the tool vendors haven't been too helpful in clarifying the issues.
Sometimes it feels like people want to be able to write arbitrarily bad
Verilog, and then have a push button tool find all the problems.
I know what I want, so I'll just describe that and describe the pros and
cons of Jasper in meeting that.
I know that I can't find all the problems people create with simulation.
Even with an infinity of cycles and an infinity of assertion checks and an
infinity of transactors for stimulus. This is for any modern, reasonably
complex chip. So I need more. I need to be able to prove that certain
things are true or false.
I can make decisions about what I need to prove using my experience and
known high-bug-rate areas, or high risk areas. I don't have to pretend
I'm stupid and know nothing.
I don't want a tool that just tries a little harder and better than what
I've got with simulation, and tells me if it can find something. Anything
can find bugs. I can find bugs with just a sharp pointed stick. So people
bragging about these onesy-twosy bugs they find with some tool is silly.
Being able to prove true/false for properties is what I need. A property
is just an arbitrary bit of boolean logic, possibly with state, possibliy
looking at the design at arbitrary points (white box). If I can prove
these properties easily, then I can find bugs. It's that simple.
So what is Jasper? You read in as much RTL as you want. This is nice.
They blackbox anything you don't read in. It's always easier to define
interface properties at high levels, because we usually architect good
interfaces there, and poor interfaces at lower levels. The tradeoffs are
all about speed and whether you'll ever get a result, if you're at too
high a level.
Jasper has nice ways of creating new arbitrary boundaries within a chunk
of RTL. These commands are called "stopat" and "assume". The stopat
means that arbitrary values are inserted starting there, rather than
propagated, like a top level port. "assume" can be an arbitrary function,
to limit the legal values.
You can create what I call scafflolding RTL (or a "jig" instance in Jasper
parlance) to surround the design under test. This RTL can define the legal
constraints on interfaces or have complicated logic for saying whether an
output is legal. This is all Verilog. This is great if you're a designer.
No learning curve for the language. We all know you can represent anything
in Verilog. Works great. I have lots of functions and behavioral Verilog
in this scaffolding RTL.
They also have a script based input, for the basic read, stopat, assume,
and prove commands. Prove's can be arbitrary logic, and use anything in
the design.
They are some weaknesses. You can use hierarchical references in prove
scripts, but not (currently) the jig RTL. But you can hook arbitrary ports
to the jig RTL, that can get hierarchical references connected, so you can
get anything you want. It's just an issue of how much you write.
When they find a false proof, you can get a nice trace. Their current GUI
is a little weak. It's Tcl/java based. Not the prettiest looking but gets
the job done. They are developing a new GUI though.
You start at the end result and work backwards. You can click and get all
signals that are part of the fanin for a signal, or you can source browse
with a "why" button that shows why the value is that way.
The trace is color coded. You can tell which signals are not critical
to the false proof, and which ones are just assumptions. The red signals
are the key ones. They may not be possible. You look around for red ones
that might be wrong, and click on them to "justify". The Jasper tool then
follows that path and makes sure it's legal.
I find I create a manual list of flops to "justify" as part of my script.
It reminds me of the early days of using dc_shell. People lived with doing
a bunch of support work, because the results were worth it. Once I get my
manual list for a area of logic, I find I don't have to do much interactive
clicking.
It's definitely a white box tool. I find that's a good thing. I can get
inside a designer's head without talking to him, using this Jasper tool.
The wild thing that gets a little while to get used to is, if you're an
old-school simulation guy, that you're always working backwards from a
result to the stimulus. You create simple proofs, and the Jasper tool
creates all the complexity around that, as opposed to you focusing on
creating complicated simulation transactors.
For instance, I crawl before I walk. I look for writes of FIFOs while full,
reads while empty. Then I look at any pipeline flow control signals, and
whether I can create simple checks around them. Then I define legal inputs
for interfaces at some level. By now I have a feel for what goes fast and
slow for the Jasper tool and the amount of RTL I'm throwing at it. If I
throw nothing but legal inputs, I check that I get nothing but legal
outputs. Note the in to out is uncorrelated at this point, so it's not
bulletproof. I'm just going for bang for buck proofs at this point. I go
in and proof any assertions the designer put in his code at this point.
(Those are usually so simple to prove!)
At this point I've built up a set of RTL and script stuff, and I just keep
expanding it. The nice thing is then all this stuff is re-used. If I've
got common interfaces in a big chip, I can reuse all the scaffolding RTL
and script stuff.
I've been using Jasper on blocks of RTL up to around 5 K lines. You want
quick interactivity. Trying to work at higher levels than this will
probably be too slow. I use it on blocks of RTL up to about 10,000 lines,
although that's pushing it.
I've found bugs where the Jasper proof tool had to work back 32 cycles or
so. Pretty complicated stuff.
One weak point in Jasper is memories. They are treated as black boxes.
Normally any value on the output is not legal (for FIFOs, etc). So you
have to build abstraction models on those interface boundaries, usually
optimized for a particular proof... i.e. single bits that say whether you
got a transaction of a certain type, etc.
My other experiences were with @Verifier and Magellan, both interesting,
and with their own pros and cons. We use @Verifier for other reasons, and
I tried hard to use Magellan to prove OVA assertions. Both of those tools
would need me to define correct interfaces to get further good results,
just like Jasper. But I like the way Jasper flows. It's a nice hammer to
swing. So I'm sticking with it. I find the bugs, and even when I don't
I can prove things true. That is amazingly powerful. Just yesterday,
while I didn't find this one bug, I assembled a proof that demonstrated the
bug and proved that the fix was correct and there were no other similar
failure modes.
I have found bugs on my own with Jasper though.
The first design outside of my own code I found FIFO issues with all the
different FIFOs in the design. I was stoked after the first 2, and worked
hard for the trifecta. Didn't take too long.
In my RTL, the Jasper guys found 2 very subtle bugs in one week.
We were at our status meeting, and I was whining that I didn't think anyone
could start cold on a design, and find a bug in a week with Jasper. They
said they could.
I described the top level interfaces, (they had a little knowledge of what
we were doing already). They went away. Came back next Friday and found
two very subtle bugs. They saved my ass. Our guy doing simulation, even
knowing what the problems were, took a long time to fine tune his
transactors to expose the issues... actually I'm not sure if he ever was
able to. (He thinks he eventually did, but I'm not sure.)
I got down on my knees and bowed down in front of the Jasper sales rep and
the support engineers.
Jasper has been working with some customers on getting rid of testbench
development in the early stages of a design. So it's possible. I've done
it a little. Simulation still has it's place, in terms of efficiency
(# of bugs found per unit time), I think. For things like simple
functional verification (can I read/write all CSRs etc), simulation is
still better.
It's all about using the tool in the right place, understanding it's
strengths and weaknesses, and planning accordingly.
Or, you can just assume you can write garbage Verilog and someone should
have a pushbutton tool, and bitch to Cooley if that's not true!
If you ran a Cooley Bake-off, and had any piece of random RTL, with
a random bug, and I was competing with other guys for finding it, I would
probably use Jasper and have a reasonable chance of finding the problem
before anyone else.
- Kevin Normoyle
Azul Systems, Inc. Mountain View, CA
Index
Next->Item
|
|
