( DAC 03 Item 12 ) ----------------------------------------------- [ 01/20/04 ]
Subject: @HDL, Synopsys Magellan (Ketchum)
THE NEWER KIDS: It looks like this year, the Synopsys secret 0-in "me, too"
tool, Ketchum/FormalVera/Magellan, has actually for sure honest been released
for public use. Whether it'll catch on or not is another qwuestion. The
other newish kid in this 0-in "me, too" space is @HDL -- whose @ obviously
stems from the heady let's-impress-those-Internet-venture-capitalists days.
Annoying @ symbols aside, it looks like a number of verification engineers
had good things to say about @HDL.
Two years ago Synopsys had some super secret project called Ketchum that
had something to do with automatic test bench generation. Last year at
DAC they announced FormalVera, but it was never sold to the general
public. This DAC it was renamed again to Magellan, but it's still not
for sale (maybe 3Q). I certainly associate some vendors with vaporware
but Synopsys has not been on that list of late; they're generally very
concerned about only pitching what they can deliver.
Anyway, Synopsys said that formal tools are limited in how many clock
cycles they can look, and this technology is a way of addressing that.
They basically mix simulation and static formal checking. The tool
automatically derives assertions from your code (you can add your own
as well), automatically identifies promising states in the state space
that might prove or disprove the assertion, and automatically generates
simulation vectors that get to that state, then explore around it with
the static checker (for a maximum of maybe 200-300 clocks). The
simulator is like warp drive, and the static checking is like impulse
power. It's sort of like using warp drive to get to the next star
system and then impulse to explore it.
The Synopsys Magellan people contrasted this with 0-in, which also mixes
simulation and formal checking but requires the user to create the
vectors. Any bugs identified are verified via the simulator, to
eliminate false reports. If it is having a hard time getting vectors
that go to the desired state, it alters the random distribution on the
fly. If it can't prove or disprove an assertion it leaves a monitor for
simulation.
Magellan supports Open Vera, Verilog, VHDL and System Verilog. In a real
design of 7M gates, they said it generated 332 properties and in an
overnight run it proved or disproved 284 of them, and found 48 real bugs.
One of the bugs took 21,000 cycles to demonstrate. They said that
embedded RAMS can be a problem (state space explosion) so you may need
to black box them. They also integrate with Debussy.
@HDL sells a tool that sounds a lot like Synopsys Magellan. They claim
it has a better GUI and note they also do formal and structural checks
for clock domain crossings.
- John Weiland of Intrinsix
0-in keeps popping up at the top of my list for Assertion Based
Verification given their track record and well working tools. Synopsys
finally managed to get Magellan out and it is going to be interesting to
see how well they catch up since they have entered the ABV market with a
formal based tool really late. Jasper has a couple of things that makes
them interesting, Harry Foster of course and then a different use model
for verification.
Time will tell if it is harder to write the abstract model they require
as a reference or to write testbenches and use assertions.
- Anders Nordstrom of Elliptic Semiconductor
If you are talking of formal verification instead of LEC, then Magellan
(Ketchum) did catch my eye a little but have not felt any real need for
it. At least not from the Synopsys sales pitch I heard. Would like to
try out the tool, though. Not likely to happen in my company right now.
- [ An Anon Engineer ]
My evaluation of @Verifier is quite limited. I did not get the chance
to look into the rival products as, at Intel, we have our own internal
formal verification tool. Due to budget constraints, we decided not to
pursue any commercially available tool. Time constraints also forced us
to drop formal verification from our schedule.
What I liked about the @Verifier was the automatic property generation
and formal analysis of those properties. We found quite a few redundant
codes in our design. Our design was 15+ million gates and we
partitioned it into different functional blocks and ran the tool.
The negative aspect of @Verifier was its language. Over the last 2
years, we felt that @HDL support for the property language was changing
as the market changes its direction on adopting a standard languages.
Every 6 months or more, we were advised to preferably code the
properties in a different language as the industry was moving in that
direction. On some occasions, @Verifier would crash without leaving any
clues of what went wrong. This behavior is also found with other tools
though.
Their customer support was good and they were very keen on working with
us. In the beginning, the tool had a hard time accepting certain wierd
but legal Verilog syntaxes or constructs that our internal tool
generated. Those were fixed readily.
- Mohsin Ali of Intel
We are an ASIC design house that is supporting RTL handoff. In RTL
handoff interface, there are 2 issues. 1st is when RTL is ready to
final synthesis. We had spent time for synthesis iteration due to RTL
functional bug. 2nd is even if RTL release is pushed out, they want us
to keep design schedule.
To resolve these issues, we did benchmark of intent verification tools.
Our criteria was the following:
(1) Functionality
- Built-in and/or specifiable assertions.
- Analyzing capability for detected errors.
(2) Capacity
- Over million gates handling under 12 hrs.
(3) Error detection coverage
- Detected 95% or more functional errors.
- Report capability of untested RTL line number.
From the benchmark results, just @HDL @Verifier evaluator met this
criteria. We are now adopting @HDL products in RTL handoff.
- Yutaka Koike of Oki Semiconductor
Let me introduce our design. It is a TCP/IPsec/iSCSI transport offload
engine. It contains about 80 state machines and lots of arbiters. It
is very state rich and is not a typical design.
Frankly, we only have deployed DABV (dynamic assertion based verif)
methodology since it can be cost justified at reducing debug time. Our
evaluation of @Verifier was using this approach. We spent 3 months
converting our Real Intent Verix proprietary properties written at
signal, interface and protocol levels into Sugar/PSL 1.0. This was done
by a summer intern. I am now in the process of evaluating Cadence
Incisive and the Novas/Verdi/PSL offering and am quite pleased.
What I found from the @Verifier/@Designer evaluation is that @HDL was
about 3 months ahead of Cadence on the PSL implementation, but their
@Designer interface and debugger was very unstable compared to Novas
Debussey/nWave. We filed about 30 bug reports in about 2 weeks.
Granted this was in a 3 week period using beta code so some of this
should be expected. About 80% of the PSL 1.0 spec was implemented which
was quite impressive. Integration with the @Designer waveform viewer
and source code debugger was in its infancy. The one which we found
interesting was the Assertion Studio tool. This allowed designers to
debug PSL implementation of interfaces and bus protocols before
inserting into the design. No one has tools like this.
Traditionally, designers here have not done unit level sims and
testbenches because 1) they are throw-aways, 2) they are poorly trained,
3) they have little or no concept of verification and 4) they are
poorly managed. We chose to use Harry Foster's approach which forces
the designers to instantiate all standard interfaces (fifos, arbiters,
etc.) in the form of parameterized Verilog macros with PSL embedded.
Please see "Assertion-Based Design" by H. Foster, chapter 7 (Assertion
CookBook) page 211 to 268.
Last but not least, PSL can be used as a specification tool for the
generation of Verilog based "monitor" models. @HDL has tools in this
area. Similarly, the folks at IBM have a tool called FoCS and other
vendors have products in development. The Denali folks for example have
a form of golden reference model monitor models which emulates various
protocols in parallel with the DUT. This technique is quite powerful
since it complements PSL properties written at the interface and
protocol level.
- [ An Anon Engineer ]
We have been evaluating @HDL's Verifier. Here are some things that @HDL
can do for us that a linter or DC couldn't catch:
1. @HDL checks for deadlock states. This was useful for PVA2, but it
was mostly a distraction. We had many hundreds of lines of errors in
this check that were false errors. Designers here were using the
default state transition in their case statement coding style. @HDL
had trouble interpreting that, even though it was OK. The people
we've talked to from @HDL told us that bug has been fixed in the
current tool version.
2. Check for unreachable states. This @HDL check is useful to get an
early look at unreachable states in the RTL design phase. This can
and should be caught by a cover tool in the verification phase, but
it may be dropped by a 95% cover requirement (or whatever our cover
requirement might be). I think it's an important check in the RTL
phase.
3. Fast clock --> slow clock crossing check. The @HDL tool checks to
see that the FF driving from a fast clock zone into a slow clock zone
can not change on 2 clock edges in a row. If data does change on 2
concurrent edges, data may be lost in the crossing to the slow zone.
@HDL examines the logic cone into the fast driver and looks for
possible changes that would break this rule. We have no way to check
this in lint or DC or cover. Our only chance to catch a bug like
this is through simulation targeted at it.
4. Full case check. The full case directive tells Design Compiler that
there doesn't need to be a default path through the MUX. The
options list shown in the case statement is complete. @HDL verifies
that any unused select values can not happen. This is another
potential bug that we can only catch during simulation.
5. Parallel case check. The parallel case directive tells Design
Compiler that no 2 inputs to a case are asserted at the same time.
This saves gates in synthesis by taking the priority logic out. This
burned us in PVA2, but we caught it late in simulation and generated
a new netlist. @HDL checks that the inputs to the case statement are
mutually exclusive. These are things that we can do with our other
tools, but that we could do much more efficiently with @HDL.
6. Automatically check for correct synchronization across clock zones.
@HDL checks the synchronization paths and verifies that they are
good. One of the checks are that there is no logic between the
metastable FF and the sync FF in a 2 clock sync circuit. We can
check all the sync paths with DC and Perl scripts on the netlist,
but it is much easier to have this automatic check.
7. Check for asynchronous inputs to clocked processes (always loops).
@HDL outputs a warning when a clocked process is receiving a signal
from another clock zone. @HDL also color codes all the clock zones
in the RTL so it is easy to see when a signal is used that is not in
the process clock zone. Asynchronous inputs can be checked using
Design Compiler, but this is a much more efficient way of doing it.
I could verify all async input using DC in 2 days. I could probably
verify all async inputs using @HDL in 2-3 hours.
8. FSM state diagrams. This is a nice design feature that helps
designers and design reviewers to see all the state transitions.
- Jason Franklin of F5 Networks
I am using @HDL for mainly two purposes:
(1) exploit their structural analysis,
(2) use @Verifier as a convenient vehicle to verify Sugar 2 (PSL)
assertions with the IBM RuleBase engine (or a similar tool).
We are also using IBM RuleBase tool directly, but it is less convenient
than using it through @Verifier.
The only other tool we have (very briefly) looked at was 0-in's, and we
feel that there is no substantial difference in their capability of
verifying PSL assertions. However, we haven't really tried it, so we
don't know for sure.
- Ran Ginosar of Technion, Israel
@HDL features I liked.
- Gangadhar of DigiPro Design
My info comes not from DAC, but from an in-house evaluation of @HDL's
@Verifier a few months prior to DAC.
After about a one-year tool evaluation hiatus (brought on by both project
pressures and a reduced budget) we began looking at a few tools a couple
of months ago. One that I spent a good deal of time with was the @HDL
tool @Verifier, the cross-clock domain checker.
It comes as an additional feature on top of @Designer which has RTL
linting capability as well as other types of "design rule" checks (not to
mention a waveform viewer ala Debussy). We were interested in the cross-
clock domain checks to begin with, but these other features are of
interest as well. We evaluated version 3.0 in various patch levels.
Setting up @Verifier isn't bad at all. A field engineer from @HDL did
most of it for us, but I could have done it myself with only a little
additional ramp-up time. Most library constructs are understood (it uses
the Verilog simulation library), although some UDPs needed simple
behavioral models built. The memory models we had were quite complex, so
I made some simplified ones for @Verifier. Once that was done, we made a
couple of black boxes for complex hard macros and we were ready to begin.
First step was clock identification. This is very simplistic; every net
that hits a synchronous endpoint is considered a unique clock. Once you
have a report of all of the clocks, you set up the clock info file that
defines the main clocks and all of these gated/generated clocks become
"synonyms". This was straightforward enough, even on our design which
has numerous recovered clock domains and PLLs.
Now @Verifier can begin its analysis. You tell the tool if you have some
sort of required synchronization strategy (specific module/cell, two- or
three-flop, perhaps others as well) and tell it to go. It's very fast;
just a few minutes on our 1.2M gate design.
If your design uses a lot of "config registers" which are not
synchronized but are considered okay, you need to tell the tool about
them or else it'll flag them. We let it do this, and then put the known
"static" flops into the "config register" list. More on this later.
The interface is pretty easy to navigate through, and cross-clock domain
paths are shown to you in your RTL source code. Netlist tracing is done
in @Designer just as it would be in Debussy. The register/wire names are
colorized on a per-clock basis which makes seeing places where clock
domains are mixed easy to spot.
Since we want to use a tool like this in "regression" mode, I had a
problem with putting some registers into the "config register" area in
the control file. This is a "big hammer", affecting all downstream
endpoints. You could validate in one version of the design that all
places such a register was used were okay to mask, then change the logic
later such that one or more endpoints were true cross-clock domain
problems. You'd miss it unless you went back and built up the control
file all over again... yecch.
So I recommended to @HDL that they create a Synopsys-like point-to-point
exception capability. As of the final version we worked with, this
wasn't in there yet but they understood the issue I raised so I would
assume it's in there by now (or soon will be).
I found a few places in the code while I was using @Designer to trace
paths that appeared to be mixing terms from more than one clock domain,
but they didn't result in a violation at the endpoint register. I don't
recall how this one was resolved, but I do seem to recall that it was
dealt with in a patched release. They spun these very fast for us during
the eval.
Also, the tool is capable of recognizing some structures such as FIFOs
and applying special checks to those circuits. However, the recognition
capability is template-based which is very sensitive to the coding style
used. None of our FIFOs were recognized and there was no mechanism to
tell the tool they were indeed FIFOs. @HDL fixed some of the templates
and explained that the templates would get better and better over time;
seems likely but would remain to be seen.
Overall, the tool was very good at showing those cross-clock domain paths
that were missed. The linting tool was respectable, and a welcome
addition to the one we currently use.
As a note, we did not purchase the tool although those of us who
evaluated it wanted to; it was just a business decision. The @HDL people
were *terrific* to work with -- everything you'd expect from a small
company and more. Most bugs we pointed out were fixed very quickly and
they really listened when we talked about how we'd like to use the tool
and what they needed to do to make it work that way. The tool may not be
revolutionary, but it was easy to use and it brought together many types
of checks under one GUI. I would use in my role as both a designer and a
backend implementation engineer -- I found it very useful.
And one final note -- @Designer had some features in the waveform
viewing/simulation debugging component that were really great. We
thought it likely beat Debussy (which we currently use) but since we
didn't really do an acual evaluation of that portion of the tool, it's
just worth mentioning the feature here.
- [ An Anon Engineer ]
|
|
