RE: [sv-ac] Issue #921

Dmitry, I think that the notion of threads being spawned from OR
operations are already established among users (well, some of them), so
it may not be that counterintuitive. 
ed


> -----Original Message-----
> From: Korchemny, Dmitry [mailto:dmitry.korchemny@intel.com] 
> Sent: Tuesday, March 28, 2006 9:50 AM
> To: Eduard Cerny; john.havlicek@freescale.com
> Cc: sv-ac@eda.org
> Subject: RE: [sv-ac] Issue #921
> 
> Hi Ed,
> 
> In my understanding, the action in the 'not' form depends on the tight
> or loose semantics, while the '|->' form should always print 
> a message.
> 
> I am also concerned with automata optimization, and I am not sure that
> the subroutine call semantics may be defined intuitively 
> enough for the
> language user.
> 
> Regards,
> Dmitry
> 
> -----Original Message-----
> From: Eduard Cerny [mailto:Eduard.Cerny@synopsys.com] 
> Sent: Tuesday, March 28, 2006 4:43 PM
> To: Korchemny, Dmitry; john.havlicek@freescale.com
> Cc: sv-ac@eda.org
> Subject: RE: [sv-ac] Issue #921
> 
> Hello Dmitry, John,
> 
> apart from one having a success and the other a vacuous success, why
> would there be a diff as far as $display execution is concerned?
> 
> Somehow the "loose" approach is more appealing to me, but it could
> preclude possible optimizations on the automata.  At one 
> time, John you
> said that we could have both approaches supported, but would the user
> choose? Or would it be automatic, if there are side effects then the
> loose or lazy approach would take over?
> 
> ed
> 
> > -----Original Message-----
> > From: owner-sv-ac@eda.org [mailto:owner-sv-ac@eda.org] On 
> > Behalf Of Korchemny, Dmitry
> > Sent: Tuesday, March 28, 2006 9:28 AM
> > To: john.havlicek@freescale.com
> > Cc: sv-ac@eda.org
> > Subject: RE: [sv-ac] Issue #921
> > 
> > Hi John,
> > 
> > My problem is that the sequences are typically negated when 
> > used without
> > implication in properties. 
> > 
> > Consider two examples:
> > 
> > assert property (not((a, $display(...)) ##1 b));
> > and
> > assert property ((a, $display(...)) ##1 b|-> false);
> > 
> > These properties are equivalent, but their semantics would be 
> > different.
> > 
> > My guess is that examples provided by you are more usable with cover
> > property statements rather than with assertions or assumptions.
> > 
> > [My Outlook setting should be wrong, and therefore we are 
> > always getting
> > the garbage characters in my mails. I suspect that this one 
> will have
> > the same problem, but I don't know what should be fixed.]
> > 
> > Thanks,
> > Dmitry
> > 
> > -----Original Message-----
> > From: John Havlicek [mailto:john.havlicek@freescale.com] 
> > Sent: Tuesday, March 28, 2006 4:03 PM
> > To: Korchemny, Dmitry
> > Cc: john.havlicek@freescale.com; sv-ac@eda.org
> > Subject: Re: [sv-ac] Issue #921
> > 
> > Hi Dmitry:
> > 
> > First, the execution of the subroutines is not well-defined.
> > That is the issue that has been raised.
> > 
> > I can give you my intuition for various examples, but it is 
> > up to us to come up with a definition and check it with due 
> > diligence.
> > 
> > For 
> > 
> >    assert property (
> >      ((a, x = 0) or (b, x = 1)) 
> >      ##1 (1, $display("x = %b", x)
> >    );
> > 
> > [I reformatted and added a parenthesis], my intuition is that
> > if a and b both hold at a clock event, then you should get two 
> > displays at the next clock event.  
> > 
> > [Since this mail is going to the reflector archive, let's also 
> > acknowledge here that we understand that in order to use local 
> > variables, we have to have a declared property -- for the purposes 
> > of this discussion, we are looking at results of substituting 
> > the bodies of property declarations into assertion directives.]
> > 
> > For 
> > 
> >    assert property (
> >       not (
> >          ((a, x = 0) or (b, x = 1)) ##1 (1, $display("x = %b", x))
> >       )
> >    );
> > 
> > [I again reformatted and adjusted parentheses--let me know if 
> > I changed what you intended], I am not so sure.  This really 
> > depends on the "when" part of the definition of execution of 
> > subroutines.  A tight approach could detect failure of the property 
> > in the first cycle.  A loose approach could let the "threads" run, 
> > in which case I think you should see displays as above.
> > 
> > We should check what the current document in mantis says about 
> > this example.
> > 
> > Best regards,
> > 
> > John H.
> > 
> > > X-IronPort-AV: i="4.03,137,1141632000"; 
> > >    d="scan'208"; a="15756833:sNHT36897112"
> > > X-MimeOLE: Produced By Microsoft Exchange V6.5
> > > Content-class: urn:content-classes:message
> > > Date: Tue, 28 Mar 2006 14:50:16 +0200
> > > X-MS-Has-Attach: 
> > > X-MS-TNEF-Correlator: 
> > > Thread-Topic: [sv-ac] Issue #921
> > > thread-index: AcZSZTHBF5Y7HOeVTOeoW7FUQnvMlwAAIhyg
> > > From: "Korchemny, Dmitry" <dmitry.korchemny@intel.com>
> > > Cc: <sv-ac@eda.org>
> > > X-OriginalArrivalTime: 28 Mar 2006 12:50:21.0257 (UTC)
> > FILETIME=[2C73DB90:01C65266]
> > > 
> > > Let's consider two assertions:
> > > 
> > > assert property ((a, x =3D 0) or (b, x =3D 1)) ##1 (1, $display("x
> > =3D3D =
> > > %b",
> > > x)); assert property (not ((a, x =3D 0) or (b, x =3D 1)) ##1 (1, =
> > > $display("x
> > > =3D3D %b", x)));
> > > 
> > > What shall I get in each case?
> > > 
> > > What about assumptions?
> > > 
> > > Thanks,
> > > Dmitry
> > > -----Original Message-----
> > > From: John Havlicek [mailto:john.havlicek@freescale.com]=20
> > > Sent: Tuesday, March 28, 2006 2:43 PM
> > > To: Korchemny, Dmitry
> > > Cc: sv-ac@eda.org
> > > Subject: Re: [sv-ac] Issue #921
> > > 
> > > Hi Dmitry:
> > > 
> > > If a and b both hold in the first cycle, then=20
> > > there should be two displays in the second cycle,
> > > one of"x =3D 0" and one of "x =3D 1".
> > > 
> > > Intuitively, "or" forks, but does not join.
> > > 
> > > J.H.
> > > 
> > > > This is a multi-part message in MIME format.
> > > >=20
> > > > ------_=3D_NextPart_001_01C6525C.326C3F74
> > > > Content-Type: text/plain;
> > > > 	charset=3D"US-ASCII"
> > > > Content-Transfer-Encoding: quoted-printable
> > > >=20
> > > > Hi all,
> > > >=20
> > > > =3D20
> > > >=20
> > > > I think that the issue is problematic altogether. Consider the
> > > following
> > > > example:
> > > >=20
> > > > =3D20
> > > >=20
> > > > ((a, x =3D3D 0) or (b, x =3D3D 1)) ##1 (1, $display("x 
> =3D3D %b",
> > x));
> > > >=20
> > > > =3D20
> > > >=20
> > > > Assume at the first cycle both a and b hold. What value will be
> > > > displayed and how many times?
> > > >=20
> > > > =3D20
> > > >=20
> > > > Thanks,
> > > >=20
> > > > Dmitry
> > > >=20
> > > >=20
> > 
> > 
>