( DAC 01 Item 21 ) --------------------------------------------- [ 7/31/01 ]
Subject: Averant 'Solidify', @HDL, Prover
YET ANOTHER FORMAL TOOL OR THREE: Averant, Prover, and DAC newbie @HDL
also presented their verification tools that all seemed to basically work
by comparing your design's spec to what you've actually coded in Verilog.
Again, all three appeared to have Yet Another Set Of Proprietary Asserts
(just like Verplex, 0-in, Ketchum, and Real Intent) added more credance to
Harry Foster's warning that all these N different proprietary asserts are
more 'part of the problem' than 'part of the solution'. Ugh. Anyway, if
you're willing to learn each and every new special language these tools
have, they're supposed to be quite good at finding bugs you wouldn't
normally see through olde-fashioned overnight testbench regressions.
"Here's my ten-second summary of my experiences to date with
Averant's Solidify. I've been using Solidify to verify mid-sized
(1000-input, 1000-output, few hundred thousand gates) combinational
logic.
Positives: it verifies RTL versus abstract properties, unlike
netlist-to-netlist verifiers like Formality. The properties are
easier to create than a Specman or Verilog testbench, and of course
once you verify the property, you have no worries about "coverage" in
your test vectors. When Solidify finds problems, the counter-example
vectors it produces are nicely pruned, and they pointed me right at
the problem areas.
The latest version lets Solidify see into the design's hierarchy
(earlier versions could only use top-level signals in properties), and
this lets you write hierarchical properties to verify circuits that
would otherwise be too complex for Solidify (or at least too complex
for impatient designers who don't want to wait a few hours for the
answer).
Solidify includes some very helpful, powerful builtins, like onehot and
onehot0 assertions.
The documentation includes a section on "Writing Efficient Properties"
in the "Advanced Modeling" chapter. Maybe everything I do is
"Advanced" (well, yes, of course, that must be it), but I'd put this
in a special "read this right now, do not pass Go, do not collect
Unnecessary Frustration" section. I found the hints here extremely
helpful.
Negatives: it's quite possible to create properties which Solidify
can't verify in a reasonable amount of time. Creating good properties
can require a little bit of ingenuity if your logic is complex.
Solidify's found bugs for me, and I've found it much easier and faster
than writing Verilog or Specman tests. Obviously with a thousand or
so inputs I can't very well run an exhaustive simulation, so it's been
very comforting to know that the circuit passes in Solidify."
- Martin Harriman of Tau Networks
"Solidify by Averant
-------------------
1. It is a "Static Functional Verifier". The only one in the world.
There may be distinctions between a static functional verifier and
a model checker. However, such distinctions are not obvious to a
user.
2. Properties are written in a proprietary language. They are kept in
a file that is separated from the design file.
3. Target block-level verification. It is unclear if it can handle
large blocks.
4. The associated diagnostic tools appear to be weak compared to
BlackTie and Verix.
5. Available on Linux/Intel."
- Henry So of Mobilygen, Inc.
"a) Veritable: Averant static checker type deal. Looks more formal
in nature. Called Verity-check. Mostly a state checker, but
also has race detection and linting-type checks. They had a
2nd tool, but I seem to have lost my handout. I remember it
too was worth a closer look.
b) Averant: Solidify. Static checker. Big news here is that the
list of real life success stories has grown. I think last
year they had one (Cisco). Tool looks much the same with
some improvements in the GUI area to aid in setup, coding
and debugging."
- Peet James, Qualis Design
"We are looking at Verix (Implied Intent / Expressed Intent) from Real
Intent. To us this looks like a strong competitor to Verplex's Black
Tie, not so much as a competitor to Averant's Solidify. Of course,
the Real Intent sales people disagree, especially as we are buying
Solidify. We will continue to look at tools in the "Static Functional
Verification" arena as we believe that there is a lot of potential
payback in this area."
- [ An Anon Engineer ]
"Solidify looked pretty good in the domain of single clock designs. Too
bad we and everyone else has a whole bunch of multi-clock designs."
- John Szetela of AMD
"We've done evals this year on Averant and Real Intent, and had Formal
Check (from Cadence) in for a demo. Averant had a lot of trouble
parsing my chosen design, and had to code up custom memories to
replace the LSI RAMs in the design. It was awkward to use, since
assertions needed to include all the control code which was already
in the design. E.g. 'if !reset && posedge CLK && state == 1 then on
next CLK state -> 2'."
- Jeff Deutch, Avici Systems
"@Verifier by @HDL
-----------------
1. Properties are described by Verilog PLI calls.
2. Released 6 months ago.
3. Automatically detect errors such as multiple state machine
deadlocks.
4. Available on Linux/Intel.
5. The purchase price is in the order of $75K.
6. Could not schedule a demo."
- Henry So of Mobilygen, Inc.
"At Prover, the interesting thing to me was that their approach came
from the software world of validation and they are bringing the core
technology to hardware side. The discussion was centered around the
fact that they have a proof engine that can be interfaced with a
parser on the front end and a display tool at the back end.
Conceptually, this appeared logical, yet the person in the booth
could not actually show me a demo (I wasn't interested in equivalence
checking demo he was prepared for). The discussion of the technology
itself was intriguing to see if there was a new business opportunity
there."
- Yatin Trivedi, Intrinsix
|
|
