Subject: RE: FTL fully supports that assume/guarantee paradigm
From: Sandeep K. Shukla (skshukla@ics.uci.edu)
Date: Mon Jul 16 2001 - 22:23:17 PDT
Dear Roy,
Your observations are almost right about my usage requirements.
let me ask this question.
If I say
assume f1
assume f2
assert g
and give model M, and run PROVER,
what does it prove? Doesn't it prove M |= (f1 & f2) -> g ?
Now usually for bug hunting, if I find a bug, I usually try to manually
verify that f1 and f2 are indeed true of the environment and the counter
example
is not due to over relaxation or wrong assumptions for the environment.
However, if we don't find any bugs, then I would try to prove f1 and f2
about the environment because otherwise I won't know if I made a mistake
in the assumptions.
However, when I do the FSM approach, what I am doing is
M \intersect A(f1) \intersect A(f2) where A(fi) denotes an FSM describing
all
behavioral traces that abide by the property fi.
So I am proving M \intersect A(f1) \intersect A(f2) |= g
and there what I have to prove in order to guarantee that E |= f1 & f2
is to show that M \intersect A(not f1)\intersect A(not f2) = empty language
automata
Now since I construct A(fi) by hand, most of the time I can make sure that
A(fi) is
strongly deterministic and hence constructing A(not fi) is not expensive and
requires
an inexpensive complementation.
So the FSM approach lets an experienced designer gain a lot in terms of
complexity,
because an automatic fi to A(fi) generator will blow up or make A(fi)
nondeterministic
and hence complementation will become expensive.
In a way f1 and f2 weakest precondition on the environment that allows me to
prove g of the
model M.
I sort of agree with you that just for bug hunting we do n ot need full
power of assume guarantee
because bug hunting is not a formal method, rather a heuristic anyway.
However, when the bug
hunting results in no bug, then to satisfy ourselves, that the lack of bug
is not due to too
strong assumptions made, we need the full power of Assume Guarantee.
Regards
Sandeep
-----Original Message-----
From: owner-vfv@eda.org [mailto:owner-vfv@eda.org]On Behalf Of Armoni,
Roy
Sent: Monday, July 16, 2001 8:08 PM
To: Sandeep K. Shukla; John Emmitt
Cc: vfv@eda.org
Subject: RE: FTL fully supports that assume/guarantee paradigm
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 - 22:22:29 PDT