Subject: RE: [sv-ac] SVA/PSL equivalences
From: Armoni, Roy (roy.armoni@intel.com)
Date: Wed Oct 29 2003 - 22:04:31 PST
Hi John,
You are right. The ones that are not equivalent are:
initial assert @(c) not (x || y)
and
(!(x! | y!)) @c
The SVA version is a liveness property while the PSL is a safety.
Regards,
Roy
-----Original Message-----
From: owner-sv-ac@eda.org [mailto:owner-sv-ac@eda.org] On Behalf Of John
Havlicek
Sent: Wednesday, October 29, 2003 5:53 PM
To: Armoni, Roy
Cc: john.havlicek@motorola.com; eisner@il.ibm.com;
dana@wisdom.weizmann.ac.il; sv-ac@eda.org
Subject: [sv-ac] SVA/PSL equivalences
Hi Roy:
Let's look at the property/formula comparison first.
We can look at the assertion/formula comparison later.
Currently, SVA neutral semantics is defined only for
non-empty words, but since you have a clock I don't think
this affects the main point. So I will ignore the
restriction of w non-empty in SVA. I assume x,y are
boolean.
* <S> denotes the unclocked property resulting from
applying the SVA clock rewrite rules to the SVA clocked
property S.
* "|=" denotes SVA property satisfaction.
* "|==" denotes SVA tight satisfaction.
* "|=(c)" denotes PSL formula satisfaction relative to clock c.
* "|==(c)" denotes PSL tight satisfaction relative to clock c.
* "||=" denotes boolean satisfaction in both SVA and PSL.
In SVA,
w |= @(c) not(x or y)
iff w |= <@(c) not(x or y)>
iff [(x or y) is not a boolean expression]
w |= not <@(c) (x or y)>
iff w |= not (<@(c) x> or <@(c) y>)
iff w |= not ((!c[*0:$] ##1 c&x) or (!c[*0:$] ##1 c&y))
iff not({\bar w} |= ((!c[*0:$] ##1 c&x) or (!c[*0:$] ##1 c&y)))
iff not({\bar w} |= (!c[*0:$] ##1 c&x) or {\bar w} |= (!c[*0:$] ##1
c&y))
iff not({\bar w} |= (!c[*0:$] ##1 c&x))
and
not({\bar w} |= (!c[*0:$] ##1 c&y))
iff not(there exists 0 <= i < |w| such that
{\bar w}^{0..i} |== (!c[*0:$] ##1 c&x))
and
not(there exists 0 <= i < |w| such that
{\bar w}^{0..i} |== (!c[*0:$] ##1 c&y))
iff not(there exists 0 <= i < |w| such that {\bar w}^{0..i} is a
clock tick of c and {\bar w}^i ||= x)
and
not(there exists 0 <= i < |w| such that {\bar w}^{0..i} is a
clock tick of c and {\bar w}^i ||= y)
I am using Verilog flavor PSL, so "|" goes to "||".
In PSL,
w |=(true) (!(x! || y!)) @c
iff w |=(c) !(x! | y!)
iff not({\bar w} |=(c) (x! || y!))
iff not({\bar w} |=(c) x! or {\bar w} |=(c) y!)
iff not({\bar w} |=(c) x!)
and
not({\bar w} |=(c) y!)
iff not(there exists 0 <= i < |w| such that {\bar w}^{0..i} is a
clock tick of c and {\bar w}^i ||= x)
and
not(there exists 0 <= i < |w| such that {\bar w}^{0..i} is a
clock tick of c and {\bar w}^i ||= y)
Thus, at the property level, "@(c) not(x or y)" looks
to me to be equivalent to "(!(x! || y!)) @c".
When you add the "initial assert property" in SVA, the SVA semantics
has the enabling condition. This makes a difference if w is
empty or if the first letter of w does not satisfy the enabling
condition. So let's assume that w is non-empty, the enabling
condition is 1, and w is proper. [Recall that w proper means
that for all 0 <= i < |w|, if w^i \in {\top, \bot}, then w is
infinite and w^j = w^i for all j >= i.]
w,1 |= initial assert property @(c) not(x or y)
iff if {\bar w}^0 ||= 1, then w |= @(c) not(x or y)
iff not({\bar w}^0 ||= 1) or w |= @(c) not (x or y)w
iff |w| = 0 or {\bar w}^0 = \bot or w |= @(c) not(x or y)
iff [we assumed |w| > 0]
{\bar w}^0 = \bot or w |= @(c) not(x or y)
iff w^0 = \top or w |= @(c) not(x or y)
iff [we assumed w is proper]
w = \top^\omega or w |= @(c) not(x or y)
iff [@(c) not(x or y) is non-degenerate, so
\top^\omega |= @(c) not(x or y)]
w |= @(c) not(x or y)
Thus, at the assertion level, "initial assert property @(c) not(x or y)"
looks to me to be equivalent to "(!(x! || y!)) @c" provided w is proper
and non-empty.
I am not worried about alignment on non-proper words. So the only case
left that I care about is w empty. This is not yet defined in the
SVA semantics, but I guess SVA would define
w,b |= initial assert property Q
iff if |w| > 0 and {\bar w}^0 ||= b, then w |= Q
so
emptyword,1 |= intial assert property Q
and it is easy to see that in PSL
emptyword |=(true) (!(x! || y!)) @c
since the clock ticks do not exist.
What do you think?
Best regards,
John H.
>
> Hi John,
>
> I agree that clocked Booleans in SVA are strong, and thus the
> translation of b matches (b!) in PSL. But then the two semantics do =
> not
> agree on
>
> initial assert @(c) not (x or y)
> vs.
> (!(x! | y!)) @c
>
> Is that right?
>
> Regards,
> Roy
>
>
>
> -----Original Message-----
> From: John Havlicek [mailto:john.havlicek@motorola.com]=20
> Sent: Tuesday, October 28, 2003 10:18 PM
> To: Armoni, Roy
> Cc: EISNER@il.ibm.com; sv-ac@eda.org
> Subject: Re: [sv-ac] negated boolean proposal
>
>
> Hi Roy:
>
> As you know, there has been a lot of work in the SVA/PSL Alignment
> Subcommittee
> to define a mapping from a subset of SVA to PSL and to prove semantic
> correspondence under the mapping.
>
> In the proposed PSL 1.1, strong booleans are ornamented with a
trailing
> "!",=20
> while in SVA 3.1, the naked boolean is strong. This is not
> syntactically
> aligned, but it is (fairly well) semantically aligned. The mapping
> accounts=20
> for the syntactic difference at the property level by defining=20
>
> T(@(c) b) =3D {M(@(c)b)}!
> =3D {M(b)@c}!
> =3D {b@c}!
>
> The weak boolean can be expressed in SVA 3.1 using a device, such
as=20
> not(!b or !b).
>
> Best regards,
>
> John H.
>
>
> >=20
> > Hi Cindy,
> >=20
> > The reason I wrote that the proposed change will not create a
> disruption
> > to the alignment effort is because SVA and PSL are not fully
aligned.
> > Take for instance the SVA formula
> > initial assert @(c) b
> > which is a liveness property in SVA, while a straightforward rewrite
> to
> > PSL results in
> > b@c
> > which is a safety property. I believe that a similar effect is
> created
> > when "initial" is replaced by "always".
> >=20
> > In general, I wouldn't underestimate the effect of liveness =
> properties
> > that are created without the user intention.
> >=20
> > Regards,
> > Roy
> >=20
> >=20
> > -----Original Message-----
> > From: Cindy Eisner [mailto:EISNER@il.ibm.com]=20
> > Sent: Tuesday, October 21, 2003 11:03 AM
> > To: Armoni, Roy
> > Cc: john.havlicek@motorola.com; sv-ac@eda.org; Dana Fisman;
> > dana@wisdom.weizmann.ac.il
> > Subject: RE: [sv-ac] negated boolean proposal
> >=20
> >=20
> > roy,
> >=20
> > i disagree that what you have in mind does not cause disruption to =
> the
> > alignment efforts. changing to immediate booleans is a huge
> disruption,
> > as
> > it is completely opposite to the approach taken in psl.
> >=20
> > i would not worry too much about generations of engineers pondering
> the
> > strength of boolean expressions. first, i have never known one to
> worry
> > about it yet. second, the issue is relevant only on infinite paths
> > where
> > the clock never ticks. so i don't see much potential for future =
> worry
> > from
> > the user community either.
> >=20
> > regards,
> >=20
> > cindy.
> >=20
> > --------------------------------------------------------------------
> > Cindy Eisner
> > Formal Methods Group
> > IBM Haifa Research Laboratory
> > Haifa 31905, Israel
> > Tel: +972-4-8296-266
> > Fax: +972-4-8296-114
> > e-mail: eisner@il.ibm.com
> >=20
> >=20
> > "Armoni, Roy" <roy.armoni@intel.com>@eda.org on 10/16/2003 05:36:56
=
> PM
> >=20
> > Sent by: owner-sv-ac@eda.org
> >=20
> >=20
> > To: <john.havlicek@motorola.com>
> > cc: <sv-ac@eda.org>
> > Subject: RE: [sv-ac] negated boolean proposal
> >=20
> >=20
> > Hi John,
> >=20
> > * Yes, what I have in mind requires changing to immediate Booleans.
> >=20
> > * No, it does not require rewriting the entire SVA formal semantics.
> > Actually, after reviewing again the way SVA semantics is written, =
> then
> > in addition to your proposal, it requires only one line change, that
> is
> > the rewrite rule of ##1 has to be changed to:
> > @(c) (R1 ##1 R2) --> ( (@(c) R1) ##1 !c[*0:$] ##1 c ##0 (@(c) R2) )
> >=20
> > * No, it will not cause any disruption whatsoever to the current =
> state
> > of the alignment between SVA and PSL.
> >=20
> > * The significant of this change is for generations of engineers for
> > whom we will save the bother of figuring out the strength of a
> property
> > and its strength under negation.
> >=20
> > Regards,
> > Roy
> >=20
> >=20
> > -----Original Message-----
> > From: John Havlicek [mailto:john.havlicek@motorola.com]
> > Sent: Thursday, October 16, 2003 4:08 PM
> > To: Armoni, Roy
> > Cc: john.havlicek@motorola.com; sv-ac@eda.org
> > Subject: Re: [sv-ac] negated boolean proposal
> >=20
> >=20
> > Roy:
> >=20
> > Can you be more specific about what you have in mind?
> > I have the following questions about it.
> >=20
> > * Does it require changing to immediate booleans?
> >=20
> > * Does it require rewriting the entire SVA formal semantics?
> >=20
> > * Will it cause significant disruption of the current alignment
> > between SVA and PSL semantics?
> >=20
> > * How significant is the change in practice?
> >=20
> > Best regards,
> >=20
> > John H.
> >=20
> > >
> > > Hi John,
> > >
> > > Thanks for raising this issue. The difference in the semantics
> > between
> > > 1. on one hand and 3.,4.,5. on the other hand is indeed bothering.
> At
> > > the same time, I believe that 1. and 2. should have exactly the =
> same
> > > meaning - the difference between "!" and "not" is only syntactic.
> > >
> > > I believe that there is no real dilemma here and we can make all
of
> > > 1.-5. equivalent, but it requires some work, much more than the
> small
> > > change in your proposal. However, I am willing to invest this
work
> > for
> > > the benefit of all the future SVAs that are going to be written
out
> > > there.
> > >
> > > I wonder what is the committee's take on this?
> > >
> > > Thanks,
> > >
> > > Roy
> > >
> > >
This archive was generated by hypermail 2b28 : Wed Oct 29 2003 - 22:05:20 PST