Re: [sv-ac] an example for discussion of 1668

Hi Dmitry:

I agree that this example can be rewritten in 
other ways.

Your version is a combination of the rewrite shown 
in the sketch for 1667 and a second rewrite to 
eliminate the local variable declaration assignment.

I believe that your version has the desired 
semantics.  But I do not conclude from this that 
we do not need local variable arguments.

An even simpler representation, without local variables
at all, is 

   assert property (
       @(ev1) sig_a |=> @(ev2) sig_b ##1 !sig_b
   );

I am encouraged that we agree that the local variable
argument v in my original example needs to get its
initial assignment when we get to the timestep of the
new clock @(ev2).  That was the main point I was trying
to argue.

J.H.


> X-ExtLoop1: 1
> X-IronPort-AV: i="4.14,333,1170662400"; 
>    d="scan'208"; a="203470373:sNHT12938509185"
> X-MimeOLE: Produced By Microsoft Exchange V6.5
> Content-class: urn:content-classes:message
> Date: Tue, 27 Mar 2007 11:32:27 +0200
> X-MS-Has-Attach: 
> X-MS-TNEF-Correlator: 
> Thread-Topic: [sv-ac] an example for discussion of 1668
> Thread-Index: AcdvyAvAMVTHlPTnSb2kfEJ5++LECgAhkJAw
> From: "Korchemny, Dmitry" <dmitry.korchemny@intel.com>
> X-OriginalArrivalTime: 27 Mar 2007 09:36:13.0841 (UTC) FILETIME=[5C6A3810:01C77053]
> 
> Hi John,
> 
> Why cannot the user write these properties as:
> 
>    property q(logic sig);
> 	 logic v;
>        (sig, v =3D !sig) |-> sig_b ##1 v;
>    endproperty
> 
>    assert property (
>       @(ev1) sig_a |=3D> @(ev2) q(sig_b)
>    );
> ?
> 
> Thanks,
> Dmitry
> 
> -----Original Message-----
> From: owner-sv-ac@server.eda.org [mailto:owner-sv-ac@server.eda.org] On
> Behalf Of John Havlicek
> Sent: Monday, March 26, 2007 6:57 PM
> To: sv-ac@server.eda-stds.org
> Subject: [sv-ac] an example for discussion of 1668
> 
> Hi Dmitry:
> 
> I had an action item to send you an example to help
> us discuss the problem of local variable initialization
> when the clock is changing and a signal is being assigned
> to the local variable in the initialization.
> 
> Here is an example that I think covers this situation:
> 
>    property q(input local logic v);
>        (v, v =3D !v) |-> sig_b ##1 v;
>    endproperty
> 
>    assert property (
>       @(ev1) sig_a |=3D> @(ev2) q(sig_b)
>    );
> 
> J.H.
> 
> --=20
> This message has been scanned for viruses and
> dangerous content by MailScanner, and is
> believed to be clean.

-- 
This message has been scanned for viruses and
dangerous content by MailScanner, and is
believed to be clean.