( DVcon 05 Item 14 ) -------------------------------------------- [ 10/25/05 ]
Subject: Calypto SLEC
ALL THINGS BEING EQUAL -- One of the new verification tools I saw at DAC this
year was a stupidly named tool called "SLEC" from a company called "Calypto".
(EDA seems to attract people who don't know how to name tools well; with all
capital letters, "SLEC" sounds too much like "BLECK!" -- a sound people make
when they are sick. D'oh!) Anywaaaaay.... What BLECK, err... What SLEC
does is it performs sequential equivalence checking on RTL source code. That
is, let's say you create a piece of RTL that completely models a Transmeta
Crusoe processor. It has all the correct micro architecture, yada, yada,
yada -- but it chows power like a space heater. You go in and mess around
with your RTL to get your micro architecture consuming less power. So even
though you messed with registers and state machines, BLECK SLEC can (voila!)
magically check if your "original" and your "low power" Crusoe RTL models are
functionally equivalent. (Or so the Calypto people claim...)
But don't listen to me, listen to the users below:
I saw the Calypto SLEC RTL and SLEC System demos a few days after DATE
2005, and then had a more in-depth discussion with the Calypto guys.
These meetings occurred just days after my design team was struggling to
check the consistency between two RTL versions of our complex bus bridge,
where the second one was retimed. We were using a mix of register-based
formal check and dynamic verification, so the first things that got my
interest were:
1. SLEC's ability to check the two designs without losing itself
in a register-to-register comparison. Or giving it back tons of
"unmatched" points and meaningless logic cones.
2. Its ability to create a testbench/VCD with a counter-proof of the
mismatches without any testbench or formal properties as input.
You have to write a script to specify in which timing window you
expect the results of the retimed design. It seems easy to
capture the specs -- a graphic way to extract constraints would
perhaps help further.
I will be able to comment more on this aspect when I let my engineers try
the product with our designs, but from the demo it appears a valid method
and a brand new approach.
I have some concerns related to SLEC's one-bug-at-time flow (i.e. you have
to debug one bug after the others without having a kind of ranked list of
mismatches) but this probably isn't an issue since the debug flow would
still be quick with such visual counter-proofs.
I was impressed by Calypto's SystemC equivalence checker, "SLEC System".
I think this is the core of their technology around which they also built
up SLEC RTL. My understanding is that Calypto starts from a more
hardware-oriented SystemC, which I believe is the right point in the
design flow for me to start to use equivalence checking. They don't claim
that the tool can cross-check a very high transaction level SystemC
description vs. low-end RTL gate-level netlist.
The Calypto demo was with a relatively small design, so speed was rather
fast. I got from the Calypto guys the message that SLEC would be better
for compact sub-modules one-by-one.
After years of "dumb" equivalence checkers, I finally I saw something new
in SLEC, so I am asking my methodology team to proceed with an in-depth
evaluation of the tool.
- Riccardo Mariani of Yogitech Italy
The Calypto SLEC tool does sequential equivalence checking of two RTL
designs even when there is no state correspondence between the two designs.
We sometimes modify our RTL micro-architecture to get better timing or
power. This naturally creates a re-timed or re-powered RTL where the
state encoding or the number of registers between the original RTL and the
re-timed/re-powered RTL are different. (Traditionally we would use a
testbench, simulator, etc. to verify their RTL equivalence using some
targeted functional vectors, but this is incomplete and could lead to
false positives. SLEC is a formal check that eliminates simulation for
this purpose. It proves the equivalence between cycle-accurate or
transaction-level models.) SLEC allows us to verify that the functional
I/O behavior is preserved across these changes.
SLEC takes in 3 inputs:
- Original RTL (spec)
- Re-timed/re-powered RTL (impl)
- Configuration information (TCL file).
The configuration information requires the specification of the design
spec, design impl, and any boolean or temporal constraints on the inputs
to the two designs (reset sequence or specification of reset states).
Additional information about which outputs to check can also be specified
(default is all outputs). SLEC does not require an exact correspondence
between the inputs and the outputs of your designs.
SLEC has 2 modes of operation:
- Bug detection mode. Here they use the technique of bounded model
checking. In this mode, SLEC attempts to verify equivalence for
'n' cycles after reset. If it does not find a counter-example, it
deems the two RTL models to be equivalent. Note that under this
condition, there might be a bug lurking beyond the 'n+1' cycles;
however, I found this useful for finding bugs in the early part
of the design cycle.
- Full proof mode. This attempts to prove equivalence using induction
and model checking techniques, but can blow up if the sequential
depth is very large.
In our tests of SLEC the runtimes ranged from a few minutes to 4 hours to
"out of memory" runs, depending on the size of the models.
What we found about SLEC in our eval:
- The configuration setup (TCL interface) is simple.
- It doesn't support standard PSL and SVA assertions for specifying
input constraints. Instead it has its own syntax for temporal
constraints on the inputs.
- The front-end language parser (Calypto uses a third-party parser)
is separate from the back-end solvers, which enables them to support
any future system or HDL languages.
- It has formal engine solvers that combines SAT, BDD's and induction
engines.
- SLEC generates simulation testbenches for counter examples and can
generate VCD dumps (their own interpretation of the RTL).
- I would like to see Calypto do automatic black-boxing of memories
based on the memory consumption during analysis and appropriately
report back to the designer how the analysis was done (which memories
were black-boxed?).
- Capacity is an issue. It would be nice if Calypto would incorporate
incremental capabilities and hierarchical analysis into their tool.
Overall, SLEC addresses two important aspects of design:
a) Equivalence between system-level transaction vs. cycle-accurate
RTL models.
b) Equivalence between re-timed or re-powered RTL models.
With SLEC, my RTL quality is no longer dependent on the quality of the
test bench. It's useful to anyone interested in the above two problems.
- [ An Anon Engineer ]
Index
Next->Item
|
|
