( DAC 01 Item 18 ) --------------------------------------------- [ 7/31/01 ]
Subject: 0-in, Synopsys 'Ketchum'
SHHHH! IT'S SECRET: It's no secret these days with most users who read
ESNUG that Synopsys is quietly working on an officially unannounced product
that is, for most intents & purposes, almost a carbon copy of what 0-in's
been doing publically for years. OK, so there might be some nitpicking
differences -- but you'll have to ask Janick Bergeron what they are -- I'm
just a chip design guy, not a verification whiz. I'm told both Ketchum and
0-in both use Formal voodoo to 'search' for a design's unreachable states.
That's close enough for me. (DAC'00 #16 and SNUG'01 #23)
"Synopsys "Ketchum", Valiosys, and 0-in looked interesting. I think
the semi-formal approaches by "Ketchum" and 0-in are a good way to
get the old 'foot-in-the-door' in regards to getting the designers
accustomed to specifying simple properties about their design."
- [ An Anon Engineer ]
"THURSDAY: Extensive Demo with 0-in. 0-in offers two products 0-in
Check and 0-In Search. The first allows the users to embed assertions
into RTL code via metacomments. Then extract the assertions with a
pre-processor and then utilize these assertions during simulation.
Certain classes of assertions have functional coverage metrics
associated with them so a user can view the function coverage of a
given design element. In addition to user checks, they have a number
of assertion checkers for numerous industry standard interfaces like:
LPC, PCI-X, Amba, Infiband, SPI-4, Utopia,
POS-PHY, CSIX, Hypertransport, etc.
These checkers also collect functional coverage information about the
interfaces in question and will flag protocol violations.
Their second product, 0-in Search, is attempting to use formal
techniques to amplify existing tests the verification groups have
already written. This technology looks interesting. Its hard to
explain, so I won't try but I plan on evaluating this and seeing
if it can find bugs we are currently missing with Specman."
- Sean Smith of Cisco Systems
"Ketchum from Synopsys (under NDA)
2 main features:
Semi-formal automatic test generation (no checking)
- measures quality of coverage
- creates tests targeting areas of low coverage
- generates tests for hard to reach design structures
- has been tried on a 2.6 million gate design and on
DesignWare modules
Formal proof of properties and assertions
- assertions checked during simulation and/or through formal
verification
- supports simulation-based debug (stimulus generated to
demonstrate a failure)
- supports OpenVera and RTL for writing of the assertion checkers
- some checkers generated automatically (full- and parallel-case)
- will add support for the Open Verification Library
Status: Working with pre-release customers, looking for beta partners"
- [ An Anon Engineer ]
"I have brief experience with 0-in. I do not like it. In general, I do
not like any tool which is based on comments put in the code. Code is
cluttered and everything is very much tool specific."
- [ An Anon Engineer ]
"I like the 0-in tool's ability to give designers a structured way to
put assertions in their Verilog. (Boy, am I starting to sound like
a SW person.)"
- Dan Joyce, Compaq Computers
"I have seen the 0-in approach a couple years ago, don't know what they
are up to lately. I thought their checkers were useful, but had
reservations about cluttering up my source code with vendor-specific
pragmas and they didn't have a lot of value in their checkers which
I couldn't have easily replicated in HDL. Not really sure what it
would take for me to pay real money for their tool, but it was
interesting."
- Tom Loftus, Intrinsix
"0-in: Saw them last year, has real potential but does not provide
exhaustive searches.
Synopsys "Ketchum": Late and very little new compared to what is
out there.
The biggest lie I found at DAC occurred in a demo for Ketchup. They
said that Synopsys is the only one attacking the problem of
constraining the inputs for a formal model checker. I admit they
have some novel ideas but not many and they will be late to market
with an immature product. There are problems with the Ketchum
methodology that others were talking about how to solve.
Real Intent: Tried them last year will probably bring them back."
- [ An Anon Engineer ]
"0-in: Our friends at Zero-In announced a joint deal with Synopsys
called reactive testbenches. The non-static checkers that 0-in
have can create Vera hooks to run and fire under Vera. Plan on
doing it with 'e' as well."
- Peet James, Qualis Design
"A flier from 0-in caught my eye the other day. I like the concept of
embedded assertions in the RTL code triggering error messages in
simulation. Adding assertions while designing the RTL seems easy
enough. They claim that once a simulation has been written their
tools can create more testcases that would attempt to break the
embedded assertions. I would be curious to know how much 0-In slows
down simulation time."
- Kristie Armentrout of Tektronix
"Synopsys/Ketchum
New technology for formal verification coupled with simulation. Aimed
at generating test sequences to exhaustively exercise all "reachable"
state combinations for a selected set of signals. Input is a set of
registers / signals to cover; N signals implies the tool must try &
generate sequences to hit up to 2**N possible combinations. Tool uses
directed random simulation to hit "easy" combinations, then uses formal
methods coupled with random sim to hit harder combinations. Tool also
capable of proving states unreachable, so in the end you get a report
indicating states able to reach (and the Verilog testbench necessary to
hit all those states), states able to prove unreachable, states unable
to reach which are still potentially reachable. Technology can be
used to drive design into corner-case situations unlikely to ever hit
with straight random simulation. Can utilize generated testbench with
traditional simulation monitors to find bugs. Synopsys used Ketchum to
find bugs in DesignWare 16550 UART that escaped detection by
conventional means. nVidia and Agere are early customers, claim some
amount of success with product. Expect technology to be formally
released by next DAC. One of the key engineering directors responsible
for productizing some of Synopsys' most important leaps (DC, PhysOpt)
is now heading up this team. R&D team is very talented, but problem is
very hard! Limitations: can be applied to blocks, not chips. A very
hard technical problem, easy to space-out (exponential state-space to
be searched.) Could be useful to apply technology to particularly
troublesome blocks (i.e., USB) which have lots of corner-case
conditions to exercise."
- [ An Anon Engineer ]
"There are currently 3 approaches to testing interesting corner cases:
1.) hand written tests which are difficult and costly,
2.) a shotgun approach based on directed random testing targeting
the area of interest, and
3.) semi-formal where formal methods are used to specify a test
that will reach a specific corner case.
Ketchum falls into the third category. The user defines the corner
cases of interest by defining target signals using a TCL interface.
In order to ensure the tests are realistic/implementable the user also
has to constrain the test environment. This approach allows the
verification engineer to focus on specifying what should be verified
rather than how tests should be implemented. It also makes the
methodology much more quantifiable than most verification which is
a big benefit to managers when discussing tape ship!
Currently Ketchum is Verilog only which may not be an issue in the USA
but matters for Europe. The tool itself still appears to be pre-alpha
meaning most examples are still being run in-house by Synopsys.
One important issue with Ketchum is capacity though exhausive state
coverage is less important than when doing formal verification.
Without hands on experience it is difficult to get a feel for the types
of designs it can handle. The example used during the DAC demo was a
UART with 23K gates and 2K registers. When running it could report
states reached, unreachable and those where status unknown.
The tool supports OpenVera Temporal assertions. I am not a fan of Vera
and believe in using open interfaces but Ketchum assertions can
apparently also be written in RTL. Ketchum assertions can be used as
properties and tests generated that provide counter examples. This is
useful to improve acceptability to designers. It's interesting to note
that the Ketchum team are trying to boost the tools abilities as a
model checker."
- [ An Anon Engineer ]
"I would not classify 0-In as a newbie tool and from what I saw on the
show, I think it is by far the most useful one. There were many 0-In
wannabe's and they fall short of what I can do with 0-In.
The wannabes seem to be aimed at replacing simulation early in the
design phase by replacing block level testbenches with written
assertions. Sure, that works but why? That is not what is slipping
my schedule by months and costing me a respin of an ASIC!
All these other tools help me find bugs that I know I have to look for.
What I want is a tool that finds the bugs that I don't even know I was
supposed to look for! Those are the tough bugs to find. With 0-In, I
get help to verify that the chip doesn't do any illegal behaviour in
normal mode and it also checks legal states outside of what I define
as normal."
- Anders Nordstrom of Nortel
"0-In
Design verification product line: Zero-In Check (with Checkerware
library), Zero-In Search, Zero-In View all bundled together in a single
tool suite.
Zero-in Check uses the Checkerware library of directives to provide an
easy way to add assertions (including pretty complicated ones, like
timing-dependent hand-shakings on a bus) to your rtl code. You need to
tag the constructs that you want it to go after, and it will insert
checkers. You then run simulations (on VCS for instance) and use their
GUI to see which checkers fired. You can also get a rough idea of test
coverage because the gui tells you how many times in the test suite
each checker's code was exercised, and what the checker results
were -- the amount of information delivered depends directly on how
well the assertion was coded though--it is not bullet-proof.
They call their strategy "white-box verification", marketing-speak for
the assertion-based nature, and attempts to cloud the fundamental truth
that Verilog assertions are free to everyone, and are commonly used as
part of a standard DV strategy. That said, their tool can really
simplify the coding of complex assertions. Perhaps most interesting,
the Checkerware library comes with a full set of bus monitors already
implemented, including LDT and DDR SDRAM amongst many others. Assuming
the bus monitors are good, they could be very useful and timesaving.
The Zero-In Search feature is supposed to "amplify" the power of your
existing tests to find and create new corner cases. I interpreted this
to mean that it automatically calculates and adds in timing delays on
relevant signals in order to create different paths through the code
and expose new bugs. This, of course, can be easily accomplished by a
good suite of randoms as long as one writes test to randomize the
correct signals timings etc. Again, they seem to have created a way to
make it a little bit easier to do something that we should already be
doing anyway.
They had testimonials from Sun, Tensilica and HP posted in their booth.
They said they've done designs of up to 20M Gates (!?) on a multi-
processor Sun with 1GB of memory. They have ported to Redhat ver 6.2.
We both thought this tool was interesting but more of a luxury item.
It would give you a way to standardize and sometimes simplify checkers
at the cost of the license fees & the pain of learning how to use it."
- [ An Anon Engineer ]
"0-Search by 0-In
----------------
It is a semiformal verification tool. It "performs formal analysis
surrounding the states that your testbenches simulate." At every clock
tick in a logic simulation, it analyses the logic cones in the design
and searches for violations of the user-defined properties in a legal
way. The purchase price is in the order of $100K. Leasing program is
also available."
- Henry So of Mobilygen, Inc.
"Zero-In & Real Intent
---------------------
Both companies provide the ability to instantiate very powerful in-line
assertion checkers as comments in the Verilog code. Zero-In uses the
assertions to perform what they call semi-formal checking -- they use
model checking to explore and "amplify" the existing test vector space.
Real Intent formally checks each assertion and they can generate
simulation-based Verilog monitors from the assertions. Both tools look
very powerful, and they both have an impressive array of customers.
Broadcom uses Real Intent, but I think I remember that Broadcom is also
looking at Zero-In. nVIDIA has both. ARM is looking at both.
In the next chip, we will explore the idea of designers instantiating
assertion checkers at coding time to assist white box verification
(internal verification, as opposed to black box verification, which
operates on the I/O signals only). I see tremendous power in this
method.
Of course, one problem we will have to solve is figuring out how to
use the assertions with MCL code. Both companies thought it could be
done using some sort of include-type file."
- [ An Anon Engineer ]
|
|
