Re: [sv-ac] Issue #921

Hi Dimitry,

as far as I remember, in both the tight and loose approaches, in both 
examples,
a display is executed iff a holds at the first cycle.

Doron

Korchemny, Dmitry wrote:

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