( ESNUG 430 Item 10 ) -------------------------------------------- [06/16/04]
Subject: ( DVcon 04 #10 ) One User's Hands-on Eval of Jasper JasperGold
> We use Jasper in our flow. We have found some really good corner case
> bugs in our earlier PCI-based designs and we are having mixed results
> in our new generation of products. This could be our fault of not
> having resourced adequately; a classic challenge of staffing the
> traditional approaches vs. new methodologies. The challenge has been
> that though we are "believers" in the formal methodology, we are waiting
> for vendors to provide solutions that can be integrated easily with the
> least ramp up time that we can put to "use". There is still ground to
> cover before Jasper becomes main-stream.
>
> - [ An Anon Engineer ]
From: Dan Katz <dan.katz=user domain=cavium got calm>
Hi John,
We have been evaluating JasperGold to explore how the tool would fit into
our current design/verif flow. We began by using Japser on one of my
blocks that had just been completed so it was relatively immature and
rather buggy to begin with. The block is a standard network interface;
mostly datapath, some interesting control.
We began by simply sending the block and a basic spec to the Jasper guys
and within a week, they had come back with about 6 bugs based on only a few
assertions. Then a Jasper AE came onsite to further expose us to the tool.
Another 6 bugs were uncovered during that week.
I thought the tool was quite intuitive and easy to use, once you understand
how Jasper carves out its inspection space. The tool does a nice job
showing the user where the proof boundries lie by color-coding the signals
on the waveform display.
Since Jasper uses the white-box model, it really requires that the person
debugging the proof have a pretty good understanding of how the code should
function. If you do not know the design's intent, it takes much longer to
find the terms that are actually breaking the design.
The other problem that we encountered was that our memory models were not
handled very well and needed to be black-boxed. In a datapath design, this
can get quite cumbersome.
In terms of a usage model, I believe that Jasper is most valuable for use
by the RTL engineer at the design entry time. Assumptions are fresh in the
mind and can be easily proved. The designer has the knowledge and is not
hindered by a white-box approach. In Cavium, our designers usually whittle
together a small testbench to do basic testing before passing it off to
verification for full/rigorous testing. Testbenching as a side project is
time consuming and throw-away once the real testbench comes up. Focusing on
a tool like Jasper is a much more productive use of time. The proofs do not
require the code of a checking testbench and can exercise the design at a
much more complete level since every option is thrown at it. My testbench's
tend to do only basic transactions in a handfull of configurations. Jasper
does everything all-at-once.
The other place we identified for potential Jasper use is during bug fixes
found with simulation. Bugs can usually be described as a failure of
an assumption (two things asserted at the same time, etc). Using Japer to
prove bug fixes means that the bug is really fixed and we won't suffer from
whack-a-mole problems. Even cousin assumptions could be explored.
As a small company, we still struggle with the time investment needed to
train engineers and expose them to Jasper. Schedules are tight and
usually do not account for tool adoption.
Jasper works well on small code examples, but can quickly become overrun if
the block becomes too large or its forced to look at too big a state space.
Once the proof is written, I've found it to be an interactive and iterative
process in properly constraining the space.
Jasper is a great tool, but it can't do everything. One thing about finding
bugs is that different approaches turns up different bugs. Jasper gives us
options. The other side effect that the entire Jasper process has, is that
when debugging proofs, the debugger is exposed to many scenarios that may
or may not be possible. This forces a more detailed spec of the block just
to accept or dismiss the cases.
During our eval, we did not encounter any tool bugs.
I personally have not had the opportunity to try other tools, so I don't
have much basis for comparison.
- Dan Katz
Cavium Networks Santa Clara, CA
|
