Re: [sv-ac] non-urgency of 1668

Hi Dmitry:

O.k., your example now makes sense to me, but 
I'm missing the point you are trying to make.

In the spirit of the sketch for 1667 your
example could become (exact syntax has not been
defined yet)

   property q(input local bit w);
       (w, w = !w) |-> b ##1 w ##1 c;
   endproperty
   
   property p;
       bit v;
       (a, v = a) |=> q(v);
   endproperty
   
   assert property (@(posedge clk) p);

I don't see any ambiguity or issue here.  You definitely
want the value of "v" that is assigned by "v = a" to get
put into "w" before you test "w" at the beginning of q. 
The implicit initialization assignment from the sketch
of 1667 will do that.

J.H.

> X-ExtLoop1: 1
> X-IronPort-AV: i="4.14,298,1170662400"; 
>    d="scan'208"; a="214899800:sNHT70664706"
> X-MimeOLE: Produced By Microsoft Exchange V6.5
> Content-class: urn:content-classes:message
> Date: Mon, 19 Mar 2007 08:45:34 +0200
> X-MS-Has-Attach: 
> X-MS-TNEF-Correlator: 
> Thread-Topic: [sv-ac] non-urgency of 1668
> thread-index: AcdiRgaxUh0UFG8lTUOtdoLTWLbGuAHFrBTQAA+ALcAAFcp/oA==
> From: "Korchemny, Dmitry" <dmitry.korchemny@intel.com>
> X-OriginalArrivalTime: 19 Mar 2007 06:46:12.0758 (UTC) FILETIME=[48CA7B60:01C769F2]
> 
> Yes, of course. It should have been:=20
> 
> property q(w);
>     (w, w =3D !w) |-> b ##1 w ##1 c;
> endproperty
> 
> property p;
>     bit v;
>     (a, v =3D a) |=3D> q(v);
> endproperty
> 
> assert property (@(posedge clk) p);
> 
> is equivalent to (I am using pseudo syntax here):
> 
> assert property (@(posedge clk) ( bit v: (a, v =3D a) |=3D> (v, v=20
> =3D !v) |-> b ##1 v ##1 c));
> 
> Thanks,
> Dmitry
> 
> -----Original Message-----
> From: Eduard Cerny [mailto:Eduard.Cerny@synopsys.com]=20
> Sent: Sunday, March 18, 2007 10:20 PM
> To: Korchemny, Dmitry; john.havlicek@freescale.com; sv-ac@eda-stds.org
> Subject: RE: [sv-ac] non-urgency of 1668
> 
> I think that you need a formal arg v in q and then pass the actual v t o
> the instance of q.
> ed
> =20
> 
> > -----Original Message-----
> > From: owner-sv-ac@eda.org [mailto:owner-sv-ac@eda.org] On=20
> > Behalf Of Korchemny, Dmitry
> > Sent: Sunday, March 18, 2007 10:46 AM
> > To: john.havlicek@freescale.com; sv-ac@eda-stds.org
> > Subject: RE: [sv-ac] non-urgency of 1668
> >=20
> > Hi John,
> >=20
> > It highly depends on the parameter passing semantics. If we adopt the
> > substitution semantics, then the meaning of passing a local variable
> > will be slightly different. E.g.,
> >=20
> > property q;
> >     (v, v =3D !v) |-> b ##1 v ##1 c;
> > endproperty
> >=20
> > property p;
> >     bit v;
> >     (a, v =3D a) |=3D> q;
> > endproperty
> >=20
> > assert property (@(posedge clk) p);
> >=20
> > is equivalent to (I am using pseudo syntax here):
> >=20
> > assert property (@(posedge clk) ( bit v: (a, v =3D a) |=3D> (v, v=20
> > =3D !v) |->
> > b ##1 v ##1 c));
> >=20
> > Thanks,
> > Dmitry
> >=20
> > -----Original Message-----
> > From: owner-sv-ac@server.eda.org=20
> > [mailto:owner-sv-ac@server.eda.org] On
> > Behalf Of John Havlicek
> > Sent: Friday, March 09, 2007 2:24 PM
> > To: sv-ac@server.eda-stds.org
> > Subject: [sv-ac] non-urgency of 1668
> >=20
> > Hi All:
> >=20
> > In our last meeting, we decided that 1668 is not urgent.
> >=20
> > I have thought some more about this and realized that=20
> > more of 1667 than just assignments in the formal argument
> > list is dependent on 1668.
> >=20
> > Indeed, the basic semantics of binding an actual argument=20
> > expression to a local variable formal argument will be the=20
> > same as a similar local variable declaration assignment, as in
> > the current sketch for 1667:
> >=20
> >    property p(local <type> v, ...);
> >       ...
> >    endproperty
> >=20
> >    ...
> >=20
> >    p(.v(e),...)
> >=20
> > should have the same semantics as
> >=20
> >    property p(<type> v1, ...);
> >       <type> v =3D v1;
> >       ...
> >    endproperty
> >=20
> >    ...
> >=20
> >    p(.v1(e),...)
> >=20
> >=20
> > It is clear to me that for 1667 we do not want a restriction=20
> > that says that e must be a constant expression.
> >=20
> > So, I am of the mind now that we really do need to make=20
> > progress to converge on 1668 before I can do anything with
> > 1667.
> >=20
> > Best regards,
> >=20
> > J.H.
> >=20
> > --=20
> > This message has been scanned for viruses and
> > dangerous content by MailScanner, and is
> > believed to be clean.
> >=20
> > --=20
> > This message has been scanned for viruses and
> > dangerous content by MailScanner, and is
> > believed to be clean.
> >=20
> >=20
> >=20

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