RE: [sv-ac] Issue #921

Sorry about assumptions, stupid question.

Dmitry

-----Original Message-----
From: owner-sv-ac@eda.org [mailto:owner-sv-ac@eda.org] On Behalf Of
Korchemny, Dmitry
Sent: Tuesday, March 28, 2006 2:50 PM
To: john.havlicek@freescale.com
Cc: sv-ac@eda.org
Subject: RE: [sv-ac] Issue #921

Let's consider two assertions:

assert property ((a, x = 0) or (b, x = 1)) ##1 (1, $display("x =3D %b",
x)); assert property (not ((a, x = 0) or (b, x = 1)) ##1 (1, $display("x
=3D %b", x)));

What shall I get in each case?

What about assumptions?

Thanks,
Dmitry
-----Original Message-----
From: John Havlicek [mailto:john.havlicek@freescale.com] 
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 
there should be two displays in the second cycle,
one of"x = 0" and one of "x = 1".

Intuitively, "or" forks, but does not join.

J.H.

> This is a multi-part message in MIME format.
> 
> ------_=_NextPart_001_01C6525C.326C3F74
> Content-Type: text/plain;
> 	charset="US-ASCII"
> Content-Transfer-Encoding: quoted-printable
> 
> Hi all,
> 
> =20
> 
> I think that the issue is problematic altogether. Consider the
following
> example:
> 
> =20
> 
> ((a, x =3D 0) or (b, x =3D 1)) ##1 (1, $display("x =3D %b", x));
> 
> =20
> 
> Assume at the first cycle both a and b hold. What value will be
> displayed and how many times?
> 
> =20
> 
> Thanks,
> 
> Dmitry
> 
>