Re: [sv-ac] notes from SV-AC meeting 2007-09-25

From: John Havlicek <john.havlicek_at_.....>
Date: Thu Sep 27 2007 - 09:22:30 PDT
HI Erik:

I think that it is not legal to repeat the same label within a given
scope.  Identical labels might be used in distinct scopes (e.g.,
nested ones), but in this case I think you will have an error 
for repetition of the b1 label.

It seems to me that when you remove the "assume property" from 
the foreach loop, there is no declared item left to reference
hierarchically.  So why can't you move the labels out of the 
always and into the generate, so that you get the same hierarchical
names?

Also, you can be more specific about the equivalence by saying that
it is the "assume property" statements that are equivalent, perhaps
identifying the hierarchical names.

J.H.

> X-ExtLoop1: 1
> X-IronPort-AV: E=Sophos;i="4.21,204,1188802800"; 
>    d="scan'208";a="287878748"
> X-MimeOLE: Produced By Microsoft Exchange V6.5
> Content-class: urn:content-classes:message
> Date: Thu, 27 Sep 2007 08:09:55 -0700
> X-MS-Has-Attach: 
> X-MS-TNEF-Correlator: 
> Thread-Topic: [sv-ac] notes from SV-AC meeting 2007-09-25
> Thread-Index: AcgBFlw/jbpUMP4lRb+K5uOxeW2LNgAAdCFw
> From: "Seligman, Erik" <erik.seligman@intel.com>
> Cc: <sv-ac@eda-stds.org>, "Korchemny, Dmitry" <dmitry.korchemny@intel.com>
> X-OriginalArrivalTime: 27 Sep 2007 15:09:56.0800 (UTC) FILETIME=[77094C00:01C80118]
> 
> 
> My main worry was that actually doing this would require the new
> generate block to have the same label as the original for loop, which
> still exists in the rewritten code.  Is it legal to repeat the same
> label in both a for loop and a generate block? =20
> 
> Or are the restrictions we placed strong enough that we can consider the
> entire original for loop to be rewritten as a generate, rather than
> creating a new generate which just contains the assertions?
> 
> 
> -----Original Message-----
> From: John Havlicek [mailto:john.havlicek@freescale.com]=20
> Sent: Thursday, September 27, 2007 7:55 AM
> To: Seligman, Erik
> Cc: Seligman, Erik; sv-ac@eda-stds.org; Korchemny, Dmitry
> Subject: Re: [sv-ac] notes from SV-AC meeting 2007-09-25
> 
> Hi Erik:
> 
> The concern is that there are already rules about how hierarchical names
> are assembled from labeled blocks, loops in generates, etc.
> 
> The phrases "is logically equivalent to" and "the instance names of the
> assumptions are based on the labels appearing in the original code" seem
> to be saying that the rewrite does not produce the correct hierarchical
> names.
> 
> There was discussion in the meeting that it would be good to construct
> the rewrite so that the rules that already exist for labeled blocks,
> loops in generates, etc. will produce the correct hierarchical names.
> 
> My intuition is that this can be done.
> 
> J.H.
> 
> > X-ExtLoop1: 1
> > X-IronPort-AV: E=3DSophos;i=3D"4.21,203,1188802800";=20
> >    d=3D"scan'208";a=3D"154902245"
> > X-MimeOLE: Produced By Microsoft Exchange V6.5
> > Content-class: urn:content-classes:message
> > Date: Thu, 27 Sep 2007 05:47:06 -0700
> > X-MS-Has-Attach:=20
> > X-MS-TNEF-Correlator:=20
> > Thread-Topic: [sv-ac] notes from SV-AC meeting 2007-09-25
> > Thread-Index: Acf/o/4QPLbT+aCdQOqTb00bVP0zygBYD1CQAAAOS4A=3D
> > From: "Seligman, Erik" <erik.seligman@intel.com>
> > Cc: "Korchemny, Dmitry" <dmitry.korchemny@intel.com>
> > X-OriginalArrivalTime: 27 Sep 2007 12:47:08.0027 (UTC)=20
> > FILETIME=3D[83A64CB0:01C80104]
> >=20
> > Oops, forgot to mention which proposal I'm asking about!=3D20 I'm=20
> > referring to the comments on 1995 (asserts in loops).
> >=20
> > -----Original Message-----
> > From: Seligman, Erik=3D20
> > Sent: Thursday, September 27, 2007 5:46 AM
> > To: 'john.havlicek@freescale.com'; sv-ac@server.eda-stds.org
> > Cc: Korchemny, Dmitry
> > Subject: RE: [sv-ac] notes from SV-AC meeting 2007-09-25
> >=20
> > Hi guys-- can someone describe in more detail the issues with the=20
> > example on p.2, mentioned in the notes, or point me to an LRM section?
> > Thanks...
> >=20
> > -----Original Message-----
> > From: owner-sv-ac@server.eda.org [mailto:owner-sv-ac@server.eda.org]=20
> > On Behalf Of John Havlicek
> > Sent: Tuesday, September 25, 2007 11:43 AM
> > To: sv-ac@server.eda-stds.org
> > Subject: [sv-ac] notes from SV-AC meeting 2007-09-25
> >=20
> > Hi Folks:
> >=20
> > My notes from today's meeting are attached.
> >=20
> > Please let me know if corrections are required.
> >=20
> > J.H.
> >=20
> > --=3D20
> > This message has been scanned for viruses and dangerous content by=20
> > 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 Thu Sep 27 09:23:44 2007

This archive was generated by hypermail 2.1.8 : Thu Sep 27 2007 - 09:24:20 PDT