Formal verification and Static Timing 
Author Message
 Formal verification and Static Timing

I would like to address these questions to those who actually use a static timing
analysis tool or a formal verification tool. The questions are the value and need of
using such tools.

Static timing analyzer: Why not just use the STA built into your synthesizer? As far
as I can tell for design's under say 200 - 300k gate the built in STA does the job in
reasonable amount of time. Now for very large designs maybe the performance
advantage of an STA like SST Velocity, or PrimeTime then makes sense. Have I
got it right or is there something I'm missing? Does an STA check for things that you
can check for in the synthesis tool?

Formality: I think know the reasons why one would like to use something like
Formality on a large design. To check that the synthesizer didn't make a logic error.
The question is has anyone that uses Formality (or other formal verification tool)
ever found a problem? What type of problem did you find? And does this tool
eliminate the need (beyond checking for proper startup etc.) for post route
simulation?

Submitted for the community's comments



Mon, 28 Jan 2002 03:00:00 GMT  
 Formal verification and Static Timing


Quote:
>Static timing analyzer: Why not just use the STA built into your synthesizer? As far
>as I can tell for design's under say 200 - 300k gate the built in STA does the job in
>reasonable amount of time. Now for very large designs maybe the performance
>advantage of an STA like SST Velocity, or PrimeTime then makes sense. Have I
>got it right or is there something I'm missing? Does an STA check for things that you
>can check for in the synthesis tool?

Let's take a good example: Synopsys Design Compiler vs. PrimeTime.  Now, you'd
think that there'd be no use for PrimeTime since Synopsys makes both products,
and DC should do everything that PT does, right?

Wrong.

DC's timing algorithms are not as detailed as PT's, and it does fewer timing
checks (e.g. FF falling edge recovery check: DC seems oblivious to such
requirements, but PT checks it).
PT seems to support more realistic wire load models.  Does the design
I am working on right now meet timing?  Depends - in DC it doesn't, and in PT
it (almost) does.

I am now waiting to get detailed timing results back from layout.  I'm
pretty sure that PT will do a better job at that point.



Mon, 28 Jan 2002 03:00:00 GMT  
 Formal verification and Static Timing
Joshua Schwartz a crit :

Quote:

> Formality: I think know the reasons why one would like to use something like
> Formality on a large design. To check that the synthesizer didn't make a logic error.
> The question is has anyone that uses Formality (or other formal verification tool)
> ever found a problem? What type of problem did you find? And does this tool
> eliminate the need (beyond checking for proper startup etc.) for post route
> simulation?

> Submitted for the community's comments

Hi,

1) Formality is an equivalence checker, that is, compares two
designs (gate or RTL level) on a structural point of view. It tries
to match the memory elements and verifies that the combinational
logic blocks are functionally equivalent. How does it work? First,
it performs a kind of symbolic logic synthesis of the RTL models if
one or both of your models are RTL level models. Then it builds BDDs
of the combinational blocks and compares the BDDs. What can it be
used for and is it really needed?
- Find logic synthesis problems when checking a gate level model
against its RTL level description. As the symbolic synthesis
algorithm is different from the "real" synthesis one it might be
that it finds a bug (the bug could be a description error that was
not seen by the synthesizer or a synthesizer bug). In my opinion
this is not the main interest for this technology. But it's much
cheaper and faster than hardware simulation accelerators. And more
than that, it's exhaustive and does not depend on a test partern.
There is no need to design complex simulation environments. So if
you already use hardware simulation accelerators in order to check
your netlists, equivalence checking could save you time and money.
Warning: hardware simulation accelerators are used to speed up RTL
simulations too. Equivalence checking can't help on this.
- Check that two RTL descriptions are equivalent. As long as you
don't move your memory elements you can use an equivalent checker as
a fast functionality verification tool. Once you validated a golden
RTL model you can modify and test it faster than by simulating and,
again, exhaustively. This is much more useful.
- Check that two gate level models are equivalent. You can insert
test stuff or clock trees and check the modified netlist against a
golden netlist. Again it's faster than simulation and it's
exhaustive. Very useful too.

2) Equivalence checking is not the only formal verification method.
Model checking is more complicated and works on smaller blocks but
is much more interesting (my opinion, of course). It can be used to
compare two RTL models on a functional point of view, even when the
memory elements are different. Example: two descriptions of the same
state machine, one using an adjacent encoding and the other a one
hot encoding. It can also check your RTL (or gate level) model
against a set of temp{*filter*}logic properties. Example: "Never the
traffic lights are simultaneously green in both roads" or "Always if
a client requests the bus he actually gets it". Model checking helps
the designer at a higher abstraction level and finds a lot of bugs.
As the property checking is exhaustive it covers the corner cases.
It does not suppress the need for simulation but it speeds up the
design cycle and avoids more bugs.

Hope it helps. Regards,
--
Renaud Pacalet, ENST / COMELEC, 46 rue Barrault 75634 Paris Cedex 13



Mon, 28 Jan 2002 03:00:00 GMT  
 Formal verification and Static Timing

Quote:



> >Static timing analyzer: Why not just use the STA built into your synthesizer? As far
> >as I can tell for design's under say 200 - 300k gate the built in STA does the job in
> >reasonable amount of time. Now for very large designs maybe the performance
> >advantage of an STA like SST Velocity, or PrimeTime then makes sense. Have I
> >got it right or is there something I'm missing? Does an STA check for things that you
> >can check for in the synthesis tool?

> Let's take a good example: Synopsys Design Compiler vs. PrimeTime.  Now, you'd
> think that there'd be no use for PrimeTime since Synopsys makes both products,
> and DC should do everything that PT does, right?

> Wrong.

> DC's timing algorithms are not as detailed as PT's, and it does fewer timing
> checks (e.g. FF falling edge recovery check: DC seems oblivious to such
> requirements, but PT checks it).

Is it also oblivious when timing is done on an SDF backannotated version of the
netlist ?

- Show quoted text -

Quote:

> PT seems to support more realistic wire load models.  Does the design
> I am working on right now meet timing?  Depends - in DC it doesn't, and in PT
> it (almost) does.

> I am now waiting to get detailed timing results back from layout.  I'm
> pretty sure that PT will do a better job at that point.



Mon, 28 Jan 2002 03:00:00 GMT  
 Formal verification and Static Timing

Quote:

> I would like to address these questions to those who actually use a static timing
> analysis tool or a formal verification tool. The questions are the value and need of
> using such tools.

> Static timing analyzer: Why not just use the STA built into your synthesizer? As far
> as I can tell for design's under say 200 - 300k gate the built in STA does the job in
> reasonable amount of time. Now for very large designs maybe the performance
> advantage of an STA like SST Velocity, or PrimeTime then makes sense. Have I
> got it right or is there something I'm missing? Does an STA check for things that you
> can check for in the synthesis tool?

Basically, you're right.
PrimeTime does it only faster and more user-friendly. But I guess you could do without.

Quote:

> Formality: I think know the reasons why one would like to use something like
> Formality on a large design. To check that the synthesizer didn't make a logic error.

This would be a possible application. But maybe not the most driving one ...

Quote:

> The question is has anyone that uses Formality (or other formal verification tool)
> ever found a problem? What type of problem did you find? And does this tool
> eliminate the need (beyond checking for proper startup etc.) for post route
> simulation?

Works best for netlist-netlist comparison , i.e. after clock tree insertion.
Works also for some (a lot ?) of cases of RTL - netlist comparison. But this would be
again the synthesis check.

Quote:

> Submitted for the community's comments

  Jos De Laender , personal opinion , not speaking for my company.


Mon, 28 Jan 2002 03:00:00 GMT  
 Formal verification and Static Timing

Quote:

> The question is has anyone that uses Formality (or other formal verification tool)
> ever found a problem? What type of problem did you find? And does this tool
> eliminate the need (beyond checking for proper startup etc.) for post route
> simulation?

I'd find it difficult to forgive DC (say) if it introduced
logical errors which were later picked up by an equivalence
checker.  That's not to say it couldn't happen, just that
it would{*filter*}me off.  Instead I think that equivalence
checking should be the responsibility of the synthesis
tool (that's if it can't be sure to get it right first
time).

But a checker could be used for ECOs, to ensure that any
handcrafting (shock horror) of the netlist doesn't damage
the logic.

But it is model checking which may be the cooler aspect of
formal verification.  If such a tool can reason about the
design and so provide proof of certain characteristics of my
design - e.g. that buffer will never overflow, or those two
flags which should be mutually exclusive aren't - then that
could avoid having to simulate.  That could save a lot of
verification time, and would be worth having.

However, I don't think model checkers are up to anything much bigger
than a JK flip-flop yet :-)

Those more in the know, come on down.

t



Mon, 28 Jan 2002 03:00:00 GMT  
 Formal verification and Static Timing

Quote:


>> The question is has anyone that uses Formality (or other formal verification tool)
>> ever found a problem? What type of problem did you find? And does this tool
>> eliminate the need (beyond checking for proper startup etc.) for post route
>> simulation?

>I'd find it difficult to forgive DC (say) if it introduced
>logical errors which were later picked up by an equivalence
>checker.  That's not to say it couldn't happen, just that
>it would{*filter*}me off.  Instead I think that equivalence
>checking should be the responsibility of the synthesis
>tool (that's if it can't be sure to get it right first
>time).

>But a checker could be used for ECOs, to ensure that any
>handcrafting (shock horror) of the netlist doesn't damage
>the logic.

As far as equivalence checker is concerned, I haven't seen a single
design so far that was sent to fab w/o some hand-editing. Equivalnce
checker are the best way to verify that one did not mess up the logic
during hand-editing.

Aso some times, the last minute bugs are fixed in metal, or by hand
crfting gates. In those cases one can save some time by avoiding
re-synthesis by comparing modified-RTL with new-gates.

Quote:
>But it is model checking which may be the cooler aspect of
>formal verification.  If such a tool can reason about the
>design and so provide proof of certain characteristics of my
>design - e.g. that buffer will never overflow, or those two
>flags which should be mutually exclusive aren't - then that
>could avoid having to simulate.  That could save a lot of
>verification time, and would be worth having.

>However, I don't think model checkers are up to anything much bigger
>than a JK flip-flop yet :-)

>Those more in the know, come on down.

I have done some model-checking with designs bigger than one JK FF :-)
Though model-checkers are not yet good enough to handle lots of gates,
they can be of use in modules that are small-but-crucial. I surprised
many designers by finding bugs in just about all the arbiters (that
handle more than two reqs) I have verified so far that the designers
thought oh-so-easy-to-design.

The main advantage of formal methods is the confidence it gives after
the proof. I was never too confident about a simulation that's running
error-free for weeks, but trusted most of my less-than-one-day proofs
of some crucial state-machines. But may be it's just me :-)

--

Cheers,

--O--O--O--O--O--O--O--O--O--O--O--O--O--O--O--O--O--O--O--O--O--O



Mon, 28 Jan 2002 03:00:00 GMT  
 Formal verification and Static Timing
Quote:
> Joshua Schwartz writes:
> Static timing analyzer: Why not just use the STA built into your synthesizer? As far

The question should be:  Why can't synthesis tools guarantee quality results all the
time?  One thing to remember, a synthesis tool is software.  Name one software product
that doesn't have some quirks in it.  Also, there are human inputs involved.  Synthesis
tools are meant to be an aid, not a guarantee...  ;)

STA tools external from synthesis tools are very useful, especially for large designs.
DesignTime, the timing analyzer used by the Synopsys synthesis engine, has capacity
and performance limitations.  PrimeTime and similar STA tools, offer better algorithms,
along with higher capacity and performance capabilities required for large designs.
Looking at PrimeTime, there are faster tools out there, but this really shouldn't be
the issue.  The real bottleneck for STA is parasitic extraction.

Quote:
> Formality: I think know the reasons why one would like to use something like

See the ESNUG320 Item3 responses.  A lot of good answers to your question.  There is
some way to access the archives of ESNUG, but I forget how...

Quote:
> Shyam Pullela writes:
> I was never too confident about a simulation that's running error-free for weeks,
> but trusted most of my less-than-one-day proofs of some crucial state-machines.
> But may be it's just me...

Formal methods over simulation is definitely a totally different verification hat
to accept for a majority of designers... ;)

Quote:
> Tommy Kelly writes:
> However, I don't think model checkers are up to anything much bigger
> than a JK flip-flop yet

You got that right.  I want a vendor solution for a cache controller!  Model Checking
vendors still have a lot of limitations that need to be fixed before the average
Joe-designer can use it like any other EDA commodity tool.  But when they do work, very
impressive.  As a designer, knowing the promises for a Model Checker, you have to say
"Way cool!".  It is a lot more interesting than an Equivalence Checker.  But from a
practical sense, the vendors are not yet there.

There are some vendors that try to bridge the gap to Model Checking.  Dynamic tools
such as Vera and Verisity.  Static tools such as Chrysalis.  From the static standpoint,
the current focus is on smaller problems.

Formal tools beyond simple Equivalence Checking are expensive, pretty, and don't scale
well.  That is why a lot of custom solutions are necessary within some design groups.  
They may be ugly, but they are cheap and try to directly solve the problems that exist.

Mike



Tue, 29 Jan 2002 03:00:00 GMT  
 Formal verification and Static Timing
Is it true that Formality uses DC as frontend ??
M

Quote:
>> Joshua Schwartz writes:
>> Static timing analyzer: Why not just use the STA built into your
synthesizer? As far
>The question should be:  Why can't synthesis tools guarantee quality
results all the
>time?  One thing to remember, a synthesis tool is software.  Name one
software product
>that doesn't have some quirks in it.  Also, there are human inputs

involved.  Synthesis
Quote:
>tools are meant to be an aid, not a guarantee...  ;)

>STA tools external from synthesis tools are very useful, especially for
large designs.
>DesignTime, the timing analyzer used by the Synopsys synthesis engine, has
capacity
>and performance limitations.  PrimeTime and similar STA tools, offer better
algorithms,
>along with higher capacity and performance capabilities required for large
designs.
>Looking at PrimeTime, there are faster tools out there, but this really
shouldn't be
>the issue.  The real bottleneck for STA is parasitic extraction.

>> Formality: I think know the reasons why one would like to use something
like
>See the ESNUG320 Item3 responses.  A lot of good answers to your question.
There is
>some way to access the archives of ESNUG, but I forget how...

>> Shyam Pullela writes:
>> I was never too confident about a simulation that's running error-free
for weeks,
>> but trusted most of my less-than-one-day proofs of some crucial
state-machines.
>> But may be it's just me...
>Formal methods over simulation is definitely a totally different
verification hat
>to accept for a majority of designers... ;)

>> Tommy Kelly writes:
>> However, I don't think model checkers are up to anything much bigger
>> than a JK flip-flop yet
>You got that right.  I want a vendor solution for a cache controller!
Model Checking
>vendors still have a lot of limitations that need to be fixed before the
average
>Joe-designer can use it like any other EDA commodity tool.  But when they
do work, very
>impressive.  As a designer, knowing the promises for a Model Checker, you
have to say
>"Way cool!".  It is a lot more interesting than an Equivalence Checker.
But from a
>practical sense, the vendors are not yet there.

>There are some vendors that try to bridge the gap to Model Checking.
Dynamic tools
>such as Vera and Verisity.  Static tools such as Chrysalis.  From the
static standpoint,
>the current focus is on smaller problems.

>Formal tools beyond simple Equivalence Checking are expensive, pretty, and
don't scale
>well.  That is why a lot of custom solutions are necessary within some
design groups.
>They may be ugly, but they are cheap and try to directly solve the problems
that exist.

>Mike



Thu, 31 Jan 2002 03:00:00 GMT  
 Formal verification and Static Timing

Quote:

> Formal methods over simulation is definitely a totally different verification hat
> to accept for a majority of designers... ;)

HDL coding over schematic capture is ... (10 years ago).

Quote:
> You got that right.  I want a vendor solution for a cache controller!  Model Checking
> vendors still have a lot of limitations that need to be fixed before the average
> Joe-designer can use it like any other EDA commodity tool.

Yes, there are some possible improvements in Model Checking
(abstraction could be one of them). But it's already very useful.
The problem does not come from the vendors. It comes from the
designers, as usual. Temp{*filter*}logic is not so easy to understand.

Quote:
> But when they do work, very
> impressive.  As a designer, knowing the promises for a Model Checker, you have to say
> "Way cool!".  It is a lot more interesting than an Equivalence Checker.  But from a
> practical sense, the vendors are not yet there.

What do you mean? They don't offer the magic black box with the
red and green leds?

Quote:

> There are some vendors that try to bridge the gap to Model Checking.

What gap? Between what and what?

Quote:
> Dynamic tools
> such as Vera and Verisity.

As far as I know Vera and Verisity are testbench generators.
Nothing to do with formal verification. A lot to do with coverage.
I may be wrong.

Quote:
> Static tools such as Chrysalis.

They propose an equivalence checker and a model checker, as
everybody else. How do they bridge the gap?

Quote:
> From the static standpoint,
> the current focus is on smaller problems.

True for model checking, false for equivalence checking.

Quote:

> Formal tools beyond simple Equivalence Checking are expensive,

VIS is free. ( http://www.*-*-*.com/ ~vis/).

Quote:
> pretty, and don't scale
> well.  That is why a lot of custom solutions are necessary within some design groups.
> They may be ugly, but they are cheap and try to directly solve the problems that exist.

> Mike

I really think that formal verification (especially model checking)
is very useful. Today. Dynamic verification of this assumption:
- take two projects, one using simulation only, the other using
  formal verification too
- try to get an accurate measure of the time your designers spend
  in verification (not only the run time but including the reference
  model design, the simulation environment design, customization
  and understanding of the tools, etc.)
- count the bugs

Regards,
--
Renaud Pacalet, ENST / COMELEC, 46 rue Barrault 75634 Paris Cedex 13



Fri, 01 Feb 2002 03:00:00 GMT  
 Formal verification and Static Timing

Quote:
>> Formality: I think know the reasons why one would like to use something like
> See the ESNUG320 Item3 responses.  A lot of good answers to your question.  There is
> some way to access the archives of ESNUG, but I forget how...

See http://www.deepchip.com

--

Phone: +49 711 821-4 94 93                 :    Fax: +49 711 821-4 55 71
Alcatel Telecom, Microelectronic Center, Lorenzstr.10, D-70435 Stuttgart



Sat, 02 Feb 2002 03:00:00 GMT  
 
 [ 11 post ] 

 Relevant Pages 

1. Formal verification and Static Timing

2. BACUP meeting: Formal Verification, Physical Verification; SourceLink

3. BACUP meeting: Formal Verification, Physical Verification; SourceLink

4. Formal verification methods for OOPS

5. Formal methods for verification of OOPS

6. Functional programming languages & formal verification

7. IBM/Israel: Open Positions in Functional Formal Verification

8. Scientific puzzle of formal circuit verification at next week's DAC

9. Formal verification of one-hot state machine.

10. Formal Verification

11. Formal verification

12. Advertisement: EDA Jobs (Formal Verification)

 

 
Powered by phpBB® Forum Software