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

Hi Erik:

My opinion is that it is o.k. to do this in an example.  If you
say "For example", then people should understand this is an
illustration, not a rewriting algorithm.  In fact, even though
I used the work "rewrite" in my mail, I would not use it in 
the proposal.

The current draft has already been criticized on the basis that 
the hierarchical names do not correspond.  

A different solution is to have distinct hierarchical names and 
say which hierarchically identified assertion in the foreach 
behaves equivalently to which hierarchically identified assertion
in the generate.  I don't think this is as good, but you should 
decide how you want to proceed.

J.H.



> X-ExtLoop1: 1
> X-IronPort-AV: E=Sophos;i="4.21,204,1188802800"; 
>    d="scan'208";a="326815677"
> X-MimeOLE: Produced By Microsoft Exchange V6.5
> Content-class: urn:content-classes:message
> Date: Thu, 27 Sep 2007 09:41:22 -0700
> X-MS-Has-Attach: 
> X-MS-TNEF-Correlator: 
> Thread-Topic: [sv-ac] notes from SV-AC meeting 2007-09-25
> Thread-Index: AcgBIqZNmgpSkc2RT+Kkhb72RkzbFwAAhqDQ
> From: "Seligman, Erik" <erik.seligman@intel.com>
> Cc: <sv-ac@eda-stds.org>, "Korchemny, Dmitry" <dmitry.korchemny@intel.com>
> X-OriginalArrivalTime: 27 Sep 2007 16:41:23.0185 (UTC) FILETIME=[3D2D3610:01C80125]
> 
> Moving the labels out to the generate works for that example, but it's
> not a general solution, as there will be other unrelated statements in
> the loop in typical cases.  Is this OK? =20
> 
> I'm worried people will see that in the example, and complain that it
> doesn't work in general, so the proposal is broken.  This is why I
> phrased it the way I did in the last draft.=20
> 
> But if you think it's OK to do this to clarify the example, while also
> commenting that moving the label doesn't work in general, I can rewrite
> it like that.
> 
> -----Original Message-----
> From: John Havlicek [mailto:john.havlicek@freescale.com]=20
> Sent: Thursday, September 27, 2007 9:23 AM
> To: Seligman, Erik
> Cc: john.havlicek@freescale.com; sv-ac@eda-stds.org; Korchemny, Dmitry
> Subject: Re: [sv-ac] notes from SV-AC meeting 2007-09-25
> 
> 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=3DSophos;i=3D"4.21,204,1188802800";=20
> >    d=3D"scan'208";a=3D"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:=20
> > X-MS-TNEF-Correlator:=20
> > 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"=20
> > <dmitry.korchemny@intel.com>
> > X-OriginalArrivalTime: 27 Sep 2007 15:09:56.0800 (UTC)=20
> > FILETIME=3D[77094C00:01C80118]
> >=20
> >=20
> > My main worry was that actually doing this would require the new=20
> > generate block to have the same label as the original for loop, which=20
> > still exists in the rewritten code.  Is it legal to repeat the same=20
> > label in both a for loop and a generate block? =3D20
> >=20
> > Or are the restrictions we placed strong enough that we can consider=20
> > the entire original for loop to be rewritten as a generate, rather=20
> > than creating a new generate which just contains the assertions?
> >=20
> >=20
> > -----Original Message-----
> > From: John Havlicek [mailto:john.havlicek@freescale.com]=3D20
> > 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
> >=20
> > Hi Erik:
> >=20
> > The concern is that there are already rules about how hierarchical=20
> > names are assembled from labeled blocks, loops in generates, etc.
> >=20
> > The phrases "is logically equivalent to" and "the instance names of=20
> > the assumptions are based on the labels appearing in the original=20
> > code" seem to be saying that the rewrite does not produce the correct=20
> > hierarchical names.
> >=20
> > 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,=20
> > loops in generates, etc. will produce the correct hierarchical names.
> >=20
> > My intuition is that this can be done.
> >=20
> > J.H.
> >=20
> > > X-ExtLoop1: 1
> > > X-IronPort-AV: E=3D3DSophos;i=3D3D"4.21,203,1188802800";=3D20
> > >    d=3D3D"scan'208";a=3D3D"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:=3D20 =20
> > >X-MS-TNEF-Correlator:=3D20
> > > Thread-Topic: [sv-ac] notes from SV-AC meeting 2007-09-25
> > > Thread-Index: Acf/o/4QPLbT+aCdQOqTb00bVP0zygBYD1CQAAAOS4A=3D3D
> > > From: "Seligman, Erik" <erik.seligman@intel.com>
> > > Cc: "Korchemny, Dmitry" <dmitry.korchemny@intel.com>
> > > X-OriginalArrivalTime: 27 Sep 2007 12:47:08.0027 (UTC)=3D20 =20
> > >FILETIME=3D3D[83A64CB0:01C80104] =3D20  Oops, forgot to mention which =
> 
> > >proposal I'm asking about!=3D3D20 I'm=3D20  referring to the comments =
> on=20
> > >1995 (asserts in loops).
> > >=3D20
> > > -----Original Message-----
> > > From: Seligman, Erik=3D3D20
> > > 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 =3D20  Hi=20
> > >guys-- can someone describe in more detail the issues with the=3D20 =20
> > >example on p.2, mentioned in the notes, or point me to an LRM
> section?
> > > Thanks...
> > >=3D20
> > > -----Original Message-----
> > > From: owner-sv-ac@server.eda.org=20
> > >[mailto:owner-sv-ac@server.eda.org]=3D20
> > > 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 =3D20  Hi =
> Folks:
> > >=3D20
> > > My notes from today's meeting are attached.
> > >=3D20
> > > Please let me know if corrections are required.
> > >=3D20
> > > J.H.
> > >=3D20
> > > --=3D3D20
> > > This message has been scanned for viruses and dangerous content=20
> > >by=3D20  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.