Subject: RE: FTL fully supports that assume/guarantee paradigm
From: Armoni, Roy (roy.armoni@intel.com)
Date: Mon Jul 16 2001 - 12:38:12 PDT
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 - 12:39:12 PDT