Subject: FW: Safety vs Liveness
From: Harry Foster (foster@rsn.hp.com)
Date: Tue Jun 26 2001 - 07:22:37 PDT
-----Original Message-----
From: Sandeep K. Shukla [mailto:skshukla@ics.uci.edu]
Sent: Monday, June 25, 2001 7:07 PM
To: Harry Foster
Subject: Safety vs Liveness
Some how I am unable to send mail to the whole list, my
smtp server is rejecting it since morning. Could you please
send this for me?
Regards
Sandeep
As a practicing Formal Verifier at Intel for more than 2 years,
my experience is that it is the safety properties that I needed to
formulate 99% of the time (may be more). However, given that Ed and Moshe
are
on the subject, let me ask some of my doubts here.
To me a safety property is not only "something bad never happens",
it is actually all state invariant properties. In that light, some times
"liveness" type properties can be viewed as safety properties.
For example, "p eventually happens" in LTL is Fp, but usually that is not
enough
in most cases. In most cases we want to say GFp, which says that from all
states p eventually
happens. Note that this is a stronger requirement that Fp. However, I would
argue that from a hardware designer's perspective, it is more
important to have GFp, rather than Fp, because Fp, entails a possibility
that p happens in all paths once and then never happens.
Also, if we want another kind of liveness, say, way out of a bad state, we
can say
p->F(not p),
but what we want is G(p->F(not p), and hence such properties are also
state invariants.
Another thing, if we want to show GFp, the following safety formulation also
works,
try to prove G(not(p) -> X(not(p))
which basically tries to prove that whenever not p is true, it remains so
always.
If GFp is true in your system, then there will be a counter example to this
(provided Gp is
not fulfilling GFp).
If there is no counter example, then GFp is not true in your system.
So my question is, aren't most required liveness conditions some how
checkable using
state invariant properties for all practical purposes?
Sandeep
skshukla@ics.uci.edu
> -----Original Message-----
> From: Ed Clarke [mailto:emc@cs.cmu.edu]
> Sent: Monday, June 25, 2001 12:44 PM
> To: Sandeep K. Shukla; Moshe Vardi; Edmund.Clarke@cs.cmu.edu;
> Sudhir_Kadkade@sifr.com; Vassilios.Gerousis@infineon.com;
> arif@synopsys.com; avner.landver@intel.com; axels@cadence.com;
> bdeadman@sdvinc.com; cbrowy@avery-design.com; coelho@verplex.com;
> davidg@synopsys.com; dudani@synopsys.com; eisner@il.ibm.com;
> emc@cs.cmu.edu; erichm@cadence.com; fitz@co-design.com;
> flake@co-design.com; foster@rsn.hp.com; geist@il.ibm.com;
> gkhoory@synopsys.com; hillelm@msil.sps.mot.com; jbhasker@cadence.com;
> kchen@verplex.com; limor.fix@intel.com; mac@verisity.com;
> matthew@verisity.com; michael.siegel@mchp.siemens.de;
> pixley@adttx.sps.mot.com; prakash@realintent.com; roy.armoni@intel.com;
> shoham@il.ibm.com; smeier@synopsys.com; swamiv@synopsys.com;
> tla@0-in.com; wolfstal@il.ibm.com; yaron@verisity.com; ychsu@novas.com;
> zhong@innologic-systems.com
> Subject: RE: Accellera: Branching vs. Linear Time
>
>
> I think the point you make in the second part of your message is an
> important one.
> In addition to deciding on what language to use, we really need to decide
> on how
> compositional reasoning and refinement should be done as well. --Ed
>
>
>
> At 11:29 AM 6/25/2001 -0700, Sandeep K. Shukla wrote:
> >An excellent example of an LTL model checker built on top of CTL model
> >checker is
> >Cadence SMV (freely downloadable from Ken Mcmillan's webpage at
> >http://www-cad.eecs.berkeley.edu/~kenmcmil/). In this version of
> SMV, mostly
> -----Original Message-----
> From: Harry Foster [mailto:foster@rsn.hp.com]
> Sent: Thursday, June 07, 2001 12:56 PM
> To: foster@rsn.hp.com; arif@synopsys.com; pixley@adttx.sps.mot.com;
> eisner@il.ibm.com; coelho@verplex.com; davidg@synopsys.com;
> Edmund.Clarke@cs.cmu.edu; erichm@cadence.com; gkhoory@synopsys.com;
> hillelm@msil.sps.mot.com; jbhasker@cadence.com;
> zhong@innologic-systems.com; kchen@verplex.com; matthew@verisity.com;
> mac@verisity.com; flake@co-design.com; prakash@realintent.com;
> shoham@il.ibm.com; Sudhir_Kadkade@sifr.com; dudani@synopsys.com;
> swamiv@synopsys.com; tla@0-in.com; wolfstal@il.ibm.com;
> Vassilios.Gerousis@infineon.com; yaron@verisity.com;
> cbrowy@avery-design.com; michael.siegel@mchp.siemens.de;
> ychsu@novas.com; limor.fix@intel.com; bdeadman@sdvinc.com;
> roy.armoni@intel.com; avner.landver@intel.com; vardi@cs.rice.edu;
> smeier@synopsys.com; fitz@co-design.com; axels@cadence.com;
> geist@il.ibm.com; skshukla@ics.uci.edu
> Subject: Accellera FV July Paris Meeting at Intel
>
>
> Please send my e-mail to confirm your attendance at our
> July face-to-face meeting. We need to give a final attendance
> list to Intel's security to gain access to the building.
>
> Best regards,
>
> -Harry
>
This archive was generated by hypermail 2b28 : Tue Jun 26 2001 - 07:24:14 PDT