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

Hi John,

Of course, if you want to use an input local variable argument you need
to define the initialization semantics, and these two tasks are
equivalent. I just wanted to see a usage example where such an
initialization makes the code more readable or easier to write. We
definitely need local variable arguments, but this does not necessarily
mean that we need input local variable arguments (though I am not
claiming here the opposite, either).

I consider you example as a usage paradigm, therefore I tried to show
how that the existing local variable mechanism does the work, and didn't
try to eliminate the local variables in it altogether.

Thanks,
Dmitry

-----Original Message-----
From: John Havlicek [mailto:john.havlicek@freescale.com] 
Sent: Tuesday, March 27, 2007 1:42 PM
To: Korchemny, Dmitry
Cc: john.havlicek@freescale.com; sv-ac@eda-stds.org
Subject: 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.