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

From: John Havlicek <john.havlicek_at_.....>
Date: Mon Mar 19 2007 - 04:55:48 PDT
Hi Dmitry:

Your example makes no sense to me.

Your declared property "q" should not parse
because the "v" on the left side of the assignment
"v = !v" is not a declared variable or formal 
argument.

J.H.

> X-ExtLoop1: 1
> X-IronPort-AV: i="4.14,297,1170662400"; 
>    d="scan'208"; a="60170697:sNHT2893134555"
> X-MimeOLE: Produced By Microsoft Exchange V6.5
> Content-class: urn:content-classes:message
> Date: Sun, 18 Mar 2007 16:46:23 +0200
> X-MS-Has-Attach: 
> X-MS-TNEF-Correlator: 
> Thread-Topic: [sv-ac] non-urgency of 1668
> thread-index: AcdiRgaxUh0UFG8lTUOtdoLTWLbGuAHFrBTQ
> From: "Korchemny, Dmitry" <dmitry.korchemny@intel.com>
> X-OriginalArrivalTime: 18 Mar 2007 14:46:32.0353 (UTC) FILETIME=[3831F110:01C7696C]
> 
> Hi John,
> 
> 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.,
> 
> property q;
>     (v, v =3D !v) |-> b ##1 v ##1 c;
> endproperty
> 
> property p;
>     bit v;
>     (a, v =3D a) |=3D> q;
> 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 =3D =
> !v) |->
> b ##1 v ##1 c));
> 
> Thanks,
> Dmitry
> 
> -----Original Message-----
> From: owner-sv-ac@server.eda.org [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
> 
> Hi All:
> 
> In our last meeting, we decided that 1668 is not urgent.
> 
> 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.
> 
> 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:
> 
>    property p(local <type> v, ...);
>       ...
>    endproperty
> 
>    ...
> 
>    p(.v(e),...)
> 
> should have the same semantics as
> 
>    property p(<type> v1, ...);
>       <type> v =3D v1;
>       ...
>    endproperty
> 
>    ...
> 
>    p(.v1(e),...)
> 
> 
> It is clear to me that for 1667 we do not want a restriction=20
> that says that e must be a constant expression.
> 
> 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.
> 
> Best regards,
> 
> 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.
Received on Mon Mar 19 04:56:18 2007

This archive was generated by hypermail 2.1.8 : Mon Mar 19 2007 - 04:56:42 PDT