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
> 
>