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

I think one or more mails from Erik did not get through the reflector.

Shalom
 

> -----Original Message-----
> From: owner-sv-ac@server.eda.org 
> [mailto:owner-sv-ac@server.eda.org] On Behalf Of John Havlicek
> Sent: Thursday, September 27, 2007 7:15 PM
> To: Seligman, Erik
> Cc: john.havlicek@freescale.com; sv-ac@server.eda-stds.org; 
> Korchemny, Dmitry
> Subject: Re: [sv-ac] notes from SV-AC meeting 2007-09-25
> 
> Hi Erik:
> 
> Yes, this is what I had in mind.  I haven't checked it 
> carefully, but it looks o.k. in general.
> 
> To check this carefully, you should review the rules for 
> hierarchical names when labels are not specified on all 
> scopes to see what the standard says.
> 
> Manisha should also say whether this addresses her concern.
> 
> J.H.
> 
> > X-ExtLoop1: 1
> > X-IronPort-AV: E=Sophos;i="4.21,204,1188802800"; 
> >    d="scan'208";a="234251706"
> > X-MimeOLE: Produced By Microsoft Exchange V6.5
> > Content-class: urn:content-classes:message
> > Date: Thu, 27 Sep 2007 10:00:41 -0700
> > X-MS-Has-Attach: 
> > X-MS-TNEF-Correlator: 
> > Thread-Topic: [sv-ac] notes from SV-AC meeting 2007-09-25
> > Thread-Index: AcgBIqZNmgpSkc2RT+Kkhb72RkzbFwAAhqDQAADC0vA=
> > From: "Seligman, Erik" <erik.seligman@intel.com>
> > Cc: <sv-ac@eda-stds.org>, "Korchemny, Dmitry" 
> > <dmitry.korchemny@intel.com>
> > X-OriginalArrivalTime: 27 Sep 2007 17:00:42.0311 (UTC) 
> > FILETIME=[F011CD70:01C80127]
> > 
> > Does this change to the example correspond to what you had in mind?:
> > 
> > For example:
> > 
> > integer my_ints[2] =3D {123, 456};=20
> > always @(posedge clk) begin=20
> >     foreach (my_ints[i]) begin : b1
> >         foo[i] <=3D somefunction(my_ints[i]);
> > 	  a1: assume property (foo[i] !=3D `BAD_VAL);
> >     end
> > end
> > 
> > The assumptions b1[0].a1 and b1[1].a1 in this example are logically 
> > equivalent to the assumptions in the example below:
> > 
> > integer my_ints[2] =3D {123, 456};=20
> > always @(posedge clk) begin=20
> >     foreach (my_ints[i]) begin=20
> >         foo[i] <=3D somefunction(my_ints[i]);
> >     end
> > end
> > 
> > genvar i1;
> > generate for (i1=3D0; i1<=3D1; i1=3Di1+1) begin : b1=20
> >   a1: assume property (@(posedge clk) (foo[i1] !=3D `BAD_VAL));
> >     end
> > Endgenerate
> > 
> > 
> > 
> > -----Original Message-----
> > From: Seligman, Erik=20
> > Sent: Thursday, September 27, 2007 9:41 AM
> > To: 'john.havlicek@freescale.com'
> > Cc: sv-ac@eda-stds.org; Korchemny, Dmitry
> > Subject: RE: [sv-ac] notes from SV-AC meeting 2007-09-25
> > 
> > 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]
> > 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
> > > >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
> > > >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
> > > >[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.
> 
---------------------------------------------------------------------
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.