Hi Dmitry: I recommend documenting this sort of thing in a bug note along with a note that says that SV-AC needs external feedback in order to address the issue. J.H. > X-eda.org-MailScanner-Watermark: 1205192544.13796@Ux86qxdbd3+Nj8aQeELWqA > X-Authentication-Warning: server.eda.org: majordom set sender to owner-sv-ac@eda.org using -f > X-eda.org-MailScanner-Watermark: 1205192383.13524@m3BYFiEDMSADa3DFlyaw3A > X-ExtLoop1: 1 > X-IronPort-AV: E=Sophos;i="4.25,440,1199692800"; > d="scan'208,217";a="303435174" > X-MimeOLE: Produced By Microsoft Exchange V6.5 > Content-class: urn:content-classes:message > Date: Tue, 4 Mar 2008 01:36:03 +0200 > X-MS-Has-Attach: > X-MS-TNEF-Correlator: > Thread-Topic: [sv-ac] initial vs initial_check > Thread-Index: Ach9CO9iRYp/1a2gRSGT9aT04SARnAAJfaWgAASCOjAAEX9JYA== > From: "Korchemny, Dmitry" <dmitry.korchemny@intel.com> > X-OriginalArrivalTime: 03 Mar 2008 23:36:09.0581 (UTC) FILETIME=[5BE461D0:01C87D87] > X-eda.org-MailScanner: Found to be clean, Found to be clean > X-Spam-Status: No, No > Sender: owner-sv-ac@eda.org > X-eda.org-MailScanner-Information: Please contact the ISP for more information > X-MailScanner-ID: m23NfN4D027622 > X-eda.org-MailScanner-From: owner-sv-ac@server.eda.org > > This is a multi-part message in MIME format. > > ------_=_NextPart_001_01C87D87.59D7E23D > Content-Type: text/plain; charset="us-ascii" > Content-Transfer-Encoding: quoted-printable > > Then we won't be able to fix this unless we get an explicit comment from > the champions or from other committees. > > =20 > > Dmitry > > =20 > > ________________________________ > > From: owner-sv-ac@server.eda.org [mailto:owner-sv-ac@server.eda.org] On > Behalf Of Lisa Piper > Sent: Monday, March 03, 2008 5:15 PM > To: Eduard Cerny; Korchemny, Dmitry; sv-ac@server.eda.org > Subject: RE: [sv-ac] initial vs initial_check > > =20 > > This was fixed in 1698: > > =20 > > If the concurrent assertion statement appears in an always always > procedure, the property is always > > monitored. If the statement appears in an initial initial procedure, > then the monitoring is performed only > > on the first clock tick. > > =20 > > Two inferences are made from the procedural context: the clock from the > event control of an always > > always or initial procedure and the enabling conditions. > > =20 > > =20 > > =20 > > ________________________________ > > From: owner-sv-ac@eda.org [mailto:owner-sv-ac@eda.org] On Behalf Of > Eduard Cerny > Sent: Monday, March 03, 2008 8:06 AM > To: Korchemny, Dmitry; sv-ac@eda.org > Subject: RE: [sv-ac] initial vs initial_check > > =20 > > Hi Dmitry, > > =20 > > I agree that the clock should be inferred from initial block too and > Draft 4 seems to say so, although the text in Draft 4 is confusing: > > =20 > > Two inferences are made from the procedural context: the clock from the > event control of an always=20 > > procedure and the enabling conditions. > > A clock is inferred if the statement is placed in an always or initial > procedure with an event control > > abiding by the following rules: > > - The clock to be inferred must be placed as the first term of the event > control as an edge specifier > > (posedge expression or negedge expression). > > - The variables in expression must not be used anywhere in the always or > initial procedure. > > =20 > > The 1st sentence says only always procedure, but the other ones aloow > inference form either always or initial. > > =20 > > Best regards, > > ed > > =20 > > =20 > > From: owner-sv-ac@eda.org [mailto:owner-sv-ac@eda.org] On Behalf Of > Korchemny, Dmitry > Sent: Monday, March 03, 2008 3:31 AM > To: sv-ac@eda.org > Subject: [sv-ac] initial vs initial_check > > =20 > > Hi all, > > =20 > > I would like to make the following observation, though it is probably > too late. > > =20 > > Currently the clock inference rules for initial procedures are the same > as for always procedures, e.g., in the following case > > =20 > > initial @(posedge clk) assert property (a); > > =20 > > the clock is inferred, > > =20 > > while in > > =20 > > initial @clk assert property (a); > > =20 > > the clock is not inferred. > > =20 > > But essentially these rules were introduced only for consistency > reasons, and it would be more natural to infer all events from the > sensitivity list of the initial procedure, since synthesis > considerations are not valid here. > > =20 > > If we change the inference rules in the initial procedure, initial_check > will be redundant, and this would simplify everything, including the VPI > changes. Though this new definition would break the backward > compatibility, I think it will not have any real negative impact. > > =20 > > What do you think? > > =20 > > Dmitry > > --------------------------------------------------------------------- > 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=20 > dangerous content by MailScanner <http://www.mailscanner.info/> , and is > > believed to be clean.=20 > > > --=20 > This message has been scanned for viruses and=20 > dangerous content by MailScanner <http://www.mailscanner.info/> , and is > > believed to be clean.=20 > --=20 > This message has been scanned for viruses and=20 > dangerous content by MailScanner <http://www.mailscanner.info/> , and is > > believed to be clean.=20 > --------------------------------------------------------------------- > 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. > > --=20 > This message has been scanned for viruses and > dangerous content by MailScanner, and is > believed to be clean. > > > ------_=_NextPart_001_01C87D87.59D7E23D > Content-Type: text/html; charset="us-ascii" > Content-Transfer-Encoding: quoted-printable > > <html xmlns:ns1=3D"http://schemas.microsoft.com/office/2004/12/omml"> > > <head> > <META HTTP-EQUIV=3D"Content-Type" CONTENT=3D"text/html; charset=3Dus-ascii"> > <meta name=3DGenerator content=3D"Microsoft Word 11 (filtered)"> > > <style> > <!--a:link > {mso-style-priority:99;} > span.MSOHYPERLINK > {mso-style-priority:99;} > a:visited > {mso-style-priority:99;} > span.MSOHYPERLINKFOLLOWED > {mso-style-priority:99;} > pre > {mso-style-priority:99;} > span.HTMLPREFORMATTEDCHAR > {mso-style-priority:99;} > > /* Font Definitions */ > @font-face > {font-family:Courier; > panose-1:2 7 4 9 2 2 5 2 4 4;} > @font-face > {font-family:"MS Mincho"; > panose-1:2 2 6 9 4 2 5 8 3 4;} > @font-face > {font-family:Tahoma; > panose-1:2 11 6 4 3 5 4 4 2 4;} > @font-face > {font-family:Consolas; > panose-1:2 11 6 9 2 2 4 3 2 4;} > @font-face > {font-family:TimesNewRoman; > panose-1:0 0 0 0 0 0 0 0 0 0;} > @font-face > {font-family:CourierNew;} > @font-face > {font-family:"\@MS Mincho"; > panose-1:0 0 0 0 0 0 0 0 0 0;} > /* Style Definitions */ > p.MsoNormal, li.MsoNormal, div.MsoNormal > {margin:0in; > margin-bottom:.0001pt; > font-size:11.0pt; > font-family:Courier;} > a:link, span.MsoHyperlink > {color:blue; > text-decoration:underline;} > a:visited, span.MsoHyperlinkFollowed > {color:purple; > text-decoration:underline;} > pre > {margin:0in; > margin-bottom:.0001pt; > font-size:10.0pt; > font-family:"Courier New";} > p.Body, li.Body, div.Body > {margin-top:10.0pt; > margin-right:0in; > margin-bottom:0in; > margin-left:0in; > margin-bottom:.0001pt; > text-align:justify; > text-justify:inter-ideograph; > punctuation-wrap:simple; > text-autospace:none; > font-size:10.0pt; > font-family:TimesNewRoman; > color:black;} > p.ExampleCodeIndented, li.ExampleCodeIndented, div.ExampleCodeIndented > {margin-top:0in; > margin-right:0in; > margin-bottom:0in; > margin-left:20.15pt; > margin-bottom:.0001pt; > punctuation-wrap:simple; > font-size:9.0pt; > font-family:CourierNew; > color:black;} > p.body0, li.body0, div.body0 > {margin-top:10.0pt; > margin-right:0in; > margin-bottom:0in; > margin-left:0in; > margin-bottom:.0001pt; > text-align:justify; > text-justify:inter-ideograph; > punctuation-wrap:simple; > text-autospace:none; > font-size:10.0pt; > font-family:TimesNewRoman; > color:black;} > p.examplecodeindented0, li.examplecodeindented0, div.examplecodeindented0 > {margin-top:0in; > margin-right:0in; > margin-bottom:0in; > margin-left:20.15pt; > margin-bottom:.0001pt; > punctuation-wrap:simple; > font-size:9.0pt; > font-family:CourierNew; > color:black;} > span.htmlpreformattedchar > {font-family:Consolas;} > span.emailstyle19 > {font-family:Arial; > color:windowtext; > font-weight:normal; > font-style:normal; > text-decoration:none none;} > span.EmailStyle24 > {font-family:Arial; > color:navy;} > span.EmailStyle25 > {font-family:Arial; > color:blue; > font-weight:normal; > font-style:normal; > text-decoration:none none;} > span.EmailStyle26 > {font-family:Arial; > color:blue; > font-weight:normal; > font-style:normal; > text-decoration:none none;} > @page Section1 > {size:595.3pt 841.9pt; > margin:1.0in 1.25in 1.0in 1.25in;} > div.Section1 > {page:Section1;} > --> > </style> > > </head> > > <body lang=3DEN-US link=3Dblue vlink=3Dpurple> > > <div class=3DSection1> > > <p class=3DMsoNormal><font size=3D2 color=3Dblue face=3DArial><span style= > =3D'font-size: > 10.0pt;font-family:Arial;color:blue'>Then we won’t be able to fix this > unless we get an explicit comment from the champions or from other committe= > es.</span></font></p> > > <p class=3DMsoNormal><font size=3D2 color=3Dblue face=3DArial><span style= > =3D'font-size: > 10.0pt;font-family:Arial;color:blue'> </span></font></p> > > <p class=3DMsoNormal><font size=3D2 color=3Dblue face=3DArial><span style= > =3D'font-size: > 10.0pt;font-family:Arial;color:blue'>Dmitry</span></font></p> > > <p class=3DMsoNormal><font size=3D2 color=3Dblue face=3DArial><span style= > =3D'font-size: > 10.0pt;font-family:Arial;color:blue'> </span></font></p> > > <div> > > <div class=3DMsoNormal align=3Dcenter style=3D'text-align:center'><font siz= > e=3D3 > face=3D"Times New Roman"><span style=3D'font-size:12.0pt;font-family:"Times= > New Roman"'> > > <hr size=3D2 width=3D"100%" align=3Dcenter tabindex=3D-1> > > </span></font></div> > > <p class=3DMsoNormal><b><font size=3D2 face=3DTahoma><span style=3D'font-si= > ze:10.0pt; > font-family:Tahoma;font-weight:bold'>From:</span></font></b><font size=3D2 > face=3DTahoma><span style=3D'font-size:10.0pt;font-family:Tahoma'> owner-sv= > -ac@server.eda.org > [mailto:owner-sv-ac@server.eda.org] <b><span style=3D'font-weight:bold'>On = > Behalf > Of </span></b>Lisa Piper<br> > <b><span style=3D'font-weight:bold'>Sent:</span></b> Monday, March 03, 2008= > 5:15 > PM<br> > <b><span style=3D'font-weight:bold'>To:</span></b> Eduard Cerny; Korchemny, > Dmitry; sv-ac@server.eda.org<br> > <b><span style=3D'font-weight:bold'>Subject:</span></b> RE: [sv-ac] initial= > vs > initial_check</span></font></p> > > </div> > > <p class=3DMsoNormal><font size=3D2 face=3DCourier><span style=3D'font-size= > :11.0pt'> </span></font></p> > > <p class=3DMsoNormal style=3D'text-autospace:none'><font size=3D2 color=3Db= > lack > face=3D"Times New Roman"><span style=3D'font-size:9.5pt;font-family:"Times = > New Roman"; > color:black'>This was fixed in 1698:</span></font></p> > > <p class=3DMsoNormal style=3D'text-autospace:none'><font size=3D2 color=3Db= > lack > face=3D"Times New Roman"><span style=3D'font-size:9.5pt;font-family:"Times = > New Roman"; > color:black'> </span></font></p> > > <p class=3DMsoNormal style=3D'text-autospace:none'><font size=3D2 color=3Db= > lack > face=3D"Times New Roman"><span style=3D'font-size:9.5pt;font-family:"Times = > New Roman"; > color:black'>If the </span></font><font size=3D2 color=3Dblue face=3D"Times= > New Roman"><span > style=3D'font-size:9.5pt;font-family:"Times New Roman";color:blue'>concurre= > nt > assertion </span></font><font size=3D2 color=3Dblack face=3D"Times New Roma= > n"><span > style=3D'font-size:9.5pt;font-family:"Times New Roman";color:black'>stateme= > nt > appears in an </span></font><b><s><font size=3D1 color=3Dred><span > style=3D'font-size:9.0pt;color:red;font-weight:bold'>always</span></font></= > s></b><b><font > size=3D1 color=3Dred><span style=3D'font-size:9.0pt;color:red;font-weight:b= > old'> </span></font></b><i><font > size=3D2 color=3Dblue face=3D"Times New Roman"><span style=3D'font-size:9.5= > pt; > font-family:"Times New Roman";color:blue;font-style:italic'>always </span><= > /font></i><font > size=3D2 color=3Dblack face=3D"Times New Roman"><span style=3D'font-size:9.= > 5pt; > font-family:"Times New Roman";color:black'>procedure, the property is alway= > s</span></font></p> > > <p class=3DMsoNormal style=3D'text-autospace:none'><font size=3D2 color=3Db= > lack > face=3D"Times New Roman"><span style=3D'font-size:9.5pt;font-family:"Times = > New Roman"; > color:black'>monitored. If the statement appears in an </span></font><b><s>= > <font > size=3D1 color=3Dred><span style=3D'font-size:9.0pt;color:red;font-weight:b= > old'>initial</span></font></s></b><b><font > size=3D1 color=3Dred><span style=3D'font-size:9.0pt;color:red;font-weight:b= > old'> </span></font></b><i><font > size=3D2 color=3Dblue face=3D"Times New Roman"><span style=3D'font-size:9.5= > pt; > font-family:"Times New Roman";color:blue;font-style:italic'>initial </span>= > </font></i><font > size=3D2 color=3Dblack face=3D"Times New Roman"><span style=3D'font-size:9.= > 5pt; > font-family:"Times New Roman";color:black'>procedure, then the monitoring is > performed only</span></font></p> > > <p class=3DMsoNormal style=3D'text-autospace:none'><font size=3D2 color=3Db= > lack > face=3D"Times New Roman"><span style=3D'font-size:9.5pt;font-family:"Times = > New Roman"; > color:black'>on the first clock tick.</span></font></p> > > <p class=3DMsoNormal style=3D'text-autospace:none'><font size=3D2 color=3Db= > lack > face=3D"Times New Roman"><span style=3D'font-size:9.5pt;font-family:"Times = > New Roman"; > color:black'> </span></font></p> > > <p class=3DMsoNormal style=3D'text-autospace:none'><font size=3D2 color=3Db= > lack > face=3D"Times New Roman"><span style=3D'font-size:9.5pt;font-family:"Times = > New Roman"; > color:black'>Two inferences are made from the procedural context: the clock > from the event control of an </span></font><b><s><font size=3D1 color=3Dred= > ><span > style=3D'font-size:9.0pt;color:red;font-weight:bold'>always</span></font></= > s></b></p> > > <p class=3DMsoNormal><i><font size=3D2 color=3Dblue face=3D"Times New Roman= > "><span > style=3D'font-size:9.5pt;font-family:"Times New Roman";color:blue;font-styl= > e: > italic'>always </span></font></i><font size=3D2 color=3Dblue face=3D"Times = > New Roman"><span > style=3D'font-size:9.5pt;font-family:"Times New Roman";color:blue'>or <i><s= > pan > style=3D'font-style:italic'>initial </span></i></span></font><font size=3D2 > color=3Dblack face=3D"Times New Roman"><span style=3D'font-size:9.5pt;font-= > family: > "Times New Roman";color:black'>procedure and the enabling conditions.</span= > ></font></p> > > <p class=3DMsoNormal><font size=3D2 color=3Dblack face=3D"Times New Roman">= > <span > style=3D'font-size:9.5pt;font-family:"Times New Roman";color:black'> <= > /span></font></p> > > <p class=3DMsoNormal><font size=3D3 color=3Dblue face=3DArial><span style= > =3D'font-size: > 12.0pt;font-family:Arial;color:blue'> </span></font></p> > > <p class=3DMsoNormal><font size=3D3 color=3Dblue face=3DArial><span style= > =3D'font-size: > 12.0pt;font-family:Arial;color:blue'> </span></font></p> > > <div> > > <div class=3DMsoNormal align=3Dcenter style=3D'text-align:center'><font siz= > e=3D3 > face=3D"Times New Roman"><span style=3D'font-size:12.0pt;font-family:"Times= > New Roman"'> > > <hr size=3D2 width=3D"100%" align=3Dcenter tabindex=3D-1> > > </span></font></div> > > <p class=3DMsoNormal><b><font size=3D2 face=3DTahoma><span style=3D'font-si= > ze:10.0pt; > font-family:Tahoma;font-weight:bold'>From:</span></font></b><font size=3D2 > face=3DTahoma><span style=3D'font-size:10.0pt;font-family:Tahoma'> > owner-sv-ac@eda.org [mailto:owner-sv-ac@eda.org] <b><span style=3D'font-wei= > ght: > bold'>On Behalf Of </span></b>Eduard Cerny<br> > <b><span style=3D'font-weight:bold'>Sent:</span></b> Monday, March 03, 2008= > 8:06 > AM<br> > <b><span style=3D'font-weight:bold'>To:</span></b> Korchemny, Dmitry; > sv-ac@eda.org<br> > <b><span style=3D'font-weight:bold'>Subject:</span></b> RE: [sv-ac] initial= > vs > initial_check</span></font></p> > > </div> > > <p class=3DMsoNormal><font size=3D2 face=3DCourier><span style=3D'font-size= > :11.0pt'> </span></font></p> > > <p class=3DMsoNormal><font size=3D3 color=3Dnavy face=3DArial><span style= > =3D'font-size: > 12.0pt;font-family:Arial;color:navy'>Hi Dmitry,</span></font></p> > > <p class=3DMsoNormal><font size=3D3 color=3Dnavy face=3DArial><span style= > =3D'font-size: > 12.0pt;font-family:Arial;color:navy'> </span></font></p> > > <p class=3DMsoNormal><font size=3D3 color=3Dnavy face=3DArial><span style= > =3D'font-size: > 12.0pt;font-family:Arial;color:navy'>I agree that the clock should be infer= > red > from initial block too and Draft 4 seems to say so, although the text in Dr= > aft > 4 is confusing:</span></font></p> > > <p class=3DMsoNormal><font size=3D3 color=3Dnavy face=3DArial><span style= > =3D'font-size: > 12.0pt;font-family:Arial;color:navy'> </span></font></p> > > <p class=3DMsoNormal style=3D'text-autospace:none'><font size=3D2 color=3Db= > lack > face=3D"Times New Roman"><span style=3D'font-size:10.0pt;font-family:"Times= > New Roman"; > color:black'>Two inferences are made from the procedural context: the clock > from the event control of an </span></font><b><font size=3D1 color=3Dblack > face=3D"Courier New"><span style=3D'font-size:9.0pt;font-family:"Courier Ne= > w"; > color:black;font-weight:bold'>always </span></font></b></p> > > <p class=3DMsoNormal style=3D'text-autospace:none'><font size=3D2 color=3Db= > lue > face=3D"Times New Roman"><span style=3D'font-size:10.0pt;font-family:"Times= > New Roman"; > color:blue'>procedure </span></font><font size=3D2 color=3Dblack > face=3D"Times New Roman"><span style=3D'font-size:10.0pt;font-family:"Times= > New Roman"; > color:black'>and the enabling conditions.</span></font></p> > > <p class=3DMsoNormal style=3D'text-autospace:none'><font size=3D2 color=3Db= > lack > face=3D"Times New Roman"><span style=3D'font-size:10.0pt;font-family:"Times= > New Roman"; > color:black'>A clock is inferred if the statement is placed in an </span></= > font><b><font > size=3D1 color=3Dblack face=3D"Courier New"><span style=3D'font-size:9.0pt;= > font-family: > "Courier New";color:black;font-weight:bold'>always </span></font></b><font > size=3D2 color=3Dblack face=3D"Times New Roman"><span style=3D'font-size:10= > .0pt; > font-family:"Times New Roman";color:black'>or </span></font><b><font size= > =3D1 > color=3Dblack face=3D"Courier New"><span style=3D'font-size:9.0pt;font-fami= > ly:"Courier New"; > color:black;font-weight:bold'>initial </span></font></b><font size=3D2 > color=3Dblue face=3D"Times New Roman"><span style=3D'font-size:10.0pt;font-= > family: > "Times New Roman";color:blue'>procedure </span></font><font size=3D2 color= > =3Dblack > face=3D"Times New Roman"><span style=3D'font-size:10.0pt;font-family:"Times= > New Roman"; > color:black'>with an event control</span></font></p> > > <p class=3DMsoNormal style=3D'text-autospace:none'><font size=3D2 color=3Db= > lack > face=3D"Times New Roman"><span style=3D'font-size:10.0pt;font-family:"Times= > New Roman"; > color:black'>abiding by the following rules:</span></font></p> > > <p class=3DMsoNormal style=3D'text-autospace:none'><font size=3D2 color=3Db= > lack > face=3D"Times New Roman"><span style=3D'font-size:10.0pt;font-family:"Times= > New Roman"; > color:black'>— The clock to be inferred must be placed as the first t= > erm > of the event control as an edge specifier</span></font></p> > > <p class=3DMsoNormal style=3D'text-autospace:none'><font size=3D2 color=3Db= > lack > face=3D"Times New Roman"><span style=3D'font-size:10.0pt;font-family:"Times= > New Roman"; > color:black'>(</span></font><b><font size=3D1 color=3Dblack face=3D"Courier= > New"><span > style=3D'font-size:9.0pt;font-family:"Courier New";color:black;font-weight:= > bold'>posedge > </span></font></b><i><font size=3D2 color=3Dblack face=3D"Times New Roman">= > <span > style=3D'font-size:10.0pt;font-family:"Times New Roman";color:black;font-st= > yle: > italic'>expression </span></font></i><font size=3D2 color=3Dblack > face=3D"Times New Roman"><span style=3D'font-size:10.0pt;font-family:"Times= > New Roman"; > color:black'>or </span></font><b><font size=3D1 color=3Dblack face=3D"Couri= > er New"><span > style=3D'font-size:9.0pt;font-family:"Courier New";color:black;font-weight:= > bold'>negedge > </span></font></b><i><font size=3D2 color=3Dblack face=3D"Times New Roman">= > <span > style=3D'font-size:10.0pt;font-family:"Times New Roman";color:black;font-st= > yle: > italic'>expression</span></font></i><font size=3D2 color=3Dblack > face=3D"Times New Roman"><span style=3D'font-size:10.0pt;font-family:"Times= > New Roman"; > color:black'>).</span></font></p> > > <p class=3DMsoNormal><font size=3D2 color=3Dblack face=3D"Times New Roman">= > <span > style=3D'font-size:10.0pt;font-family:"Times New Roman";color:black'>—= > ; The > variables in <i><span style=3D'font-style:italic'>expression </span></i>mus= > t not > be used anywhere in the </span></font><b><font size=3D1 color=3Dblack > face=3D"Courier New"><span style=3D'font-size:9.0pt;font-family:"Courier Ne= > w"; > color:black;font-weight:bold'>always </span></font></b><font size=3D2 > color=3Dblack face=3D"Times New Roman"><span style=3D'font-size:10.0pt;font= > -family: > "Times New Roman";color:black'>or </span></font><b><font size=3D1 color=3Db= > lack > face=3D"Courier New"><span style=3D'font-size:9.0pt;font-family:"Courier Ne= > w"; > color:black;font-weight:bold'>initial </span></font></b><font size=3D2 > color=3Dblue face=3D"Times New Roman"><span style=3D'font-size:10.0pt;font-= > family: > "Times New Roman";color:blue'>procedure</span></font><font size=3D2 color= > =3Dblack > face=3D"Times New Roman"><span style=3D'font-size:10.0pt;font-family:"Times= > New Roman"; > color:black'>.</span></font></p> > > <p class=3DMsoNormal><font size=3D3 color=3Dnavy face=3DArial><span style= > =3D'font-size: > 12.0pt;font-family:Arial;color:navy'> </span></font></p> > > <p class=3DMsoNormal><font size=3D3 color=3Dnavy face=3DArial><span style= > =3D'font-size: > 12.0pt;font-family:Arial;color:navy'>The 1<sup>st</sup> sentence says only > always procedure, but the other ones aloow inference form either always or > initial.</span></font></p> > > <p class=3DMsoNormal><font size=3D3 color=3Dnavy face=3DArial><span style= > =3D'font-size: > 12.0pt;font-family:Arial;color:navy'> </span></font></p> > > <p class=3DMsoNormal><font size=3D3 color=3Dnavy face=3DArial><span style= > =3D'font-size: > 12.0pt;font-family:Arial;color:navy'>Best regards,</span></font></p> > > <p class=3DMsoNormal><font size=3D3 color=3Dnavy face=3DArial><span style= > =3D'font-size: > 12.0pt;font-family:Arial;color:navy'>ed</span></font></p> > > <p class=3DMsoNormal><font size=3D3 color=3Dnavy face=3DArial><span style= > =3D'font-size: > 12.0pt;font-family:Arial;color:navy'> </span></font></p> > > <p class=3DMsoNormal><font size=3D3 color=3Dnavy face=3DArial><span style= > =3D'font-size: > 12.0pt;font-family:Arial;color:navy'> </span></font></p> > > <div> > > <div style=3D'border:none;border-top:solid #B5C4DF 1.0pt;padding:3.0pt 0in = > 0in 0in'> > > <p class=3DMsoNormal><b><font size=3D2 face=3DTahoma><span style=3D'font-si= > ze:10.0pt; > font-family:Tahoma;font-weight:bold'>From:</span></font></b><font size=3D2 > face=3DTahoma><span style=3D'font-size:10.0pt;font-family:Tahoma'> > owner-sv-ac@eda.org [mailto:owner-sv-ac@eda.org] <b><span style=3D'font-wei= > ght: > bold'>On Behalf Of </span></b>Korchemny, Dmitry<br> > <b><span style=3D'font-weight:bold'>Sent:</span></b> Monday, March 03, 2008= > 3:31 > AM<br> > <b><span style=3D'font-weight:bold'>To:</span></b> sv-ac@eda.org<br> > <b><span style=3D'font-weight:bold'>Subject:</span></b> [sv-ac] initial vs > initial_check</span></font></p> > > </div> > > </div> > > <p class=3DMsoNormal><font size=3D2 face=3DCourier><span style=3D'font-size= > :11.0pt'> </span></font></p> > > <p class=3DMsoNormal><font size=3D2 face=3DArial><span style=3D'font-size:1= > 0.0pt; > font-family:Arial'>Hi all,</span></font></p> > > <p class=3DMsoNormal><font size=3D2 face=3DArial><span style=3D'font-size:1= > 0.0pt; > font-family:Arial'> </span></font></p> > > <p class=3DMsoNormal><font size=3D2 face=3DArial><span style=3D'font-size:1= > 0.0pt; > font-family:Arial'>I would like to make the following observation, though i= > t is > probably too late.</span></font></p> > > <p class=3DMsoNormal><font size=3D2 face=3DArial><span style=3D'font-size:1= > 0.0pt; > font-family:Arial'> </span></font></p> > > <p class=3DMsoNormal><font size=3D2 face=3DArial><span style=3D'font-size:1= > 0.0pt; > font-family:Arial'>Currently the clock inference rules for initial procedur= > es are > the same as for always procedures, e.g., in the following case</span></font= > ></p> > > <p class=3DMsoNormal><font size=3D2 face=3DArial><span style=3D'font-size:1= > 0.0pt; > font-family:Arial'> </span></font></p> > > <p class=3DMsoNormal><font size=3D2 face=3DArial><span style=3D'font-size:1= > 0.0pt; > font-family:Arial'>initial @(posedge clk) assert property (a);</span></font= > ></p> > > <p class=3DMsoNormal><font size=3D2 face=3DArial><span style=3D'font-size:1= > 0.0pt; > font-family:Arial'> </span></font></p> > > <p class=3DMsoNormal><font size=3D2 face=3DArial><span style=3D'font-size:1= > 0.0pt; > font-family:Arial'>the clock is inferred,</span></font></p> > > <p class=3DMsoNormal><font size=3D2 face=3DArial><span style=3D'font-size:1= > 0.0pt; > font-family:Arial'> </span></font></p> > > <p class=3DMsoNormal><font size=3D2 face=3DArial><span style=3D'font-size:1= > 0.0pt; > font-family:Arial'>while in</span></font></p> > > <p class=3DMsoNormal><font size=3D2 face=3DArial><span style=3D'font-size:1= > 0.0pt; > font-family:Arial'> </span></font></p> > > <p class=3DMsoNormal><font size=3D2 face=3DArial><span style=3D'font-size:1= > 0.0pt; > font-family:Arial'>initial @clk assert property (a);</span></font></p> > > <p class=3DMsoNormal><font size=3D2 face=3DArial><span style=3D'font-size:1= > 0.0pt; > font-family:Arial'> </span></font></p> > > <p class=3DMsoNormal><font size=3D2 face=3DArial><span style=3D'font-size:1= > 0.0pt; > font-family:Arial'>the clock is not inferred.</span></font></p> > > <p class=3DMsoNormal><font size=3D2 face=3DArial><span style=3D'font-size:1= > 0.0pt; > font-family:Arial'> </span></font></p> > > <p class=3DMsoNormal><font size=3D2 face=3DArial><span style=3D'font-size:1= > 0.0pt; > font-family:Arial'>But essentially these rules were introduced only for > consistency reasons, and it would be more natural to infer all events from = > the > sensitivity list of the initial procedure, since synthesis considerations a= > re > not valid here.</span></font></p> > > <p class=3DMsoNormal><font size=3D2 face=3DArial><span style=3D'font-size:1= > 0.0pt; > font-family:Arial'> </span></font></p> > > <p class=3DMsoNormal><font size=3D2 face=3DArial><span style=3D'font-size:1= > 0.0pt; > font-family:Arial'>If we change the inference rules in the initial procedur= > e, > initial_check will be redundant, and this would simplify everything, includ= > ing > the VPI changes. Though this new definition would break the backward > compatibility, I think it will not have any real negative impact.</span></f= > ont></p> > > <p class=3DMsoNormal><font size=3D2 face=3DArial><span style=3D'font-size:1= > 0.0pt; > font-family:Arial'> </span></font></p> > > <p class=3DMsoNormal><font size=3D2 face=3DArial><span style=3D'font-size:1= > 0.0pt; > font-family:Arial'>What do you think?</span></font></p> > > <p class=3DMsoNormal><font size=3D2 face=3DArial><span style=3D'font-size:1= > 0.0pt; > font-family:Arial'> </span></font></p> > > <p class=3DMsoNormal><font size=3D2 face=3DArial><span style=3D'font-size:1= > 0.0pt; > font-family:Arial'>Dmitry</span></font></p> > > <pre><font size=3D2 face=3D"Courier New"><span style=3D'font-size:10.0pt'>-= > --------------------------------------------------------------------</span>= > </font></pre><pre><font > size=3D2 face=3D"Courier New"><span style=3D'font-size:10.0pt'>Intel Israel= > (74) Limited</span></font></pre><pre><font size=3D2 face=3D"Courier New"><= > span > style=3D'font-size:10.0pt'> </span></font></pre><pre><font size=3D2 > face=3D"Courier New"><span style=3D'font-size:10.0pt'>This e-mail and any a= > ttachments may contain confidential material for</span></font></pre><pre><f= > ont > size=3D2 face=3D"Courier New"><span style=3D'font-size:10.0pt'>the sole use= > of the intended recipient(s). Any review or distribution</span></font></pr= > e><pre><font > size=3D2 face=3D"Courier New"><span style=3D'font-size:10.0pt'>by others is= > strictly prohibited. If you are not the intended</span></font></pre><pre><= > font > size=3D2 face=3D"Courier New"><span style=3D'font-size:10.0pt'>recipient, p= > lease contact the sender and delete all copies.</span></font></pre> > > <p class=3DMsoNormal><font size=3D3 face=3D"Times New Roman"><span style=3D= > 'font-size: > 12.0pt;font-family:"Times New Roman"'><br> > -- <br> > This message has been scanned for viruses and <br> > dangerous content by <a href=3D"http://www.mailscanner.info/"><b><span > style=3D'font-weight:bold'>MailScanner</span></b></a>, and is <br> > believed to be clean. </span></font></p> > > </div> > > <pre>--------------------------------------------------------------------- > 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. > </pre></body> > > <br />--=20 > <br />This message has been scanned for viruses and > <br />dangerous content by > <a href=3D"http://www.mailscanner.info/"><b>MailScanner</b></a>, and is > <br />believed to be clean. > <br />--=20 > <br />This message has been scanned for viruses and > <br />dangerous content by > <a href=3D"http://www.mailscanner.info/"><b>MailScanner</b></a>, and is > <br />believed to be clean. > <br />--=20 > <br />This message has been scanned for viruses and > <br />dangerous content by > <a href=3D"http://www.mailscanner.info/"><b>MailScanner</b></a>, and is > <br />believed to be clean. > </html> > > ------_=_NextPart_001_01C87D87.59D7E23D-- > -- This message has been scanned for viruses and dangerous content by MailScanner, and is believed to be clean.Received on Mon Mar 3 18:45:53 2008
This archive was generated by hypermail 2.1.8 : Mon Mar 03 2008 - 18:46:30 PST