Re: [sv-ac] Comment regarding LTL - Mantis 1932

Hi Ed:

I just want to clarify that I believe that the semantic leading
clock of an until should be inherited.

1683 was passed by the P1800 Working Group today, so I think that
we should allow the leading clocks of the operand properties to
be whatever they are.

J.H.

> X-MimeOLE: Produced By Microsoft Exchange V6.5
> Content-class: urn:content-classes:message
> Date: Tue, 29 Jan 2008 06:50:38 -0800
> Thread-Topic: [sv-ac] Comment regarding LTL - Mantis 1932
> Thread-Index: AchiH5ZJHr0hrjnUTZKEy51nIY9rYAAZneSw
> From: "Eduard Cerny" <Eduard.Cerny@synopsys.com>
> Cc: <Eduard.Cerny@synopsys.com>, <sv-ac@eda.org>
> X-OriginalArrivalTime: 29 Jan 2008 14:50:40.0275 (UTC) FILETIME=[50EA9630:01C86286]
> 
> Hi John,
> 
> I agree with requiring the same clock in until, inherited. It was more a
> question, no contest.
> 
> Regarding the vacuity definition, yes, negation poses problems once you
> add the success condition, I tried that too and gave up.=20
> 
> Regards,
> ed
> 
> > -----Original Message-----
> > From: owner-sv-ac@eda.org [mailto:owner-sv-ac@eda.org] On=20
> > Behalf Of John Havlicek
> > Sent: Monday, January 28, 2008 9:35 PM
> > To: doron.bustan@intel.com
> > Cc: Eduard.Cerny@synopsys.COM; john.havlicek@freescale.com;=20
> > sv-ac@eda.org
> > Subject: Re: [sv-ac] Comment regarding LTL - Mantis 1932
> >=20
> > Hi Doron, Ed:
> >=20
> > > >>Regarding the leading clock in until. My point is that=20
> > the rule deals
> > > with
> > > >>the case when some clock v flows in P1 until P2. But what=20
> > if there is
> > > no
> > > >>clock flowing in? E.g. Assert property (P1 until P2);
> > > >>Does the leading clock of P1 have to be the same as in P2? (I hope
> > > so.)
> > > >>
> > >=20
> > > [[DB:]] Since the leading clock of until is inherited,=20
> > there must be a
> > > clock flowing from the left into the until property; so=20
> > unless there is
> > > an inferred clock, the assertion "assert property (P1 until P2);" is
> > > illegal.
> >=20
> > I agree with Doron that if no clock flows in, then this think that
> >=20
> >    assert property (P1 until P2);=20
> >=20
> > is illegal.  Whether or not the semantic leading clock of P1 and P1
> > must be identical and identicla to the inherited clock depend on 1683.
> > If 1683 is rejected, then any non-inherited clocks of P1 and P2 must
> > be identical and also identical to the inherited clock.
> >=20
> > >=20
> > > The rule in item c) says "- Every explicit semantic leading=20
> > clock of P1
> > > or P2 is identical to c."  I think this match your intuition
> > >=20
> > >=20
> > > >>In the formal part, vacuity, in the case of P1 or P2, it=20
> > seems to me
> > > that
> > > >>if P1 has vacuous success and P2 is non-vacuous failure,=20
> > it would be
> > > >>declared as non-vacuous success. That looks strange. Or did I miss
> > > >>something?
> > > >>
> > > [[DB:]] I think you are right, and this is bothering.=20
> > However, it is not
> > > part of 1932. We tried to give a conservative definition (no false
> > > negatives) and keep the definition indifferent to negation.=20
> > I think that
> > > sometime in the future we will have to find a better definition.
> >=20
> > This seems to be an inevitable consequence of decoupling "success"
> > from "vacuity".  Our basic intuition has been that non-vacuity is
> > oblivious to negation because of the rule
> >=20
> >    w |=3D^{non} not p
> >=20
> > iff=20
> >=20
> >    w |=3D^{non} p
> >=20
> > I think that if we want
> >=20
> >    (w |=3D p or q)  and  (w |=3D^{non} p or q)
> >=20
> > to imply that=20
> >=20
> >    either
> >       w |=3D p and w^{non} |=3D p=20
> >    or=20
> >       w |=3D q and w^{non} |=3D q
> >=20
> > then we will need to recouple the concepts.  This seems to provide
> > some chanllenges for negated formulas.
> >=20
> > J.H.
> > =20
> >   =20
> >=20
> > --=20
> > This message has been scanned for viruses and
> > dangerous content by MailScanner, and is
> > believed to be clean.
> >=20
> >=20

-- 
This message has been scanned for viruses and
dangerous content by MailScanner, and is
believed to be clean.