( DAC 02 Item 9 ) ----------------------------------------------- [ 9/10/02 ]
Subject: Tempus Fugit, Innologic, Veritable, Obsidian, Novilit
STRANGE OR NEW OR BOTH: Innologic lets you turn your Verilog simulator into
a symbolic simulator (whatever that is.) Newbies Tempus Fugit & Novilit let
you do protocol checking on your design. Tiny Veritable sells property
checking. Obsidian generates random test vectors for processors
"Innologic sells a PLI that will turn your ordinary Verilog simulator
into a symbolic simulator and can also add formal verification
capability. In addition to signals taking on values of "0", "1", "X"
or "Z" they can take on any arbitrary string as a value. If you have
an AND gate and the inputs are "0" and "1", the output is "0", just
like an ordinary simulator. If the inputs are "A" and "1", the output
is "A". If the inputs are "A" and "B", the output is "A&B". If you
have a lot of symbols, signal values can turn into big, ugly equations,
which can get uglier with each new clock cycle. They say their formal
verification tool will give you the simplest possible example of how
an erroneous value can occur. They say they use very clever BDDs to
allow signals to take on really big equations as values, but if you use
enough different symbols for enough clocks the tool will run out of
steam. Note however that since you are checking for all possible
values of the pins with symbolic values on them, your simulation may be
much shorter to effectively check your design. They say they can check
a RAM in only four cycles (two write, two read). Anyway, they got a
lot of attention last year but this year most customers aren't actually
using them for symbolic simulation. However, they say that because
their simulator is symbolic, it is much faster and more memory
efficient than other simulators (something about not having to uniquify
instances - don't see how that's possible). They claim to be able to
simulate scan vectors on 50M gate designs. This field interests me; I
can't decide whether 1. symbolic simulation is useless for anything
other than a few highly specialized things like memories 2. symbolic
simulation is useable for a lot but is perhaps too hard to use, and
maybe waiting for someone to make it easier (like what happened with
model checkers) or 3. symbolic simulation is useable right now but no
one is explaining it properly to the designers. Innologic also has a
symbolic switch level simulator that would allow you to compare a SPICE
netlist to a Verilog model, but without having to do pattern matching
on the SPICE netlist like Verplex, etc. do to decide what function is
being performed."
- John Weiland of Intrinsix
"Real Intent, Innologic seem to be good."
- Jai Durgam of SiImage
"Tempus Fugit
This company built a formal analysis tool, but appears to be marketing
it strictly as a protocol checker. They make some interesting claims,
such as they will find errors that cannot be found in simulation. I
am not sure how that might be, and I didn't get an explanation that
I could understand.
At any rate, they sell a bunch of assertions for any number of busses,
and the claim that their assertions will provide 100% compliance for
any of those busses. Tempus Fugit targets SoC projects that have
protocols. Since it is a formal tool, it must be a white-box design,
which means that purchased cores are out. Oh yea, you have to buy
their formal tool, too."
- Andy Meyer of Zaiq Technologies
"Tempus Fugit: Tempus Quest.
From what I understood Tempus Quest works as follows:
Input: RTL design code + a monitor (e.g. PCI-X)
Action: It checks if the RTL works according to the monitor
rules using static analysis (line coverage, state machine equivalence).
You can add properties to be checked, and it has a neat GUI for showing
the problems.
The company provides the "monitors" (as in reference models). Monitors
are written in Verilog + specific constructs, which gets us to a small
problem: you cannot reuse reference models that you might have.
Tempus Quest is a very dedicated tool, easy to use considering that
they provide the monitors, they provide the tool. What remains for you
to do seems rather straight-forward.
There are many ways to find bugs. I wonder how a comparison between
Tempus Quest and a SAT solver (zCHAFF, Prover) would look like? Not
from the methodology point of view, I know that, but from the price,
efficiency, verification time. I won't forget to ask next time."
- Monica Farkash of IBM
"Tempus Fugit targets at standard interface IP. I think this is useful,
but now they seems not to use standard language like Sugar. The most
important tools are NC-sim (can read SystemC in the future) from
Cadence, and BlackTie (can read Sugar in the future) from Verplex."
- Zenji Oka of Ricoh
"Obsidian Software sells a tool to that creates random and directed
random tests for processors. They also sell versions aimed at specific
cores, in case you are buying a core and modifying it slightly."
- John Weiland of Intrinsix
"4.2.8 Veritable Verity-Check
Veritable is a small company. Their tool currently does not support
VHDL. It uses their own language to define properties/assertions
but they also will support the Accellera standards. The tool also has
some built-in automatic checks like
- State space search (bus conflicts, floating bus, set-reset
conflicts, one-hot, ...)
- Race detection (combinational loops, clock gating, ...)
- Design reuse methodology
- Synthesis checks (latches, ...)
- Testability checks (asynchronous resets, ...)
- Net-list checks (range violations, redundant logic, conflicting
assignments, X-assignments, ...)
They have their own waveform trace and editor tool; the editor can also
be used to define properties."
- Raimund Soenning of Philips
"Veritable sells a property checker with both built-in and programmable
checks. They claim it has a wider range of checks than other tools
and is like a combination of Atrenta Spyglass, Real Intent, @HDL plus
some other things (I'm just repeating what the salesman told me). It
does testbench generation from formal properties to exhaustively cover
all properties (sounds familiar). They say you can specify the
properties in a GUI without needing to know a language. They have
endorsed Sugar and CoDesign's Superlog, but they don't support either
yet."
- John Weiland of Intrinsix
"newbie Novilit
Input: a communication protocol written in CMDL (a non-procedural,
declarative and object-oriented high-level language).
Output: the interface implementation (C, C++, Assembler, synthesizable
VERILOG or VHDL).
It is a dedicated tool, sorry to cut short your enthusiasm, it is for
communication protocols ONLY. You're lucky if it fits your job
description, we, the others, have to wait."
- Monica Farkash of IBM
"Novilit sells a tool for developing hardware for communications
protocols. You represent your communications protocol in their own
language, and it will spit out RTL, assembly language or C, for
implementing it in hardware, firmware or software. They already
have descriptions for 50 common protocols. I didn't completely
understand the product, but that's usually a good sign; it means
it's something new."
- John Weiland of Intrinsix
|
|
