RE: [sv-ac] 1678 name resolution and the rewriting algorithm of 1549

ok

-----Original Message-----
From: John Havlicek [mailto:john.havlicek@freescale.com] 
Sent: Monday, November 05, 2007 3:36 PM
To: Bustan, Doron
Cc: john.havlicek@freescale.com; sv-ac@eda.org
Subject: Re: [sv-ac] 1678 name resolution and the rewriting algorithm of
1549

Hi Doron:

When you say "should we remove the proposal", are you talking about
1678?  1678 doesn't have a proposal.

My idea is that to resolve 1678 we should add a small amount of text,
like one or two sentences, that says that the rewriting algorithm does
not itself account for name resolution.  When following the algorithm,
extra work that is not specified in the algorithm has to be done to
keep the names straight and avoid collision or aliasing errors.

J.H.

> X-ExtLoop1: 1
> X-IronPort-AV: E=Sophos;i="4.21,372,1188802800"; 
>    d="scan'208";a="231812934"
> X-MimeOLE: Produced By Microsoft Exchange V6.5
> Content-class: urn:content-classes:message
> Date: Mon, 5 Nov 2007 14:44:31 +0200
> X-MS-Has-Attach: 
> X-MS-TNEF-Correlator: 
> Thread-Topic: [sv-ac] 1678 name resolution and the rewriting algorithm
of 1549
> Thread-Index: Acgfpw2qjZq0LSCTSbGpxJHwFun2+AAAlrwQ
> From: "Bustan, Doron" <doron.bustan@intel.com>
> Cc: <sv-ac@eda.org>
> X-OriginalArrivalTime: 05 Nov 2007 12:44:32.0540 (UTC)
FILETIME=[9D151DC0:01C81FA9]
> 
> Ok, I understand. When not limited to properties/sequences the problem
> do exists in general.
> 
> Should we remove the proposal?
> 
> Doron
> 
> -----Original Message-----
> From: owner-sv-ac@server.eda.org [mailto:owner-sv-ac@server.eda.org]
On
> Behalf Of John Havlicek
> Sent: Monday, November 05, 2007 2:26 PM
> To: Bustan, Doron
> Cc: sv-ac@server.eda.org
> Subject: Re: [sv-ac] 1678 name resolution and the rewriting algorithm
of
> 1549
> 
> Hi Doron:
> 
> The point that I keep trying to make is that if you use only the
> source code identifiers to differentiate references, then there=20
> will be collision and aliasing problems that are not specific to
> local variables.  Saying that local variable names need to be made
> unique ignores the fact that other names need to be resolved properly
> and kept straight.
> 
> Consider a nested module situation:
> 
>    module m;
> 
>       logic a;
>       ...
> 
>       module n;
>          logic a;
>          ...
> 
>          sequence s(b);
>             a =3D=3D b;
>          endsequence
>       endmodule
> 
>       sequence t;
>          a ##1 n.s(a);        =20
>       endsequence
> 
>       cover property(t);
> 
>    endmodule
> 
> If I follow the rewriting algorithm and treat the names naively, I=20
> will muddle the two a's and get something like
> 
>    cover property ( ( a ##1 (a =3D=3D (a)) ) )
> 
> when what I should have is something like
> 
>    cover property ( ( m.a ##1 (m.n.a =3D=3D (m.a)) ) )
> 
> 
> J=2EH.
> 
> > X-ExtLoop1: 1
> > X-IronPort-AV: E=3DSophos;i=3D"4.21,371,1188802800";=20
> >    d=3D"scan'208";a=3D"369838601"
> > X-MimeOLE: Produced By Microsoft Exchange V6.5
> > Content-class: urn:content-classes:message
> > Date: Mon, 5 Nov 2007 10:17:52 +0200
> > X-MS-Has-Attach:=20
> > X-MS-TNEF-Correlator:=20
> > Thread-Topic: [sv-ac] 1678 name resolution and the rewriting
algorithm
> of 1549
> > Thread-Index: AcgfBIoDvkrC3aqDSs6qs5x8Fl8PNAAfolJw
> > From: "Bustan, Doron" <doron.bustan@intel.com>
> > Cc: <sv-ac@eda.org>
> > X-OriginalArrivalTime: 05 Nov 2007 08:17:52.0773 (UTC)
> FILETIME=3D[5C7A6B50:01C81F84]
> >=20
> > Hi John,
> >=20
> > Yes you are right about the examples. I don't think that they may
> result
> > in an illegal code, but in a code that probably was not
intended.=3D20
> >=20
> > However, I don't think that it is possible to have such conflicts
> > without local variables (not necessarily as arguments.) The
conflicts
> > described in 1678 are between signals defined in an internal
sequence
> > and signals that are defined in the environment that instantiates
it.
> > The only variables that are declared inside a sequence/property are
> > local variables all other are declared outside. So I cannot see
> > conflicts in instances that do not use local variables.
> >=20
> > Am I missing something?
> >=20
> > Doron
> >=20
> > -----Original Message-----
> > From: John Havlicek [mailto:john.havlicek@freescale.com]=3D20
> > Sent: Sunday, November 04, 2007 7:01 PM
> > To: Bustan, Doron
> > Cc: john.havlicek@freescale.com; sv-ac@eda.org
> > Subject: Re: [sv-ac] 1678 name resolution and the rewriting
algorithm
> of
> > 1549
> >=20
> > Hi Doron:
> >=20
> > I think that if you take the old example from 1678
> > and apply the rewriting algorithm as it is now and=3D20
> > treat the names naively just as the identifiers that
> > appear in the source, then you will still get the=3D20
> > unintended conflicts or aliasing.
> >=20
> > Try it and let me know of you agree.  This is what
> > I wrote up in the example more carefully, so if=3D20
> > you just delete the differentiating information from
> > the names in the example, you should see the same=3D20
> > conflict.
> >=20
> > My point is that this is the kind of name resolution
> > that is handled routinely in elaboration.  It is not
> > particular to local variables.
> >=20
> > J=3D2EH.
> >=20
> > > X-ExtLoop1: 1
> > > X-IronPort-AV: E=3D3DSophos;i=3D3D"4.21,368,1188802800";=3D20
> > >    d=3D3D"scan'208";a=3D3D"311428686"
> > > X-MimeOLE: Produced By Microsoft Exchange V6.5
> > > Content-class: urn:content-classes:message
> > > Date: Sun, 4 Nov 2007 15:48:12 +0200
> > > X-MS-Has-Attach:=3D20
> > > X-MS-TNEF-Correlator:=3D20
> > > Thread-Topic: [sv-ac] 1678 name resolution and the rewriting
> algorithm
> > of 1549
> > > Thread-Index: AcgdXOsOLiYXJKC2RFifPUCfDmHMZQBjEaBg
> > > From: "Bustan, Doron" <doron.bustan@intel.com>
> > > X-OriginalArrivalTime: 04 Nov 2007 13:48:13.0407 (UTC)
> > FILETIME=3D3D[581566F0:01C81EE9]
> > >=3D20
> > > John,
> > >=3D20
> > > Can you give an example of name conflict with the up to date 1549?
> > >=3D20
> > > I don't see it.
> > >=3D20
> > > Doron
> > >=3D20
> > > -----Original Message-----
> > > From: owner-sv-ac@server.eda.org
[mailto:owner-sv-ac@server.eda.org]
> > On
> > > Behalf Of John Havlicek
> > > Sent: Friday, November 02, 2007 4:26 PM
> > > To: sv-ac@server.eda.org
> > > Subject: [sv-ac] 1678 name resolution and the rewriting algorithm
of
> > > 1549
> > >=3D20
> > > Hi Folks:
> > >=3D20
> > > In 1549, we introduced a local variable declaration
notation=3D3D20
> > > in the abstract syntax.
> > >=3D20
> > > In revising the rewriting algorithm, I deleted the parts about
> > > making local variable names unique.  The rules for overshadowing
> > > in 1549 make this unnecessary in some cases.  Doron asked about
> > > this, but I seemed to convince him that the overshadowing
took=3D3D20
> > > care of the problems.
> > >=3D20
> > > However, 1678 points out that a naive treatment of local variable
> > > identifiers results in name resolution issues when local variables
> are
> > > passed as actual arguments to other instances.  The overshadowing
> > > mechanism of 1549 does not take care of this problem.
> > >=3D20
> > > I do not think that this problem is specific to local variables.
> When
> > > rewriting and substituting actual arguments, we must respect name
> > > resolution.  Simply looking at the identifiers, references,
> > > etc. written in the source code is not good enough.  There can be
> > > incorrect aliasing for all sorts of things other than local
> variables.
> > >=3D20
> > > In order to resolve 1678, I think we need to add some language
> > > (hopefully a small amount) to say that name resolution still needs
> to
> > > be taken care of properly when following the rewriting algorithm.
> > >=3D20
> > > Name resolution is not something that we should be trying to
capture
> > > in Annex F, so I don't think we should make a special point about
> > > making local variable identifiers unique.  That would give the
wrong
> > > impression that other references do not also need to be accounted
> for
> > > with care.
> > >=3D20
> > > I have uploaded to Mantis 1678 and attached below an example of
> > > carrying out the rewriting algorithm while paying attention to
name
> > > resolution.  I don't envision it being added to the LRM.
> > >=3D20
> > > J=3D3D2EH.
> > >=3D20
> > >=3D20
> > > --=3D3D20
> > > This message has been scanned for viruses and
> > > dangerous content by MailScanner, and is
> > > believed to be clean.
> > >
> ---------------------------------------------------------------------
> > > Intel Israel (74) Limited
> > >=3D20
> > > This e-mail and any attachments may contain confidential material
> for
> > > the sole use of the intended recipient(s). Any review or
> distribution
> > > by others is strictly prohibited. If you are not the intended
> > > recipient, please contact the sender and delete all copies.
> >
---------------------------------------------------------------------
> > Intel Israel (74) Limited
> >=20
> > This e-mail and any attachments may contain confidential material
for
> > the sole use of the intended recipient(s). Any review or
distribution
> > by others is strictly prohibited. If you are not the intended
> > recipient, please contact the sender and delete all copies.
> 
> --=20
> This message has been scanned for viruses and
> dangerous content by MailScanner, and is
> believed to be clean.
> ---------------------------------------------------------------------
> Intel Israel (74) Limited
> 
> This e-mail and any attachments may contain confidential material for
> the sole use of the intended recipient(s). Any review or distribution
> by others is strictly prohibited. If you are not the intended
> recipient, please contact the sender and delete all copies.
---------------------------------------------------------------------
Intel Israel (74) Limited

This e-mail and any attachments may contain confidential material for
the sole use of the intended recipient(s). Any review or distribution
by others is strictly prohibited. If you are not the intended
recipient, please contact the sender and delete all copies.

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