( ESNUG 407 Item 1 ) -------------------------------------------- [02/26/03]
Subject: ( ESNUG 405 #6 ) 0-in, Averant Solidify, Real Intent, Tempis Fugit
> We used Averant's Solidfy briefly a year ago. Their property language was
> very powerful, but the tool failed to deliver results. It is very easy to
> write complex properties for easier checks with the language. This made
> the tool spend days without any results. Finally the design engineers
> gave up on using Solidify.
>
> The reason I want to be anon is because, I am evaluating Real Intent and
> 0-In automatic checks. I am afraid that my opinions might be not based on
> all facts. But at the same time, I would like to know what others are
> thinking.
>
> - [ Curious George ]
From: Anders Nordstrom <wolf=andersn pack=ellipticsemi wrought prom>
Hi John,
Curious George learnt one of the issues with formal tools very quickly. It
is annoying to debug thousands of warnings or false errors. It is not
enough with one tool to get the full benefit out of Assertion Based
Verification (ABV). The result from a formal engine is limited by the
quality and completeness of your properties. If your properties or
constraints specifying legal inputs to a block are too restrictive, you're
limiting the state space the tool can explore and, as in Curious George's
Averant example, the tool will not find any violated properties.
On the other hand if your properties are less restrictive and allow illegal
input combinations, it is very easy to incorrectly find a property violation
that you have to debug.
I have used 0-In's tool suite which uses both simulation and formal
verification and it has worked very well. I have found real bugs without
having to debug false errors from the formal engine, 0-In Search.
On my previous chip, 0-In Search found a bug in a FIFO controller where the
last word of an Ethernet frame was overwritten if a new frame arrived at
the same time as a down stream FIFO was full and the frame size was
incorrect, but the CRC for the frame was correct. A formal tool would never
have been able to explore enough of the state space to find this bug if the
constraints had not been debugged and verified in simulation.
Right now I am working on a new design at Elliptic Semiconductor. We
currently use 0-In's Checklist and Check tools. Checklist finds simple
problems like un-driven logic, incomplete sensitivity lists and un-connected
ports, but the real power of the tool lies in the more complex checks for
multiply driven registers, duplicate case items and clock domain crossings.
(Of course I can find all these things in simulation but I will be spending
a lot more time debugging them there.) Checklist also checks the syntax of
the assertions in my design so I know they are correct when starting my
simulations. We plan to use 0-In Search in the future but right now we're
busy writing assertions and simulating them and we will do that as long as
we find bugs in the design and our assertions need refinement.
On a related note, if you can get them, pre-written properties for standard
protocols are a great time saver. 0-In has monitors for a few standard
protocols that work for both simulation and formal analysis. It is enough
work to write a bus interface; writing a checker for it can take as long as
the actual design. I guess that this is a pretty large market. Synopsys
and Denali have pre-written checkers as well. If you only want to run
simulations you can mix standard interface monitors from different vendors,
but then you won't get the benefit of using them as constraints for formal
analysis. If you plan to do formal verification as well, your best bet is
to get the monitors from the same vendor as the formal tools.
- Anders Nordstrom
Elliptic Semiconductor Ottawa, Canada
---- ---- ---- ---- ---- ---- ----
From: James Lee <goldfish=jml bowl=asicgroup naught brawn>
Hi, John,
In response to the "Averant Solidify vs Real Intent vs 0-in vs Verplex vs
Tempus Fugit" question, I have looked at most of these tools.
We use a simple white board approach to eval these tools. We look at the
spec for the design unit we are interested in checking, then we write a list
of properties or assertions we want to address. We then reference the
automated checks that the tool implies from the RTL and cross them off. We
attempt to code the remaining checks in the property language.
Going through the tools in the order [ Curious George ] used:
Averant Solidify -- I have not looked at it in about 2 years. Two years
ago it lacked "implied intent" or "automatic assertions". Their property
language was awkward to use and we had difficulty with every property we
attempted to write.
Real Intent Verix -- We have the most experience with Verix from Real
Intent and find that typically 2/3 to 3/4 of the properties we write on
the initial list are covered by "implied intent" or "automatic
assertions". The list of automatic checks increases with each release.
I give the tool a big thumbs up since the implied checks do the vast
majority of the work. My pet peeves with Verix are - Default Cases, if
you have a default case that can never be entered but do not set every
thing to "x" but instead set everything to the default state you get a
message that the default can not be entered. We would prefer to be warned
when the default is possible to enter. State depth, if you have a state
machine with a counter that delays states for a large count is causes
state explosion and the tools dies (see my example later). Verix also
has issues with intra-assignment delays on non-blocking assignments.
These yield warnings during the compile stage. Our style guide requires
delays on all non-blocking assignments used for sequential logic. Just
like the default case, we want to reverse this message and warn when one
does not exist. They also lack Verilog 2001 support. We are rapidly
updating our style guide to use ANSI port declarations and these are not
yet supported by Verix. In fairness to Verix, let me point out that I
have seen many other tools including Cadence's HAL that warn about the
delays and all the formal tools die with state explosion.
Tempis Fugit -- We looked at Tempus Fugit in its pre-Alpha days so I do
not have up-to-date information on it. However, the strength in the tool
lies with the "IP" they have created for checking standard bus protocols.
The strength in these types of tools is in two basic camps. The automated
checks the tools imply from the RTL and the "IP" available with the tools
in terms of "canned" checks for known protocols
Since the ESUNG readers are always hungry for the dirt, let me give you a
test case that will break all of these tools.
The design: a UART with built in bit rate generator.
The properties: the data that goes in parallel should come out serially
in the proper bit order. Add a parity check for good measure. The
length of all the bits should be the same (i.e. it should not be possible
to change baud rate while sending a byte.)
This will break each of these verification tools due to the bit rate
generator causing state explosion. The tools will handle the 10 or so
states of the shift register, start and stop bits, and parity, but the
counter feeding that for the bit rate will, in my experience, make each of
these tools give up and not see the state machine.
We may later re-evaluate Tempus Fugit, Verplex, Spyglass and Solidify. And
I hope my competitors will continue to use only simulation to verify their
designs!
- James Lee
The ASIC Group Fremont, CA
|
|
