Re: [sv-ac] FW: #805

From: John Havlicek <john.havlicek_at_.....>
Date: Fri Jun 16 2006 - 05:50:12 PDT
Hi Lisa:

> A disabled evaluation of a property does not result in success or
> failure, so no action blocks are executed and no success or failure
> coverage counters are incremented.

I agree with this, although I would delete the word "coverage".

I think that since the proposal considers disabled to be distinct
from successful and failing, then no success or failure counter
of any kind should be incremented for a disabled attempt.

> Also, what happens when a new attempt occurs while disable iff condition
> is already true.   I would think we would count this as another attempt
> that is disabled, so perhaps change it to read:=20
> 
> =20
> 
> cbAssertionDisabledEvaluation
> 
> An assertion attempt reaches a disabled state (e.g. as a result of
> disable iff condition becoming true, or if an attempt is initiated when
> disable iff is true).

I agree with this, but I would rewrite it as 

An assertion attempt reaches a disabled state (e.g. as a result of the
disable iff condition becoming true during the attempt or if the attempt is
initiated when the disable iff condition is true).


Best regards,

John H.

> This is a multi-part message in MIME format.
> 
> ------_=_NextPart_001_01C6898C.07D026DA
> Content-Type: text/plain;
> 	charset="us-ascii"
> Content-Transfer-Encoding: quoted-printable
> 
> Manisha,
> 
> =20
> 
> This may be picky, but you might consider clarifying:
> 
> =20
> 
> A disabled evaluation of a property does not result in success or
> failure, so no action blocks are executed and no success or failure
> coverage counters are incremented.=20
> 
> =20
> 
> Also, what happens when a new attempt occurs while disable iff condition
> is already true.   I would think we would count this as another attempt
> that is disabled, so perhaps change it to read:=20
> 
> =20
> 
> cbAssertionDisabledEvaluation
> 
> An assertion attempt reaches a disabled state (e.g. as a result of
> disable iff condition becoming true, or if an attempt is initiated when
> disable iff is true).
> 
> =20
> 
> Lisa
> 
> =20
> 
> =20
> 
> =20
> 
> ________________________________
> 
> From: owner-sv-ac@verilog.org [mailto:owner-sv-ac@verilog.org] On Behalf
> Of Kulshrestha, Manisha
> Sent: Tuesday, June 06, 2006 11:50 AM
> To: sv-ac@verilog.org
> Subject: [sv-ac] FW: #805
> 
> =20
> 
> 
> 
> 
> 
> -----Original Message-----
> From: Kulshrestha, Manisha
> Sent: Thu 6/1/2006 12:17 PM
> To: 'sv-ac@eda.org'
> Subject: #805
> 
> 
> Hi All,
> 
> I have incorporated most of the feedback in my updated proposal
> (attached here). Please send your feedback. The original proposals are
> still on mantis in case you want to compare. The main change in this
> document is that disabled is not a success and thus very few changes are
> needed in the LRM.
> 
> Thanks.
> Manisha
> 
> 805: disable iff condition should produce vacuous match
> Lisa:           I agree with this too - failure counters do not make
>                         sense for coverage.
>                         failure counters do not make sense for coverage.
> Joseph:         yes
> Doron:          I think that disabled should not count as a success=20
>                         in coverage. we need to change is the report of
> the=20
>                         number of failures in coverage
> Bassam:         yes
> Dmitry:         I don't think the failure should be reported for
> coverage at all.
> Surrendra:      yes
> Ed:                     No success with disable to be reported.
> Dmitry:         I agree with the definition of the vacuous success.
>                         According to our discussion about the property
>                         coverage definition, there is no meaning in
> disabled
>                         coverage success, since it should not count as a
>                         coverage event at all.=20
>                         Therefore the suggestions concerning
>                         Clause 17.13.3, page 288,
>                         Clause 29.4.3, page 482, Clause 29.4.2, page
> 481,
>                         and Annex I are not relevant.
>                         I agree with the proposal concerning  Clause
> 28.4.2.
> Volkan:         yes
> 
> 
> 
> 
> ------_=_NextPart_001_01C6898C.07D026DA
> Content-Type: text/html;
> 	charset="us-ascii"
> Content-Transfer-Encoding: quoted-printable
> 
> <html xmlns:v=3D"urn:schemas-microsoft-com:vml" =
> xmlns:o=3D"urn:schemas-microsoft-com:office:office" =
> xmlns:w=3D"urn:schemas-microsoft-com:office:word" =
> xmlns=3D"http://www.w3.org/TR/REC-html40">
> 
> <head>
> <meta http-equiv=3DContent-Type content=3D"text/html; =
> charset=3Dus-ascii">
> <meta name=3DGenerator content=3D"Microsoft Word 11 (filtered medium)">
> <!--[if !mso]>
> <style>
> v\:* {behavior:url(#default#VML);}
> o\:* {behavior:url(#default#VML);}
> w\:* {behavior:url(#default#VML);}
> .shape {behavior:url(#default#VML);}
> </style>
> <![endif]-->
> <title>FW: #805</title>
> <style>
> <!--
>  /* Font Definitions */
>  @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:"\@MS Mincho";
> 	panose-1:2 2 6 9 4 2 5 8 3 4;}
> @font-face
> 	{font-family:TimesNewRoman;}
>  /* Style Definitions */
>  p.MsoNormal, li.MsoNormal, div.MsoNormal
> 	{margin:0in;
> 	margin-bottom:.0001pt;
> 	font-size:12.0pt;
> 	font-family:"Times New Roman";}
> a:link, span.MsoHyperlink
> 	{color:blue;
> 	text-decoration:underline;}
> a:visited, span.MsoHyperlinkFollowed
> 	{color:purple;
> 	text-decoration:underline;}
> p
> 	{mso-margin-top-alt:auto;
> 	margin-right:0in;
> 	mso-margin-bottom-alt:auto;
> 	margin-left:0in;
> 	font-size:12.0pt;
> 	font-family:"Times New Roman";}
> p.Heading1withNumbers, li.Heading1withNumbers, div.Heading1withNumbers
> 	{margin-top:0in;
> 	margin-right:0in;
> 	margin-bottom:3.0pt;
> 	margin-left:.25in;
> 	text-indent:-.25in;
> 	page-break-after:avoid;
> 	mso-list:l0 level1 lfo1;
> 	font-size:14.0pt;
> 	font-family:Arial;
> 	font-weight:bold;}
> span.EmailStyle19
> 	{mso-style-type:personal-reply;
> 	font-family:Arial;
> 	color:navy;}
> span.2draft
> 	{color:blue;}
> @page Section1
> 	{size:8.5in 11.0in;
> 	margin:1.0in 1.25in 1.0in 1.25in;}
> div.Section1
> 	{page:Section1;}
>  /* List Definitions */
>  @list l0
> 	{mso-list-id:1547140741;
> 	mso-list-type:hybrid;
> 	mso-list-template-ids:-47279520 227593638 67698713 67698715 67698703 =
> 67698713 67698715 67698703 67698713 67698715;}
> @list l0:level1
> 	{mso-level-style-link:"Heading1 with Numbers";
> 	mso-level-tab-stop:.25in;
> 	mso-level-number-position:left;
> 	margin-left:.25in;
> 	text-indent:-.25in;}
> ol
> 	{margin-bottom:0in;}
> ul
> 	{margin-bottom:0in;}
> -->
> </style>
> 
> </head>
> 
> <body lang=3DEN-US link=3Dblue vlink=3Dpurple>
> 
> <div class=3DSection1>
> 
> <p class=3DMsoNormal><font size=3D2 face=3DArial><span =
> style=3D'font-size:10.0pt;
> font-family:Arial'>Manisha,<o:p></o:p></span></font></p>
> 
> <p class=3DMsoNormal><font size=3D2 face=3DArial><span =
> style=3D'font-size:10.0pt;
> font-family:Arial'><o:p>&nbsp;</o:p></span></font></p>
> 
> <p class=3DMsoNormal><font size=3D2 face=3DArial><span =
> style=3D'font-size:10.0pt;
> font-family:Arial'>This may be picky, but you might consider =
> clarifying:<o:p></o:p></span></font></p>
> 
> <p class=3DMsoNormal><font size=3D2 face=3DArial><span =
> style=3D'font-size:10.0pt;
> font-family:Arial'><o:p>&nbsp;</o:p></span></font></p>
> 
> <p class=3DMsoNormal =
> style=3D'margin-left:.5in;text-autospace:none'><font size=3D2
> face=3DTimesNewRoman><span =
> style=3D'font-size:10.0pt;font-family:TimesNewRoman'>A
> disabled evaluation of a property does not result in success or =
> failure<font
> color=3Dblue><span style=3D'color:blue'>, <b><span =
> style=3D'font-weight:bold'>so no
> action blocks are executed and no success or failure coverage counters =
> are
> incremented</span></b>. <o:p></o:p></span></font></span></font></p>
> 
> <p class=3DMsoNormal style=3D'text-autospace:none'><font size=3D2 =
> color=3Dblue
> face=3DTimesNewRoman><span =
> style=3D'font-size:10.0pt;font-family:TimesNewRoman;
> color:blue'><o:p>&nbsp;</o:p></span></font></p>
> 
> <p class=3DMsoNormal style=3D'text-autospace:none'><font size=3D2 =
> face=3DTimesNewRoman><span
> style=3D'font-size:10.0pt;font-family:TimesNewRoman'>Also, what happens =
> when a
> new attempt occurs while disable iff condition is already =
> true.&nbsp;&nbsp; I
> would think we would count this as another attempt that is disabled, so =
> perhaps
> change it to read: <o:p></o:p></span></font></p>
> 
> <p class=3DMsoNormal style=3D'text-autospace:none'><font size=3D2 =
> face=3DTimesNewRoman><span
> style=3D'font-size:10.0pt;font-family:TimesNewRoman'><o:p>&nbsp;</o:p></s=
> pan></font></p>
> 
> <p class=3DMsoNormal =
> style=3D'margin-left:.5in;text-autospace:none'><font size=3D2
> face=3DTimesNewRoman><span =
> style=3D'font-size:10.0pt;font-family:TimesNewRoman'>cbAssertionDisabledE=
> valuation<o:p></o:p></span></font></p>
> 
> <p class=3DMsoNormal =
> style=3D'margin-left:.5in;text-autospace:none'><font size=3D2
> face=3DTimesNewRoman><span =
> style=3D'font-size:10.0pt;font-family:TimesNewRoman'>An
> assertion attempt reaches a disabled state (e.g. as a result of disable =
> iff
> condition becoming true, <b><font color=3Dblue><span =
> style=3D'color:blue;
> font-weight:bold'>or if an attempt is initiated when disable iff is =
> true</span></font></b>).<o:p></o:p></span></font></p>
> 
> <p class=3DMsoNormal =
> style=3D'margin-left:.5in;text-autospace:none'><font size=3D2
> face=3DTimesNewRoman><span =
> style=3D'font-size:10.0pt;font-family:TimesNewRoman'><o:p>&nbsp;</o:p></s=
> pan></font></p>
> 
> <p class=3DMsoNormal style=3D'text-autospace:none'><font size=3D2 =
> face=3DTimesNewRoman><span
> style=3D'font-size:10.0pt;font-family:TimesNewRoman'>Lisa<o:p></o:p></spa=
> n></font></p>
> 
> <p class=3DMsoNormal style=3D'text-autospace:none'><font size=3D2 =
> color=3Dblue
> face=3DTimesNewRoman><span =
> style=3D'font-size:10.0pt;font-family:TimesNewRoman;
> color:blue'>&nbsp;</span></font><font size=3D2 =
> face=3DTimesNewRoman><span
> style=3D'font-size:10.0pt;font-family:TimesNewRoman'><o:p></o:p></span></=
> font></p>
> 
> <p class=3DMsoNormal><font size=3D2 color=3Dnavy face=3DArial><span =
> style=3D'font-size:
> 10.0pt;font-family:Arial;color:navy'><o:p>&nbsp;</o:p></span></font></p>
> 
> <p class=3DMsoNormal><font size=3D2 color=3Dnavy face=3DArial><span =
> style=3D'font-size:
> 10.0pt;font-family:Arial;color:navy'><o:p>&nbsp;</o:p></span></font></p>
> 
> <div>
> 
> <div class=3DMsoNormal align=3Dcenter =
> style=3D'margin-left:.5in;text-align:center'><font
> size=3D3 face=3D"Times New Roman"><span style=3D'font-size:12.0pt'>
> 
> <hr size=3D2 width=3D"100%" align=3Dcenter tabindex=3D-1>
> 
> </span></font></div>
> 
> <p class=3DMsoNormal style=3D'margin-left:.5in'><b><font size=3D2 =
> face=3DTahoma><span
> style=3D'font-size:10.0pt;font-family:Tahoma;font-weight:bold'>From:</spa=
> n></font></b><font
> size=3D2 face=3DTahoma><span =
> style=3D'font-size:10.0pt;font-family:Tahoma'>
> owner-sv-ac@verilog.org [mailto:owner-sv-ac@verilog.org] <b><span
> style=3D'font-weight:bold'>On Behalf Of </span></b>Kulshrestha, =
> Manisha<br>
> <b><span style=3D'font-weight:bold'>Sent:</span></b> Tuesday, June 06, =
> 2006 11:50
> AM<br>
> <b><span style=3D'font-weight:bold'>To:</span></b> sv-ac@verilog.org<br>
> <b><span style=3D'font-weight:bold'>Subject:</span></b> [sv-ac] FW: =
> #805</span></font><o:p></o:p></p>
> 
> </div>
> 
> <p class=3DMsoNormal style=3D'margin-left:.5in'><font size=3D3 =
> face=3D"Times New Roman"><span
> style=3D'font-size:12.0pt'><o:p>&nbsp;</o:p></span></font></p>
> 
> <p class=3DMsoNormal =
> style=3D'mso-margin-top-alt:0in;margin-right:0in;margin-bottom:
> 12.0pt;margin-left:.5in'><font size=3D3 face=3D"Times New Roman"><span
> style=3D'font-size:12.0pt'><br>
> <br>
> <o:p></o:p></span></font></p>
> 
> <p =
> style=3D'mso-margin-top-alt:5.0pt;margin-right:0in;margin-bottom:12.0pt;
> margin-left:.5in'><font size=3D2 face=3D"Times New Roman"><span =
> style=3D'font-size:
> 10.0pt'>-----Original Message-----<br>
> From: Kulshrestha, Manisha<br>
> Sent: Thu 6/1/2006 12:17 PM<br>
> To: 'sv-ac@eda.org'<br>
> Subject: #805<br>
> <br>
> <br>
> Hi All,<br>
> <br>
> I have incorporated most of the feedback in my updated proposal =
> (attached
> here). Please send your feedback. The original proposals are still on =
> mantis in
> case you want to compare. The main change in this document is that =
> disabled is
> not a success and thus very few changes are needed in the LRM.<br>
> <br>
> Thanks.<br>
> Manisha<br>
> <br>
> 805: disable iff condition should produce vacuous match<br>
> Lisa:&nbsp;&nbsp; &nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp; I agree =
> with this
> too - failure counters do not make<br>
> &nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;
> &nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;
> &nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp; sense for coverage.<br>
> &nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;
> &nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;
> &nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp; failure counters do not make =
> sense
> for coverage.<br>
> Joseph: &nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp; yes<br>
> Doron:&nbsp; &nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp; I think that =
> disabled
> should not count as a success&nbsp;<br>
> &nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;
> &nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;
> &nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp; in coverage. we need to =
> change is
> the report of the&nbsp;<br>
> &nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;
> &nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;
> &nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp; number of failures in =
> coverage<br>
> Bassam: &nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp; yes<br>
> Dmitry: &nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp; I don't think the =
> failure
> should be reported for coverage at all.<br>
> Surrendra:&nbsp;&nbsp;&nbsp;&nbsp;&nbsp; yes<br>
> Ed:&nbsp;&nbsp;&nbsp;&nbsp; &nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;
> &nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp; No success with disable to be
> reported.<br>
> Dmitry: &nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp; I agree with the =
> definition
> of the vacuous success.<br>
> &nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;
> &nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;
> &nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp; According to our discussion =
> about
> the property<br>
> &nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;
> &nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;
> &nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp; coverage definition, there is =
> no
> meaning in disabled<br>
> &nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;
> &nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;
> &nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp; coverage success, since it =
> should
> not count as a<br>
> &nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;
> &nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;
> &nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp; coverage event at =
> all.&nbsp;<br>
> &nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;
> &nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;
> &nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp; Therefore the suggestions =
> concerning<br>
> &nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;
> &nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;
> &nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp; Clause 17.13.3, page 288,<br>
> &nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;
> &nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;
> &nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp; Clause 29.4.3, page 482, =
> Clause
> 29.4.2, page 481,<br>
> &nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;
> &nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;
> &nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp; and Annex I are not =
> relevant.<br>
> &nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;
> &nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;
> &nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp; I agree with the proposal
> concerning&nbsp; Clause 28.4.2.<br>
> Volkan: &nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp; yes<br>
> <br>
> </span></font><o:p></o:p></p>
> 
> </div>
> 
> </body>
> 
> </html>
> 
> ------_=_NextPart_001_01C6898C.07D026DA--
Received on Fri Jun 16 05:50:38 2006

This archive was generated by hypermail 2.1.8 : Fri Jun 16 2006 - 05:50:49 PDT