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

Hi Dmitry:

This is great progress.

We are agreeing on the semantics under the assumption
that the feature exists.

We can talk more about the need for the feature.

J.H.

> X-ExtLoop1: 1
> X-IronPort-AV: i="4.14,335,1170662400"; 
>    d="scan'208"; a="203633037:sNHT44438877"
> X-MimeOLE: Produced By Microsoft Exchange V6.5
> Content-class: urn:content-classes:message
> Date: Tue, 27 Mar 2007 17:22:59 +0200
> X-MS-Has-Attach: 
> X-MS-TNEF-Correlator: 
> Thread-Topic: [sv-ac] an example for discussion of 1668
> Thread-Index: AcdwZPIUwhCQFrFNQyGvaLyczPAjBgAHSgJQ
> From: "Korchemny, Dmitry" <dmitry.korchemny@intel.com>
> Cc: <sv-ac@eda-stds.org>
> X-OriginalArrivalTime: 27 Mar 2007 15:23:05.0304 (UTC) FILETIME=[D1037580:01C77083]
> 
> 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]=20
> 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=20
> other ways.
> 
> Your version is a combination of the rewrite shown=20
> in the sketch for 1667 and a second rewrite to=20
> eliminate the local variable declaration assignment.
> 
> I believe that your version has the desired=20
> semantics.  But I do not conclude from this that=20
> we do not need local variable arguments.
> 
> An even simpler representation, without local variables
> at all, is=20
> 
>    assert property (
>        @(ev1) sig_a |=3D> @(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=3D"4.14,333,1170662400";=20
> >    d=3D"scan'208"; a=3D"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:=20
> > X-MS-TNEF-Correlator:=20
> > 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=3D[5C6A3810:01C77053]
> >=20
> > Hi John,
> >=20
> > Why cannot the user write these properties as:
> >=20
> >    property q(logic sig);
> > 	 logic v;
> >        (sig, v =3D3D !sig) |-> sig_b ##1 v;
> >    endproperty
> >=20
> >    assert property (
> >       @(ev1) sig_a |=3D3D> @(ev2) q(sig_b)
> >    );
> > ?
> >=20
> > Thanks,
> > Dmitry
> >=20
> > -----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
> >=20
> > Hi Dmitry:
> >=20
> > 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.
> >=20
> > Here is an example that I think covers this situation:
> >=20
> >    property q(input local logic v);
> >        (v, v =3D3D !v) |-> sig_b ##1 v;
> >    endproperty
> >=20
> >    assert property (
> >       @(ev1) sig_a |=3D3D> @(ev2) q(sig_b)
> >    );
> >=20
> > J.H.
> >=20
> > --=3D20
> > 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.