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

Hi Ed:

By "allow the leading clocks of the operand properties to
be whatever they are" I mean that there is no restriction on
the leading clocks of the operands.  E.g.,

   assert property (@(clk1) (@(clk2) P) until (@(clk3) Q));

should be legal.

J.H.

> X-MimeOLE: Produced By Microsoft Exchange V6.5
> Content-class: urn:content-classes:message
> Date: Thu, 31 Jan 2008 12:30:13 -0800
> Thread-Topic: [sv-ac] Comment regarding LTL - Mantis 1932
> Thread-Index: AchkRwhyIhUGMYjnQmOrGUOYcXKN+gAANq1g
> From: "Eduard Cerny" <Eduard.Cerny@synopsys.com>
> Cc: <doron.bustan@intel.com>, <sv-ac@eda.org>
> X-OriginalArrivalTime: 31 Jan 2008 20:30:14.0138 (UTC) FILETIME=[1582DDA0:01C86448]
> 
> Hi John,
> 
> I am not sure I understand " leading clocks of the operand properties to
> be whatever they are". Does it mean that they must be the same in until.
> If not, that would be a bit unfortunate...
> 
> best...
> ed
> 
> -----Original Message-----
> From: John Havlicek [mailto:john.havlicek@freescale.com]=20
> Sent: Thursday, January 31, 2008 3:21 PM
> To: Eduard.Cerny@synopsys.COM
> Cc: john.havlicek@freescale.com; doron.bustan@intel.com;
> Eduard.Cerny@synopsys.COM; sv-ac@eda.org
> Subject: 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=3D[50EA9630:01C86286]
> >=20
> > Hi John,
> >=20
> > I agree with requiring the same clock in until, inherited. It was more
> a
> > question, no contest.
> >=20
> > Regarding the vacuity definition, yes, negation poses problems once
> you
> > add the success condition, I tried that too and gave up.=3D20
> >=20
> > Regards,
> > ed
> >=20
> > > -----Original Message-----
> > > From: owner-sv-ac@eda.org [mailto:owner-sv-ac@eda.org] On=3D20
> > > 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;=3D20
> > > sv-ac@eda.org
> > > Subject: Re: [sv-ac] Comment regarding LTL - Mantis 1932
> > >=3D20
> > > Hi Doron, Ed:
> > >=3D20
> > > > >>Regarding the leading clock in until. My point is that=3D20
> > > the rule deals
> > > > with
> > > > >>the case when some clock v flows in P1 until P2. But what=3D20
> > > 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.)
> > > > >>
> > > >=3D20
> > > > [[DB:]] Since the leading clock of until is inherited,=3D20
> > > there must be a
> > > > clock flowing from the left into the until property; so=3D20
> > > unless there is
> > > > an inferred clock, the assertion "assert property (P1 until P2);"
> is
> > > > illegal.
> > >=3D20
> > > I agree with Doron that if no clock flows in, then this think that
> > >=3D20
> > >    assert property (P1 until P2);=3D20
> > >=3D20
> > > 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.
> > >=3D20
> > > >=3D20
> > > > The rule in item c) says "- Every explicit semantic leading=3D20
> > > clock of P1
> > > > or P2 is identical to c."  I think this match your intuition
> > > >=3D20
> > > >=3D20
> > > > >>In the formal part, vacuity, in the case of P1 or P2, it=3D20
> > > seems to me
> > > > that
> > > > >>if P1 has vacuous success and P2 is non-vacuous failure,=3D20
> > > 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.=3D20
> > > However, it is not
> > > > part of 1932. We tried to give a conservative definition (no false
> > > > negatives) and keep the definition indifferent to negation.=3D20
> > > I think that
> > > > sometime in the future we will have to find a better definition.
> > >=3D20
> > > 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
> > >=3D20
> > >    w |=3D3D^{non} not p
> > >=3D20
> > > iff=3D20
> > >=3D20
> > >    w |=3D3D^{non} p
> > >=3D20
> > > I think that if we want
> > >=3D20
> > >    (w |=3D3D p or q)  and  (w |=3D3D^{non} p or q)
> > >=3D20
> > > to imply that=3D20
> > >=3D20
> > >    either
> > >       w |=3D3D p and w^{non} |=3D3D p=3D20
> > >    or=3D20
> > >       w |=3D3D q and w^{non} |=3D3D q
> > >=3D20
> > > then we will need to recouple the concepts.  This seems to provide
> > > some chanllenges for negated formulas.
> > >=3D20
> > > J.H.
> > > =3D20
> > >   =3D20
> > >=3D20
> > > --=3D20
> > > This message has been scanned for viruses and
> > > dangerous content by MailScanner, and is
> > > believed to be clean.
> > >=3D20
> > >=3D20

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