( DVcon 04 Item 10 ) --------------------------------------------- [ 05/26/04 ]
Subject: 0-in, Jasper, Synopsys Magellan, RealIntent Verix, Averant, @HDL
AN ACQUIRED TASTE Like a lot of other chip designers, I lump model checkers
and formal tools that aren't equivalence checkers into a catch-all category
called "bug hunters". These tools invariably start out with "first you feed
it your design..." then this is followed by "some complex formal mumbo jumbo
now happens here..." followed by "... and here are the bugs it found."
"What do you think about "bug hunters" like 0-in, Jasper,
@HDL, RealIntent, Averant, or Synopsys Magellan (Ketchum)?
Does your company use such tools?"
don't use : ################################### 70%
0-in : ####### 14%
Jasper : ## 5%
Synopsys Magellan : ## 5%
RealIntent Verix : # 4%
Averant Solidify : # 3%
@HDL : # 2%
Cadence BlackTie : 1%
With a 70% "don't use" rate, bug hunters are an acquired taste in the eyes of
many. Subtracting out all 70% of the "don't use" people leaves:
0-in : ################################################ 47%
Jasper : ################ 16%
Synopsys Magellan : ################ 16%
RealIntent Verix : ############# 13%
Averant Solidify : ########### 11%
@HDL : ######## 8%
Cadence BlackTie : ### 3%
Kvetching aside, 0-in rules the Bug Hunter category with close to 50% market
user market share numbers. All the other 0-in rivals struggle with 1/3
(or less) of the customer use that 0-in enjoys. (16%, 13%, 11%, 8% vs. 47%)
We don't use "bug-hunters". We ARE the "bug-hunters".
- John Ford of SolarFlare Communications
0-in looks good, but we don't use any of them.
- Lutz Naethke of Atmel
We used 0-in. It is a great tool. Difficult to use. Support is
good but scarce.
- Inder Singh of iVivity, Inc.
These tools can catch bugs, therefore in my book they are useful,
however, as an IP company we do not want to get tied into one
proprietary solution e.g. 0-in.
- Samuel Russell of Ceva, Inc.
None of the above. Used Averant Solidify.
- Ram Sunder of Specular Networks
We don't use any of them, don't think they are worth the time/money.
- Brad Hollister of NetSilicon, Inc.
0-in is great. The companies I work in do not use it as it is too
expensive.
- [ An Anon Engineer ]
We do not use them, because we do not consider them useful.
- Willem Sloof of Philips Microdisplay Systems
Using 0-in has helped us find bugs earlier and closer to the "source" in
a way that had visibly positive impact on schedule.
- Tom Heynemann of Hewlett-Packard
I've looked at some of these tools, and don't think they offer any
real benefit.
- Brian Kahlig of DRS Signal Technologies
Evaluated Averant a few years ago. Too hard to use. Their proprietary
assertion language at that time was too difficult to write good temporal
expressions. Just looked at @HDL. Had no automated way to deal with
multiple clock domains. It found combinatorial loops that weren't there!
Their GUI, once it came up, crashed our X server.
Been using primarily RealIntent's Verix and love it. Our more recent
evaluation showed we picked a good tool. We have found many bugs using
Verix. Look for my upcoming article in Chip Design magazine for more
details. I think using SVA and OVL are the way to go so you can be
tool independent.
I was surprised to see Averant at DVcon. Most people thought they were
out of business. I was surprised that RealIntent was only represented
by a paper.
- James Lee of the ASIC Group
We use Verix from RealIntent to detect metastability and coherency
problems that arise when signals transfer across asynchronous clock
domains. It is easy to run, and the graphical user interface is very
helpful for debugging with color coded clock domains and signals. I
also like the text reporting for sorting on warnings and errors
We have also used the automatic checking (Implied Intent) feature which
uncovers potential problems in our RTL code, such as "dead code",
"pairwise FSM deadlock", "bus contention". We have written some
assertions for testing the formal verification part of the tool, but
this is not a part of our design flow at this time.
- Tom Paulson of QLogic Corp.
We have Averant. They have their place in the hierarchy. Now that
proprietary languages for these tools have been eliminated as the
entry point, I believe they should grow.
- Winston Worrell of Microsoft
We are using Magellan, as all model checking technologies they have their
pros and cons. Magellan works very well on protocol checking, that's the
way we use it in our verification process.
- Remi Francard of STmicroelectronics
@HDL, then RealIntent.
- Carl Harvey of Cirrus Logic
Definitely Magellan, tried Averant, in future 0-in.
- Umberto Rossi of STMicroelectronics
Planning to evaluate Magellan.
- [ An Anon Engineer ]
A "bug hunter" like 0-in Confirm is very useful to check if there is
another similar bug in your design that has modified due to bugs in
simulation-based verification. (We're using 0-in.) Confirm's
supported design style by formal verification is still not enough.
In almost cases, we had to modify our target design to apply it. For
example, asynchronous latches, clock selector and so on.
- Satoshi Kowatari of Fujitsu
We have bought 0-in, but other than Checklist haven't use it much, yet.
- Tomoo Taguchi of Hewlett-Packard
We use RealIntent clock crossing and automatic checks tool and are very
happy with it.
Positives:
- Verix divides clock crossings into data and control signals which
makes it much easier to debug.
- Very stable and quality results
- excellent support
- we were able to catch parallel case and full case pragma violations
which were almost impossible to catch them in simulations
Negatives:
- the GUI is useless
- the run times are on the longer side.
The tool does a very good job of finding bugs. It does a complete job
of identifying full_case/parallel_case pragma violations.
- [ An Anon Engineer ]
We use 0-in. We got started a little late in the process so our
designers didn't put the assertions in as they were designing. We've
basically used the 0-in tools (Search, Prove and Confirm) to check very
well known structures like complex arbiters and memory interfaces. We
found and fixed a few bugs (under 5). In cases where we found bugs late
in the verification cycle through simulation or on our FPGA emulator, we
have used the 0-in formal tools to reproduce the bug, then ran a more
complete analysis to verify no additional bugs existed.
- [ An Anon Engineer ]
Under evaluation. Most promising candidates are Averant, RealIntent,
Cadence-Verplex and an inhouse tool by Infineon.
- Andreas Dieckmann of Siemens AG
We're currently designing ASICs in the order of 3 million gates. We
are using the 0-in Search tool to perform formal verification using both
custom and library assertion checks. We have been using it for about a
year and we are still working on exactly where it should fit into our
design methodology. But we have recognized that it has some powerful
capabilities to find bugs. Our prior test methodology found all but a
handful of bugs. So we targetted it mostly at hot spot areas where it
is harder to guarantee by simulation. 0-in Search has proved its worth
in finding several difficult bugs. But we are also still struggling
with learning how to identify hot spots where a bug may exist and how
to constrain the logic so Search is able to explore enough to find a bug.
An example of a bug that it found was in a flexible arbitration
fairness scheme that we implemented. The 0-in Search tool helped us
find a corner case where for one clock cycle a channel's fairness
priority was incorrectly restored. This was not discovered during our
other verification because it was a rare performance issue that did
not break functionality. But the performance issue did break the
guaranteed access assumptions that the arbiter must provide.
- [ An Anon Engineer ]
Use Synopsys Magellan. Little useful because it needs lot of time.
- Luo Min of Northwestern Polytechnical University, China
We like RealIntent tools and we do use it in our flow. After 2 years we
decided to continue to use this tool due to it's efficiency in finding
bugs. In some cases RealIntent bugs we could not have found in any
other way using our other tools.
- Yuval Itkin of Metalink Broadband, Ltd.
To the best of my ability to tell, most of these tools are either
"smart lint" tools or assertion checkers. By the time you're done
investing the time and resources to learn the tool and code the
checks, you could have done most of this yourself in Verilog,
either home-grown or using OVL. And then you don't have a licensing
or $ issue to deal with.
- [ An Anon Engineer ]
0-in good/very good for limited usage. Megellan - too early to say if
it worth the time/$, however the idea is promising.
- [ An Anon Engineer ]
Currently investigating 0-in and Jasper. We think it will be a useful
tool to improve verification and catch bugs earlier.
- Terry Doherty of Emulex Corporation
We don't use "bug hunters" today.
- Maynard Hammond of Scientific Atlanta
We are starting to use 0-in. We did an eval that compared Magellan and
0-in last year. I really liked 0-in, it clarified a bug we knew we had
but could not reproduce in simulation. 0-in showed us we misunderstood
a bug. I also used 0-in to reproduce a bug found in the lab by writing a
couple of assertions to match the lab environment, ran the formal tool
and found the bug in a half hour with no real thought or effort. I
actually did it during a meeting. A functional simulation may have
caught it in 8 hours.
- [ An Anon Engineer ]
Tools like 0-in and Magellan are looking very interesting. We'll
probably try to use them once we'll have some assetions in our RTL.
So we'll start by using assertions for simulation and once it's there,
try them with formal proof.
- Laurent Claudel of Wavecom
IMOH, busy work to some degree, but depending on the project - useful.
For us, the jury is still out on 0-in.
- [ An Anon Engineer ]
You get out of "bug hunters" what you put into them. That is, if you put
few assertions in your code, they're probably not worth the price tag and
learning curve. On the other hand, if the RTL designer puts in generous
amounts of assertions, I'm optimistic they will prove valuable. I have
to admit that we have yet to try any bug hunters precisely for the reason
that we have yet to spend considerable effort putting in assertions!
- Dan Steinberg of Integrated Device Technology
I like Verplex BlackTie to check the quality of RTL we integrate. I
think its an excellent tool. Someone did an assesment in Moto USA and
said great things about Magellan, so it is being used by another team
here. Their intial assesment is that Magellan in not great, but its
a new tool and perhaps the limitations is theirs not Magellan's.
- [ An Anon Engineer ]
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 ]
We evaluated formal verification tools (0-in/@HDL etc.,) and found them
very hard to use and very buggy and these tools are still in their
infancy... I think it is just busy work, works well for smaller design.
Once we exposed them to some harder designs they just hung for couple of
days doing nothing and that design was not even our complex design. But
we were able to use some simple features, such as detecting a missing
synchronizer, etc.
- Subbu Muddappa of Woodside Networks
I see this as a promising area for the future of verification. We've had
0-in visit a few times, and we've talked to our Synopsys AE about Ketchum
a few times as well. Our decision on where to go with an assertion
language will probably determine where we go with this. We're leaning
towards SVA, so Ketchum is in the lead. A shift away from spending
months and months of time writing directed and semi-random tests towards
a more efficient approach involving assertions keeps me hopeful.
- Jonathan Craft of McData Corp.
Busy work, I don't trust them.
- Doug Hester of Chip World Consulting
Do not use at moment.
- [ An Anon Engineer ]
They are useful, but depends on the technique. Jasper's technique allows
you to get to the end of a state space, but you may well exclude useful
stuff along the way, so is a touch limited. @HDL and Averant's Solidify
are full static formal tools; we use an in-house one. Complementary to
random techniques, but you need to take care where you use it. Full
static tools can explore the full state space of a given problem, and we
have found them very good for bus bridges and similar designs. We can
ensure that within a set number of cycles after reset, there are no bugs
for a given property. You can then use random techniques to explore the
state space which is too deep for formal.
- [ An Anon Engineer ]
Never used them. We could never justify the time & money for somebody
to go chase these types of bug hunters.
- [ An Anon Engineer ]
Starting to experiment with these property checking tools. Using the
0-in static tool.
- [ An Anon Engineer ]
We don't use these tools. Maybe we will eval them in next 6 months.
- Gao Peng of Tongji University, China
I think you mean 0-in's CDC v. their property-checker, right?
We're evaluating it now.
- [ An Anon Engineer ]
Not used.
- Michiel Vandenbroek of China Core Technology Ltd.
These are a waste of time. Unless you have resources to burn they are
not too useful. They are good ideas but hard to use.
- [ An Anon Engineer ]
I have used 0-in:
- to verify internal interfaces.
- to prove that certain (illegal) conditions cannot exist.
- to verify state machines.
- to verify Arbitration schemes.
- to monitor for over/underflow conditions.
0-in monitors:
DDR - to verify the protocol.
I got from using 0-in:
- it found hard to find corner cases not found by simulation.
- verified the DDR interface.
- proved that some illegal conditions could not exists.
- verified the soundness of arbitration schemes.
- proved that over/underflow conditions did not exist.
- verified that internal interfaces operated in the expected manner.
The biggest problem is how to use 0-in effectively. How to write good
checkers? Where to place checkers for optimal results? What to check
for? Once we figured this out, we loved it.
- [ An Anon Engineer ]
0-in has the deepest understanding of this field and the most mature
tools. Unfortunately we're a start-up and their tools cost more than we
can afford! For now we'll concentrate on simulation-based verification
using assertions, and hope for the best. Assertions are extremely
helpful for debugging a design. But most companies are still in the
education phase on that point.
- [ An Anon Engineer ]
Never used "bug hunters". Not a huge fan of assertion languages. If
I needed assertions I would just build them into my testbench in the
native language.
- Jerry Roletter of ATI
Not used.
- Chandresh Patel of Ciena Corp.
We tried 0-in early on, but got burnt. We haven't been back.
- Mark Andrews of EFI, Inc.
We have 0-in for ASIC design. I plan on using it in our next FPGA
project. I believe the libraries that come with System Verilog
will be very useful.
- Don Monroe of Enterasys Networks
Don't use.
- [ An Anon Engineer ]
Don't know them, not considering them either. Probably waste of money.
- Sandro Pintz of Precision IO, Inc.
It's seems to be future trend, but I don't see sim based verifcation
going away. Not yet, under evaluation. It will be very useful and we
can see the benefit of using assertion already for debugging. There
are also condition that's not observable from chip I/O or MPU register
acess which assertion can flag problem instead we have to eyeball it.
I think it's powerful to compare to original VHDL assertion but haven't
figure out how to debug them.
- Hsing Hsieh of Hitachi
We are very intersted in model checkers, but are currently not in the
position to adopt them at this juncture. I've used Verdict in the past
with some great results, and strongly believe such tools should be
adopted. Capacity, ease of use, and cost are the major road blocks that
impede our adoption of these tools. I believe we will be looking at
them seriously within a year, however. We currently use OVL.
I strongly recommend we consider (or reconsider) formal model checkers
for our future design projects. These tools are expensive, however.
TransEDA claimed to be the discounters of model checkers and their tools
were about $50k. They also have AMBA compliance tools, by the way. Some
of the other vendors sound like they have some interesting bells and
whistles in their model checkers to ease the "environment" creation.
- Jim Lear of Legerity
We have looked into 0-in, Jasper, Magellan. We're not buying any of
them. I think that says it all. I have used Averant before and liked
it for targeted tasks. I think Magellan has the most promise going
forward, since it works well with language-based assertions in a formal
context.
- [ An Anon Engineer ]
We went for @HDL @Verifier for PSL static functional verification but
holding it till the PSL next version get approved from Accelera. My
vote is for PSL as lot of EDA vendors are supporting it and can be used
for both static and dynamic functional verification. Also PSL can be
used for functional coverage.
- Jithendra Madala of QuickSilver Technology
I know little about the bug hunters.
- Bill Dittenhofer of Starkey
We don't use this yet but this is a GREAT type of tools (FV). Used
this in previous company - you did not mention the BEST one,
IBM RuleBase. It uses PSL, great in catching many bugs very fast.
Assertion languages are important. Libraries are a waste of time.
They never fit exactly to your needs and you end up writing you own
assertions.
- Boaz Ben-Nun of Starcore DSP
|
|
