Subject: RE: FTL fully supports that assume/guarantee paradigm
From: Armoni, Roy (roy.armoni@intel.com)
Date: Mon Jul 16 2001 - 20:08:26 PDT
Dear Sandeep and John,
The methodology that Sandeep is describing is indeed of bug-hunting.
However,
it utilizes only the "assume" part of the assume-guarantee paradigm. My
understanding is that Sandeep could allow himself to describe the
environment
using an FSM syntax because he was not interested in guaranteeing these
behaviors later on. Is that correct Sandeep?
When building a proof, one usually starts with some property g and wishes to
prove M |= g. It usually fails because environment assumptions are needed.
Next steps are to add assumptions f1, f2, ... and prove that M |= (f1 & f2)
-> g.
When this succeeds, one is left with "proof obligations" on f1 and f2.
These
obligations should be released by proving E |= f1 and E |= f2.
Note that when following this sequence, the so called artifact that Cindy
and I
described do not happen, because we do not start with an assertion and later
on use it as assumption. Rather, we first choose environment properties and
assume them, and later on release these "proof obligations". (Thanks to
Avner Landver for describing things that way). Hillel, does this paragraph
also answer your questions?
Last point is to answer John. I had a bad choice of words saying that the
paradigm is not very useful for bug-hunting. However, I think that for
building
proofs, you cannot do without it, while for bug hunting it might be that
simpler
requirements from the spec language are needed, for instance, writing FSMs
to describe the behavior. It might be an over-kill to require full support
of
assume-guarantee if your methodology does not require building proofs at
all.
Regards, Roy
-----Original Message-----
From: Sandeep K. Shukla [mailto:skshukla@ics.uci.edu]
Sent: Tuesday, July 17, 2001 4:44 AM
To: John Emmitt; Armoni, Roy; eisner@il.ibm.com
Cc: vfv@eda.org
Subject: RE: FTL fully supports that assume/guarantee paradigm
All the FV work I have done in the last two years were for bug hunting
rather than constructing proofs. In the bug hunting we used assume guarantee
equally intensively as proof construction. Usually we would take a
piece of RTL, that would have 1000s of latches and hence cannot be
pushed through the FV tools. So we did pruning. While pruning, we had
to make assumptions at the pruned interface all the time. The usual
way of doing that was to study the RTL carefully, and understand
that certain signals at the pruned interface has certain behaviors
and then we formulated properties describing such behaviors.
Then we used them as "assume" clauses.
Many times, in place of writing properties for the signals at the
pruned interface, we would, write a state machine describing the
assumed behavior. In fact, that was more easy to do because many times
writing a succinct property for an assumed behavior might be difficult.
So, in my opinion
without an assume guarantee style support (either in the form
of "assume" clauses, or a facility to describe a state machine kind
of reference model), bug hunting is not possible in a realistic design
using the current capacity limited FV tools.
Sandeep
>>-----Original Message-----
>>From: owner-vfv@eda.org [mailto:owner-vfv@eda.org]On Behalf Of John
>>Emmitt
>>Sent: Monday, July 16, 2001 2:46 PM
>>To: Armoni, Roy; eisner@il.ibm.com
>>Cc: vfv@eda.org
>>Subject: Re: FTL fully supports that assume/guarantee paradigm
>>
>>
>>Roy,
>>
>>re:
>>> I think that the real question is what you are after when doing
>>FV: is it
>>> "bug hunting"
>>> or "building proofs". I guess that for bug hunting, the
>>assume/guarantee
>>> paradigm is
>>> not very useful. However, for building proofs, it is probably
>>impossible
>>to
>>> do without
>>> decomposition.
>>
>>I would think that assume/guarantee can be very useful for bug hunting, as
>>well, since a very "deep" bug may need decomposition as much as a complete
>>proof might. Also, I think that most users should/will be focused on bug
>>hunting, rather than "proof". What is your experience on this- do
>>you focus
>>mainly on building proofs?
>>
>>Regards,
>>
>>John Emmitt
>>Verplex Systems
>>----- Original Message -----
>>From: Armoni, Roy <roy.armoni@intel.com>
>>To: <eisner@il.ibm.com>
>>Cc: <vfv@eda.org>
>>Sent: Monday, July 16, 2001 3:38 PM
>>Subject: RE: FTL fully supports that assume/guarantee paradigm
>>
>>
>>> Hi Cindy,
>>>
>>> Could you support your statement that "in practice, you require that the
>>> user rewrite
>>> many formulas in order to use them as assumptions." with some proof? I
>>> guess that
>>> you cannot because Intel has a counter-example. I refer you to
>>slide 8 in
>>> my presentation
>>> of the ForSpec language. The graph that is shown there is a real one,
>>> showing
>>> assume-guarantee relations among 50 properties. This is a real graph,
>>taken
>>> from
>>> one spec of the Pentium 4. I cannot give exact numbers, but more than a
>>few
>>> hundreds
>>> such graphs exist in the FV of the Pentium 4.
>>>
>>> I think that the real question is what you are after when doing
>>FV: is it
>>> "bug hunting"
>>> or "building proofs". I guess that for bug hunting, the
>>assume/guarantee
>>> paradigm is
>>> not very useful. However, for building proofs, it is probably
>>impossible
>>to
>>> do without
>>> decomposition.
>>>
>>> Roy
>>>
>>>
>>> -----Original Message-----
>>> From: eisner@il.ibm.com [mailto:eisner@il.ibm.com]
>>> Sent: Thursday, July 12, 2001 5:42 PM
>>> To: Armoni, Roy; vardi@cs.rice.edu
>>> Cc: vfv@eda.org
>>> Subject: Re: FTL fully supports that assume/guarantee paradigm
>>>
>>>
>>>
>>>
>>> roy and moshe,
>>>
>>> your document proves my point that the FTL mantra is misleading. in
>>> practice, you require that the user rewrite many formulas in
>>order to use
>>> them as assumptions. this defeats the whole purpose of the paradigm.
>>>
>>> regards,
>>>
>>> cindy.
>>>
>>> Cindy Eisner
>>> Formal Methods Group Tel:
>>+972-4-8296-266
>>> IBM Haifa Research Laboratory Fax: +972-4-855-0070
>>> Haifa 31905, Israel e-mail:
>>> eisner@il.ibm.com
>>>
>>>
>>
This archive was generated by hypermail 2b28 : Mon Jul 16 2001 - 20:36:35 PDT