( ESNUG 445 Item 8 ) -------------------------------------------- [05/24/05]
Subject: ( ESNUG 443 #3 ) Erik's Follow Up to his Original Jasper Review
> One other note, the head designer is one of our more stubborn guys and
> hated the Jasper tool back when it was TempestQuest. He pretty much
> discarded any results from the tool because we couldn't constrain things
> properly. This last time through, with the latest Jasper tool, the same
> guy came around and found Jasper useful. His thing is "show me waves I
> can make sense of and I'll figure out the problem", and Jasper was able
> to do that.
>
> - Erik Maier
> Tundra Semiconductor South Portland, ME
From: Erik Maier <erik.maier=user company=tundra spot gone>
Hi John,
I just wanted to offer a follow-up to the comments I made about Jasper in
ESNUG 443 #3. We used Jasper on a different block after the initial use
talked about in my last review and found some good improvements. The
interface, documentation and feel of the tools are much improved with their
more recent 3.1 release of the tool. It feels and works like a mature
interface. Jasper added some additional formal engines, which proved to be
useful for different situations. It took some time to figure out when to
use each engine but overall it was not that difficult to learn and made
running the proofs faster and easier.
This time through we used Jasper to help prove correctness on a processor
bus interface and were able to find a handful of bugs which we hadn't found
using our traditional methods. One of the bugs was actually something a
designer thought might be a problem but wasn't able to see the exact way it
could occur and Jasper found the specific scenario right away with waves to
show how it happened. We were working at the "write" and "read" level
across good size submodules within the block. We found this much easier to
define correctness but it does take more work to constrain and run formal
proofs on than working at a lower level but overall make things easier.
So we were successful running formal proofs such as "if write X shows up on
the module boundary it makes it to the other side of the module correctly"
and we could easily cover duplication, corruption and transaction droppage
for that write with one proof target.
Jasper is being used on other designs within Tundra as well, but I don't
have enough visibility to say how they are going.
- Erik Maier
Tundra Semiconductor South Portland, ME
Index
Next->Item
|
|
