Subject: RE: the problem with/phenomenon of assume/guarantee
From: Vassilios.Gerousis@infineon.com
Date: Thu Jul 12 2001 - 08:36:58 PDT
Hello Sandeep,
I am Vassilios Gerousis, Technical chair of all committees within Accellera. We need to focus this committee on donated materials that have gone through legal negotiation first. This group and Accellera cannot assume liability for materials that did not go through the normal process of technology assignment first prior to discussions. We must focus on the four donated languages only. We have cleared these donations through the legal and patent discussions.
I am also currently investigating the new documents that have so far been circulating like EDL from IBM and Omega from Verisity. These should have been cleared first before sending them around. We cannot accept document that have confidential on them either.
Best Regards
Vassilios
-----Original Message-----
From: Sandeep K. Shukla [mailto:skshukla@ics.uci.edu]
Sent: Thursday, July 12, 2001 9:32 AM
To: eisner@il.ibm.com; vfv@eda.org
Cc: roy.armoni@intel.com
Subject: RE: the problem with/phenomenon of assume/guarantee
This gives me a chance to show off how Cadence SMV is great!
I just coded the example in cadence SMV and guess what, all the things
you said cannot be proven are proved with SMV easily.
In the first case, I vary t, and hence I had to change your assertions
to include p_t (past value of t), in the second case, I use layer constructs
to fix t, and you can run the proof twice by commenting out one of the
layers (FixT0, FixT1) and using the appropriate assertions.
Sandeep
module myE(i,a,b){
input i : boolean;
output a : boolean;
output b: boolean;
init(b) := 0;
next(b) := i;
a := i;
}
module myM(a,b, c, d) {
input a: boolean;
input b : boolean;
output c: boolean;
output d: boolean;
init(c) := 0;
next(c) := a;
d := b;
}
module main(){
i, a,b,c,d: boolean;
E1: myE(i,a,b);
M1: myM(a,b,c,d);
t: boolean;
p_t: boolean;
init(p_t) := 0;
next(p_t) := t;
prop1: assert(G(c=d));
prop2: assert(G((a=t) -> X(b=p_t)));
prop3: assert(G(G((a=t) -> X(b=p_t)) -> G(c=d)));
prop4: assert(G((a=t) -> X(b=p_t)) -> G(c=d));
}
However, if you are not interested in t to vary, then try the following
module myE(i,a,b){
input i : boolean;
output a : boolean;
output b: boolean;
init(b) := 0;
next(b) := i;
a := i;
}
module myM(a,b, c, d) {
input a: boolean;
input b : boolean;
output c: boolean;
output d: boolean;
init(c) := 0;
next(c) := a;
d := b;
}
module main(){
i, a,b,c,d: boolean;
E1: myE(i,a,b);
M1: myM(a,b,c,d);
t: boolean;
layer fixT0: {
t := 0;
}
--layer fixT1:{
-- t:= 1;
-- }
prop1: assert(G(c=d));
prop2: assert(G((a=t) -> X(b=t)));
prop3: assert(G(G((a=t) -> X(b=t)) -> G(c=d)));
prop4: assert(G((a=t) -> X(b= t)) -> G(c=d));
using t//fixT0
prove prop2, prop3, prop4;
-- using t//fixT1
-- prove prop2, prop3, prop4;
}
> -----Original Message-----
> From: owner-vfv@eda.org [mailto:owner-vfv@eda.org]On Behalf Of
> eisner@il.ibm.com
> Sent: Wednesday, July 11, 2001 11:49 PM
> To: vfv@eda.org
> Cc: roy.armoni@intel.com
> Subject: the problem with/phenomenon of assume/guarantee
>
>
>
>
> all,
>
> roy and i have been discussing off-line what i see as a problem with the
> assume/guarantee paradigm, and what roy terms a phenomenon, or an
> artifact.
> i asked roy to explain this to the committee, but since he is
> traveling and
> has not had time, we agreed that i be the one to explain it to
> you. a word
> file containing a very simple example is attached below.
>
> the attachment shows that the problem is not related to one specific
> language. in fact, as roy has pointed out, it exists also in
> ltl, with the
> following assumption: G ((t <-> X t) & (a=t -> X b=t)). thus,
> the problem
> is with the paradigm itself. note that the example does not show that the
> paradigm breaks down: the paradigm says that *if* you can prove that E
> models f and that M models f->g, then you can conclude that E||M models g.
> since in the example we cannot prove that M models f->g, the paradigm does
> not require us to be able to conclude anything at all. from a purely
> formal point of view, then, the paradigm is upheld by the example.
> however, this example calls into question the practical applicability of
> the assume/guarantee paradigm for many formulas.
>
> in light of all this, we find the mantra that "every FTL property can be
> used as an assumption (and as an assertion)" to be formally correct, but
> misleading. using the formula shown in the example as an assumption is
> possible, but will result in a false negative - i.e., in a counter-example
> to a specification which is valid under the assumption. users will not
> tolerate false negatives (and should not be told to).
>
> thus, while full support of the assume/guarantee paradigm is certainly
> "nice to have", we know of no language for which the paradigm is useful
> for all formulas. users should not be made to understand why formally the
> paradigm is fully supported, rather, they should be guided by the language
> as to how to make use of its capabilities.
>
> regards,
>
> cindy.
>
> (See attached file: assumeguaranteeproblem.doc)
>
> 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 : Thu Jul 12 2001 - 08:37:50 PDT