( ESNUG 428 Item 4 ) -------------------------------------------- [04/28/04]
From: Ulrich Hensel <ulrich.hensel=user domain=amd spot calm>
Subject: Ulrich on 0-in, @HDL, BlackTie, RealIntent, Cadence FormalCheck
Hi John,
Over the last couple years we have looked into 3 areas of verification that
may be of interest to your survey:
- Assertions for simulation
Here we are especially interested in that both design and verification
engineers can easily insert assertions into their Verilog code.
Assertion insertion shouldn't take a specialist in temporal logics.
Moreover, we were looking for some improved in code coverage metrics
(above normal code coverage).
- Structural RTL sanity checks, especially clock domain checks.
- Formal verification, reusing a properties from 1,2
Here is our user/evaluator experience. This a private opinion and not
an official statement by AMD Saxony.
0-in
----
Currently we are using 0-in assertions within simulation. 0-in assertions
are written both by design and verification engineers. We are quite happy
about that. We were also quite happy about the stability of 0-in tools,
0-in support, training, and responsiveness.
The 0-in checkerware library contains a lot of checker blocks that try to
speak designer language in contrast to being just temporal logic checkers.
The complexity of the checkers varies from a simple assert to a complex
arbiter or multi clock fifo.
In the beginning, we were quite enthusiastic about the complex checkers,
we hoped that we can use one checker (a couple lines of 0-in code and
switches) to get rid off of many low level checks within the RTL code and
the verification environment.
The reality is that maybe 90% of our checkers belong in the "simple"
category. The simple checkers are easy to understand and don't come
equipped with more than 5 options. Employing a complex checker took
much more time. We had to use all options and play some tricks to make
them fit (who is doing just standard FIFOs or arbiters after all?)
Once they were in the code, they were also the hardest to maintain.
Nevertheless, a successfully instantiated complex checker provided many
additional checks at once and also meaningful coverage information
(e.g. on FIFO watermarks).
Considering the cost of the 0-in tools we are also looking into free
OVL. The majority of checkers (the 90%) could be written in OVL, too.
So if you don't care for complex predefined checkers and additional
coverage metrics then OVL is a good choice too.
@HDL and 0-in
-------------
Regardings clock domain checks we have looked into the tools of @HDL and
0-in (and formerly also in to Avantis tool cdc). In the beginning, it has
been quite hard to communicate the clock domain checking problem to EDA
vendors at all.
The @HDL tool was basically the first usable clock domain checker on
the market. Its biggest plus is the good GUI debugging capability when
a clock domain crossing problem has been detected. Saying this, their
engine couldn't cope with some of our synchronization schemes. Thus,
the tool produce quite some false negatives but also a few false
positives. Moreover, once we had purchased, the @HDL support dropped
dramatically...
The 0-in folks came in later with their tool Checklist. We have a good
impression of their checking engine. They were listening to our problems
and implemented checkers for our synchronization problems. Undesired false
negatives (e.g. when collected control signals into a bus and synchronizing
each of them with a double flip flop) can be solved with simple additional
constraint. Their ASCII error reports are better than @HDL, however, their
graphical debug support is quite poor.
They make a big point about checker propagation (e.g. stability conditions
on a bus) to simulation, and actually, we love this idea. However, we have
never used this goodie within our flow.
0-in, BlackTie, RealIntent, Cadence FormalCheck
-----------------------------------------------
Regarding formal property checking we had a very close look into Cadence
FormalCheck (this is probably very dead now), the Infineon tool CVE, and
0-ins Search and Confirm. We also looked, from a distance, at BlackTie,
RealIntent, TNI Valiosys, and Averant.
We decided to stop investigating BlackTie, RealIntent and Averant (in
Spring 2002), because they couldn't provide support for Central Europe.
This may have changed now. In general, employing a formal method in the
design flow depends on vendor support crucially.
We struggled quite some time with the traditional model checkers CVE
and FormalCheck. Beside their commonly known capacity limits, it turned
out, that writing constraints to avoid false negatives is very time
consuming and difficult. It actually required a formal verification
specialist. The capacity limits forced us to work on such small sub
blocks that didn't even have a complete specification. On this level we
didn't find any interesting bugs...
0-in Search sits on top of your simulation. That is, you can run a
system level simulation and focus Search onto some sub block. The
properties are the same as used for simulation. The constraint problem
is much milder because you can constrain an input of the sub block to
follow the simulation stimulus. Search just explores an area of a
certain depth "around" the simulation, therefore it is not a complete
formal approach but doesn't suffer from the capacity limitations. You
can also start search from a specific time in simulation, avoiding
lots of uninteresting reset or config behavior.
0-in Search was the first formal tool (not mentioning equivalence checking)
that produced real, tape out relevant bugs (before tape out, luckily) that
were not detected by our simulation. We also like that a search constraint
(that is a checker marked as a constraint) runs as a normal checker in
simulation. That helps in validating the constraint itself. We found
that only a couple of search iterations were needed to add constraints
and achieve the "good" bugs.
0-in Search didn't make it into our mainstream design flow yet because of
its costly pricing model. We couldn't justify the high costs for an
"add on" tool that an applications to all blocks and full regression
would require.
Currently, Search experts apply the tool to suspicious areas only.
0-in also offers a complete model checking tool called Confirm. We also
looked into this. Confirm starts from a simulation state but then goes
far away from the original stimulus to violate the targeted checker. We
found that Confirm again suffered from the constraint problem, as we had
to put more and more constraints. Also, we couldn't find any bug on
top of the bugs already found by O-in Search. Therefore, we don't
use Confirm.
- Ulrich Hensel
AMD Saxony Dresden, Germany
|
|
