( ESNUG 352 Item 7 ) --------------------------------------------- [5/17/00]
Subject: ( ESNUG 351 #8 ) Formality, Chrysalis, Verisity, & Model Checkers
> A few weeks ago, one of my readers forwarded me this anonymous post from
> the Yahoo CDN stock chat board:
>
> "Formality sales of about $10M doesn't point to a market leader, it
> seems like a tool bundled into a larger deal for a low price, which
> Synopsys can afford to do to build a market presence. As you probably
> know, formal verification is divided into two areas, model checking
> and comparison checking. Verplex is the runaway leader in comparison
> checking, and Chrysalis/Avanti still owns model checking. Another area
> is test bench verification where Synopsys has no presence and Verisity
> is the leader here. There is also a new company on the horizon that
> will challenge Verisity. So Formality's survival is in question, and
> this area is hot and growing."
>
> Why I'm reprinting this is that passing claim that "Chrysalis/Avanti still
> owns model checking" -- is this true? What are the customer experiences
> with their model checking tools? Why I ask this was while at HDLcon'00, I
> ran into a Cadence marketing guy who said Cadence was doing very well in
> the model checking business. I would love to see a detailed customer
> review of the Cadence model checking tools just to see if this Cadence
> marketdroid was on-the-money or blowing smoke.
>
> - John Cooley
> the ESNUG guy
From: Sherri Al-Ashari
So, when I worked at SUN, the terminology was model checking and equivalency
checking and theorem proving. The first 2 operated on RTL, and the third
you had to write what you were proving in some mathematical language. From
what I had seen ~2 years ago was that Chrysalis was ahead in equivalency
checking and FormalCheck (purchased by Cadence from Lucent) was the easiest
to use model checker.
I'm interested in hearing about this challenger to Verisity... is there
really room for a third? I wonder how believable this Yahoo source is....
- Sherri Al-Ashari
---- ---- ---- ---- ---- ---- ----
From: Mike Bartley
John,
You say there is also a new company on the horizon that will challenge
Verisity. Can you give more details please?
- Mike Bartley
Infineon
---- ---- ---- ---- ---- ---- ----
From: Garry Tuttle
Hello, John,
In one of your recent ESNUGs you mentioned a company who offer a product
competitive to Verisity. We are an EDA distributor and always on the look
out for new tools to sell in the UK and Republic of Ireland. We would be
interested to find out more about this company - can you send me more
information please?
- Garry Tuttle
Alt Technologies Basingstoke, Hampshire, UK
---- ---- ---- ---- ---- ---- ----
From: Erik Jessen
Hi, John,
I've not tried Cadence model-checking, but I believe it to be very useful.
On equivalency checking, Verplex has worked well for us. RTL v. gate on
600k gates:
flattened hierarchy : 3 hours
hieararchical compare: < 1 hour
on a Sun 266MHz CPU.
We do FPGAs and also have done equivalency checking there. We found the
following interesting results. Given:
reg [15:0] foo;
always @ (posedge clk)
if (fee == 1'b1)
foo <= 16'h0000;
else
foo <= 16'hFFFF;
Synopsys generates 16 flops for "foo". Synplicity recognizes that all 16
flops are set to the same value, and simply implements a single flop, then
wires its output 16 places. But none of the equivalency checking tools we
tried cope with Synplicity's results. Verplex allows you to tell it that
16 flops in RTL are equivalent to a single flop in gates. This led me to
do the following:
1.) I asked Synopsys to do similar flop elimination; they said they set
a policy long ago that they would output the 16 flops. (Can anyone
help me encourage them to at least have a switch to do this cleanup?)
2.) I talked to Synplicity and asked them to work with the equivalency
cheching vendors & write out a mapping file so that people can run
EC on their FPGA netlists, and also identify redundant flops in the
original design. I believe they are working on it.
In power-sensitive ASIC applications, I'd run Synplicity & EC on my netlist
to find redundant flops & remove them, before running Synopsys. Battery
time is worth it.
- Erik Jessen
Vixel Irvine, CA
---- ---- ---- ---- ---- ---- ----
From: Avi Parash
Hi John,
IBM has a Model Checker as well. (I am using it.) For more info see:
http://www.haifa.il.ibm.com/projects/verification/RB_Homepage/
Regards,
- Avi Parash
Zoran Microelectronic Ltd. Israel
|
|
