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