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