Hi Ed: Maybe we shouldn't even be using the word "match" here. I think "match" is a sequence concept, not a concept applicable to general properties. The way I have thought about this is that for "cover property" the coverage count should increment by at most one per evaluation attempt. If the property evaluation attempt succeeds then the coverage count is incremented by one, no matter how many sub-evaluations actually succeed. Otherwise, the coverage count is not incremented for that evaluation attempt. This way of viewing things corresponds nicely to the satisfaction relation at the property level. It still leaves open the question of which attached subroutines execute, but this is a more general question that is the subject of 0921. I don't think "first match" of an attempt of a property evaluation has yet been defined. I think that such a concept can be defined using ideas from the existing material on 0921. J.H. > X-Authentication-Warning: server.eda-stds.org: majordom set sender to owner-sv-ac@eda.org using -f > X-MIMEOLE: Produced By Microsoft Exchange V6.5 > Content-class: urn:content-classes:message > Date: Wed, 11 Jul 2007 11:05:37 -0700 > Thread-Topic: [sv-ac] updated cover sequence proposal > Thread-Index: AcfDvetgHwnzAaV0Q9ixHKc1EnDQLwAExp6wAASaOQAAAJ824A== > From: "Eduard Cerny" <Eduard.Cerny@synopsys.com> > X-OriginalArrivalTime: 11 Jul 2007 18:05:39.0780 (UTC) FILETIME=[16EBE040:01C7C3E6] > 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-eda.org-MailScanner-From: owner-sv-ac@server.eda.org > > This is a multi-part message in MIME format. > > ------_=_NextPart_001_01C7C3E6.1619019E > Content-Type: text/plain; > charset="us-ascii" > Content-Transfer-Encoding: quoted-printable > > I think that first match is better than one match. I'd also like an > answer to my question about mutliple first matches. > ed > =20 > > > ________________________________ > > From: owner-sv-ac@eda.org [mailto:owner-sv-ac@eda.org] On Behalf > Of Lisa Piper > Sent: Wednesday, July 11, 2007 1:53 PM > To: Bassam Tabbara; sv-ac@eda-stds.org > Subject: RE: [sv-ac] updated cover sequence proposal > =09 > =09 > > =09=20 > > =09=20 > > =09 > ________________________________ > > > From: Bassam Tabbara [mailto:Bassam.Tabbara@synopsys.com]=20 > Sent: Wednesday, July 11, 2007 11:45 AM > To: Lisa Piper; sv-ac@eda-stds.org > Subject: RE: [sv-ac] updated cover sequence proposal > > =09=20 > > Hi Lisa, > > =09=20 > > 3 comments -- independent issues: > > =09=20 > > 1) Do we really need to create a backward incompatibility > ? We can leave cover property (sequence_expr) in and recommend not using > or at least *deprecate* instead of striking out. It's not an erratum we > are fixing, rather can be thought of as better/clearer syntax + > enhancement to add disable iff -- intended to help users not make things > harder short term. > > =09=20 > > [Lisa Piper >>>] you can still do this since a sequence_expr is > an property_expr. But it will provide the one match per attempt.=20 > > =09=20 > > 2) The wording of "cover property" being a "one match" is > too strong. There are cases (implication) when more than one match > results, in fact we rely on this (per previous discussion) to define the > semantics of "cover sequence". > > =09=20 > > [Lisa Piper >>>] any suggestions? > > =09=20 > > 3) Do we need to file a separate proposal for semantics > update (the annex) ? Or are we adding to same ? > > =09=20 > > [Lisa Piper >>>] I don't think a separate proposal is good. I > will add it to this. I assume you are talking about Annex A?=20=20 > > =09=20 > > Thx. > > -Bassam. > > =09=20 > > =09=20 > > =09 > ________________________________ > > > From: owner-sv-ac@eda.org [mailto:owner-sv-ac@eda.org] On Behalf > Of Lisa Piper > Sent: Wednesday, July 11, 2007 6:18 AM > To: sv-ac@eda-stds.org > Subject: [sv-ac] updated cover sequence proposal > > I have uploaded a new version of 1768 - cover sequence. It is > attached for convenience.=20 > > Lisa <<1768_cover_sequence_3.pdf>>=20 > > =09 > --=20 > This message has been scanned for viruses and=20 > dangerous content by <http://www.mailscanner.info/> MailScanner, > and is=20 > 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=20 > believed to be clean.=20 > > > --=20 > This message has been scanned for viruses and > dangerous content by MailScanner, and is > believed to be clean. > > > ------_=_NextPart_001_01C7C3E6.1619019E > Content-Type: text/html; > charset="us-ascii" > Content-Transfer-Encoding: quoted-printable > > <!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.0 Transitional//EN"> > <HTML xmlns=3D"http://www.w3.org/TR/REC-html40" xmlns:v =3D=20 > "urn:schemas-microsoft-com:vml" xmlns:o =3D=20 > "urn:schemas-microsoft-com:office:office" xmlns:w =3D=20 > "urn:schemas-microsoft-com:office:word"><HEAD><TITLE>updated cover sequence= > proposal</TITLE> > <META http-equiv=3DContent-Type content=3D"text/html; charset=3Dus-ascii"> > <META content=3D"MSHTML 6.00.5730.11" name=3DGENERATOR><!--[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]--> > <STYLE>@font-face { > font-family: Tahoma; > } > @page Section1 {size: 8.5in 11.0in; margin: 1.0in 1.25in 1.0in 1.25in; } > P.MsoNormal { > FONT-SIZE: 12pt; MARGIN: 0in 0in 0pt; FONT-FAMILY: "Times New Roman" > } > LI.MsoNormal { > FONT-SIZE: 12pt; MARGIN: 0in 0in 0pt; FONT-FAMILY: "Times New Roman" > } > DIV.MsoNormal { > FONT-SIZE: 12pt; MARGIN: 0in 0in 0pt; FONT-FAMILY: "Times New Roman" > } > A:link { > COLOR: blue; TEXT-DECORATION: underline > } > SPAN.MsoHyperlink { > COLOR: blue; TEXT-DECORATION: underline > } > A:visited { > COLOR: blue; TEXT-DECORATION: underline > } > SPAN.MsoHyperlinkFollowed { > COLOR: blue; TEXT-DECORATION: underline > } > P { > FONT-SIZE: 12pt; MARGIN-LEFT: 0in; MARGIN-RIGHT: 0in; FONT-FAMILY: "Times = > New Roman"; mso-margin-top-alt: auto; mso-margin-bottom-alt: auto > } > SPAN.EmailStyle19 { > FONT-WEIGHT: normal; COLOR: blue; FONT-STYLE: normal; FONT-FAMILY: Arial; = > TEXT-DECORATION: none; mso-style-type: personal-reply > } > DIV.Section1 { > page: Section1 > } > OL { > MARGIN-BOTTOM: 0in > } > UL { > MARGIN-BOTTOM: 0in > } > </STYLE> > </HEAD> > <BODY lang=3DEN-US vLink=3Dblue link=3Dblue> > <DIV><SPAN class=3D134270418-11072007><FONT face=3D"Courier New" color=3D#0= > 000ff=20 > size=3D4>I think that first match is better than one match. I'd also like a= > n=20 > answer to my question about mutliple first matches.</FONT></SPAN></DIV> > <DIV><SPAN class=3D134270418-11072007><FONT face=3D"Courier New" color=3D#0= > 000ff=20 > size=3D4>ed</FONT></SPAN></DIV> > <DIV><SPAN class=3D134270418-11072007></SPAN> </DIV><BR> > <BLOCKQUOTE=20 > style=3D"PADDING-LEFT: 5px; MARGIN-LEFT: 5px; BORDER-LEFT: #0000ff 2px soli= > d; MARGIN-RIGHT: 0px"> > <DIV class=3DOutlookMessageHeader lang=3Den-us dir=3Dltr align=3Dleft> > <HR tabIndex=3D-1> > <FONT face=3DTahoma size=3D2><B>From:</B> owner-sv-ac@eda.org=20 > [mailto:owner-sv-ac@eda.org] <B>On Behalf Of </B>Lisa Piper<BR><B>Sent:</= > B>=20 > Wednesday, July 11, 2007 1:53 PM<BR><B>To:</B> Bassam Tabbara;=20 > sv-ac@eda-stds.org<BR><B>Subject:</B> RE: [sv-ac] updated cover sequence= > =20 > proposal<BR></FONT><BR></DIV> > <DIV></DIV> > <DIV class=3DSection1> > <P class=3DMsoNormal><FONT face=3DArial color=3Dblue size=3D3><SPAN=20 > style=3D"FONT-SIZE: 12pt; COLOR: blue; FONT-FAMILY: Arial"><o:p> </o= > :p></SPAN></FONT></P> > <P class=3DMsoNormal><FONT face=3DArial color=3Dblue size=3D3><SPAN=20 > style=3D"FONT-SIZE: 12pt; COLOR: blue; FONT-FAMILY: Arial"><o:p> </o= > :p></SPAN></FONT></P> > <DIV> > <DIV class=3DMsoNormal style=3D"TEXT-ALIGN: center" align=3Dcenter><FONT= > =20 > face=3D"Times New Roman" size=3D3><SPAN style=3D"FONT-SIZE: 12pt"> > <HR tabIndex=3D-1 align=3Dcenter width=3D"100%" SIZE=3D2> > </SPAN></FONT></DIV> > <P class=3DMsoNormal><B><FONT face=3DTahoma size=3D2><SPAN=20 > style=3D"FONT-WEIGHT: bold; FONT-SIZE: 10pt; FONT-FAMILY: Tahoma">From:</= > SPAN></FONT></B><FONT=20 > face=3DTahoma size=3D2><SPAN style=3D"FONT-SIZE: 10pt; FONT-FAMILY: Tahom= > a"> Bassam=20 > Tabbara [mailto:Bassam.Tabbara@synopsys.com] <BR><B><SPAN=20 > style=3D"FONT-WEIGHT: bold">Sent:</SPAN></B> Wednesday, July 11, 2007 11:= > 45=20 > AM<BR><B><SPAN style=3D"FONT-WEIGHT: bold">To:</SPAN></B> Lisa Piper;=20 > sv-ac@eda-stds.org<BR><B><SPAN style=3D"FONT-WEIGHT: bold">Subject:</SPAN= > ></B>=20 > RE: [sv-ac] updated cover sequence proposal</SPAN></FONT><o:p></o:p></P><= > /DIV> > <P class=3DMsoNormal><FONT face=3D"Times New Roman" size=3D3><SPAN=20 > style=3D"FONT-SIZE: 12pt"><o:p> </o:p></SPAN></FONT></P> > <DIV> > <P class=3DMsoNormal><FONT face=3DArial color=3Dblue size=3D2><SPAN=20 > style=3D"FONT-SIZE: 10pt; COLOR: blue; FONT-FAMILY: Arial">Hi=20 > Lisa,</SPAN></FONT><o:p></o:p></P></DIV> > <DIV> > <P class=3DMsoNormal><FONT face=3D"Times New Roman" size=3D3><SPAN=20 > style=3D"FONT-SIZE: 12pt"> <o:p></o:p></SPAN></FONT></P></DIV> > <DIV> > <P class=3DMsoNormal><FONT face=3DArial color=3Dblue size=3D2><SPAN=20 > style=3D"FONT-SIZE: 10pt; COLOR: blue; FONT-FAMILY: Arial">3 comment= > s --=20 > independent issues:</SPAN></FONT><o:p></o:p></P></DIV> > <DIV> > <P class=3DMsoNormal><FONT face=3D"Times New Roman" size=3D3><SPAN=20 > style=3D"FONT-SIZE: 12pt"> <o:p></o:p></SPAN></FONT></P></DIV> > <DIV> > <P class=3DMsoNormal=20 > style=3D"MARGIN-LEFT: 0.5in; TEXT-INDENT: -0.25in; mso-list: l0 level1 lf= > o1"><![if !supportLists]><FONT=20 > face=3DArial color=3Dblue size=3D2><SPAN=20 > style=3D"FONT-SIZE: 10pt; COLOR: blue; FONT-FAMILY: Arial"><SPAN=20 > style=3D"mso-list: Ignore">1)<FONT face=3D"Times New Roman" size=3D1><SPA= > N=20 > style=3D"FONT: 7pt 'Times New Roman'">  = > ;=20 > </SPAN></FONT></SPAN></SPAN></FONT><![endif]><FONT face=3DArial color=3Db= > lue=20 > size=3D2><SPAN style=3D"FONT-SIZE: 10pt; COLOR: blue; FONT-FAMILY: Arial"= > >Do we=20 > really need to create a backward incompatibility ? We can leave <EM><I><F= > ONT=20 > face=3DArial><SPAN style=3D"FONT-FAMILY: Arial">cover property=20 > (sequence_expr)</SPAN></FONT></I></EM> in and recommend not using or at l= > east=20 > *deprecate* instead of striking out. It's not an erratum we are=20 > fixing, rather can be thought of as better/clearer syntax + enhancem= > ent=20 > to add disable iff -- intended to help users not make things harder short= > =20 > term.</SPAN></FONT><FONT face=3DArial size=3D2><SPAN=20 > style=3D"FONT-SIZE: 10pt; FONT-FAMILY: Arial"><o:p></o:p></SPAN></FONT></= > P> > <P class=3DMsoNormal style=3D"MARGIN-LEFT: 0.25in"><FONT face=3DArial col= > or=3Dblue=20 > size=3D2><SPAN=20 > style=3D"FONT-SIZE: 10pt; COLOR: blue; FONT-FAMILY: Arial"><o:p> </o= > :p></SPAN></FONT></P> > <P class=3DMsoNormal><FONT face=3DArial color=3Dred size=3D3><SPAN=20 > style=3D"FONT-SIZE: 12pt; COLOR: red; FONT-FAMILY: Arial">[Lisa Piper=20 > >>>] you can still do this since a sequence_expr is an=20 > property_expr. But it will provide the one match per attempt.=20 > <o:p></o:p></SPAN></FONT></P></DIV> > <DIV> > <P class=3DMsoNormal><FONT face=3D"Times New Roman" size=3D3><SPAN=20 > style=3D"FONT-SIZE: 12pt"> <o:p></o:p></SPAN></FONT></P></DIV> > <DIV> > <P class=3DMsoNormal=20 > style=3D"MARGIN-LEFT: 0.5in; TEXT-INDENT: -0.25in; mso-list: l0 level1 lf= > o1"><![if !supportLists]><FONT=20 > face=3DArial color=3Dblue size=3D2><SPAN=20 > style=3D"FONT-SIZE: 10pt; COLOR: blue; FONT-FAMILY: Arial"><SPAN=20 > style=3D"mso-list: Ignore">2)<FONT face=3D"Times New Roman" size=3D1><SPA= > N=20 > style=3D"FONT: 7pt 'Times New Roman'">  = > ;=20 > </SPAN></FONT></SPAN></SPAN></FONT><![endif]><FONT face=3DArial color=3Db= > lue=20 > size=3D2><SPAN style=3D"FONT-SIZE: 10pt; COLOR: blue; FONT-FAMILY: Arial"= > >The=20 > wording of "cover property" being a "one match" is too strong. There are = > cases=20 > (implication) when more than one match results, in fact we rely on this (= > per=20 > previous discussion) to define the semantics of "cover=20 > sequence".</SPAN></FONT><FONT face=3DArial size=3D2><SPAN=20 > style=3D"FONT-SIZE: 10pt; FONT-FAMILY: Arial"><o:p></o:p></SPAN></FONT></= > P> > <P class=3DMsoNormal><FONT face=3DArial color=3Dblue size=3D2><SPAN=20 > style=3D"FONT-SIZE: 10pt; COLOR: blue; FONT-FAMILY: Arial"><o:p> </o= > :p></SPAN></FONT></P> > <P class=3DMsoNormal><FONT face=3DArial color=3Dred size=3D3><SPAN=20 > style=3D"FONT-SIZE: 12pt; COLOR: red; FONT-FAMILY: Arial">[Lisa Piper=20 > >>>] any suggestions?<o:p></o:p></SPAN></FONT></P></DIV> > <DIV> > <P class=3DMsoNormal><FONT face=3D"Times New Roman" size=3D3><SPAN=20 > style=3D"FONT-SIZE: 12pt"> <o:p></o:p></SPAN></FONT></P></DIV> > <DIV> > <P class=3DMsoNormal=20 > style=3D"MARGIN-LEFT: 0.5in; TEXT-INDENT: -0.25in; mso-list: l0 level1 lf= > o1"><![if !supportLists]><FONT=20 > face=3DArial color=3Dblue size=3D2><SPAN=20 > style=3D"FONT-SIZE: 10pt; COLOR: blue; FONT-FAMILY: Arial"><SPAN=20 > style=3D"mso-list: Ignore">3)<FONT face=3D"Times New Roman" size=3D1><SPA= > N=20 > style=3D"FONT: 7pt 'Times New Roman'">  = > ;=20 > </SPAN></FONT></SPAN></SPAN></FONT><![endif]><FONT face=3DArial color=3Db= > lue=20 > size=3D2><SPAN style=3D"FONT-SIZE: 10pt; COLOR: blue; FONT-FAMILY: Arial"= > >Do we=20 > need to file a separate proposal for semantics update (the annex) ? Or ar= > e we=20 > adding to same ?</SPAN></FONT><FONT face=3DArial size=3D2><SPAN=20 > style=3D"FONT-SIZE: 10pt; FONT-FAMILY: Arial"><o:p></o:p></SPAN></FONT></= > P> > <P class=3DMsoNormal><FONT face=3DArial color=3Dblue size=3D2><SPAN=20 > style=3D"FONT-SIZE: 10pt; COLOR: blue; FONT-FAMILY: Arial"><o:p> </o= > :p></SPAN></FONT></P> > <P class=3DMsoNormal><FONT face=3DArial color=3Dred size=3D3><SPAN=20 > style=3D"FONT-SIZE: 12pt; COLOR: red; FONT-FAMILY: Arial">[Lisa Piper=20 > >>>] I don’t think a separate proposal is good. I wi= > ll add it=20 > to this. I assume you are talking about Annex A? =20 > <o:p></o:p></SPAN></FONT></P></DIV> > <DIV> > <P class=3DMsoNormal><FONT face=3D"Times New Roman" size=3D3><SPAN=20 > style=3D"FONT-SIZE: 12pt"> <o:p></o:p></SPAN></FONT></P></DIV> > <P class=3DMsoNormal><FONT face=3DArial size=3D2><SPAN=20 > style=3D"FONT-SIZE: 10pt; FONT-FAMILY: Arial">Thx.</SPAN></FONT><o:p></o:= > p></P> > <P class=3DMsoNormal><FONT face=3DArial size=3D2><SPAN=20 > style=3D"FONT-SIZE: 10pt; FONT-FAMILY: Arial">-Bassam.</SPAN></FONT><o:p>= > </o:p></P> > <DIV> > <P class=3DMsoNormal><FONT face=3D"Times New Roman" size=3D3><SPAN=20 > style=3D"FONT-SIZE: 12pt"> <o:p></o:p></SPAN></FONT></P></DIV> > <P class=3DMsoNormal><FONT face=3D"Times New Roman" size=3D3><SPAN=20 > style=3D"FONT-SIZE: 12pt"><o:p> </o:p></SPAN></FONT></P> > <DIV class=3DMsoNormal style=3D"TEXT-ALIGN: center" align=3Dcenter><FONT= > =20 > face=3D"Times New Roman" size=3D3><SPAN style=3D"FONT-SIZE: 12pt"> > <HR tabIndex=3D-1 align=3Dcenter width=3D"100%" SIZE=3D2> > </SPAN></FONT></DIV> > <P class=3DMsoNormal style=3D"MARGIN-BOTTOM: 12pt"><B><FONT face=3DTahoma= > =20 > size=3D2><SPAN=20 > style=3D"FONT-WEIGHT: bold; FONT-SIZE: 10pt; FONT-FAMILY: Tahoma">From:</= > SPAN></FONT></B><FONT=20 > face=3DTahoma size=3D2><SPAN style=3D"FONT-SIZE: 10pt; FONT-FAMILY: Tahom= > a">=20 > owner-sv-ac@eda.org [mailto:owner-sv-ac@eda.org] <B><SPAN=20 > style=3D"FONT-WEIGHT: bold">On Behalf Of </SPAN></B>Lisa Piper<BR><B><SPA= > N=20 > style=3D"FONT-WEIGHT: bold">Sent:</SPAN></B> Wednesday, July 11, 2007 6:1= > 8=20 > AM<BR><B><SPAN style=3D"FONT-WEIGHT: bold">To:</SPAN></B>=20 > sv-ac@eda-stds.org<BR><B><SPAN style=3D"FONT-WEIGHT: bold">Subject:</SPAN= > ></B>=20 > [sv-ac] updated cover sequence proposal</SPAN></FONT><o:p></o:p></P> > <P><FONT face=3DArial size=3D3><SPAN style=3D"FONT-SIZE: 12pt; FONT-FAMIL= > Y: Arial"><!-- Converted from text/rtf format -->I=20 > have uploaded a new version of 1768</SPAN></FONT> <FONT face=3DArial><SPA= > N=20 > style=3D"FONT-FAMILY: Arial">– cover</SPAN></FONT> <FONT face=3DAri= > al><SPAN=20 > style=3D"FONT-FAMILY: Arial">sequence. It is attached for=20 > convenience.</SPAN></FONT> <o:p></o:p></P> > <P><FONT face=3DArial size=3D3><SPAN=20 > style=3D"FONT-SIZE: 12pt; FONT-FAMILY: Arial">Lisa</SPAN></FONT><FONT fac= > e=3DArial=20 > color=3Dblack size=3D2><SPAN=20 > style=3D"FONT-SIZE: 10pt; COLOR: black; FONT-FAMILY: Arial">=20 > <<1768_cover_sequence_3.pdf>> </SPAN></FONT><o:p></o:p></P> > <P class=3DMsoNormal><FONT face=3D"Times New Roman" size=3D3><SPAN=20 > style=3D"FONT-SIZE: 12pt"><BR>-- <BR>This message has been scanned for vi= > ruses=20 > and <BR>dangerous content by <A=20 > href=3D"http://www.mailscanner.info/"></SPAN></B><B><SPAN=20 > style=3D"FONT-WEIGHT: bold">MailScanner</A>, and is <BR>believed to be cl= > ean.=20 > <o:p></o:p></SPAN></FONT></P></DIV><BR>-- <BR>This message has been scann= > ed=20 > for viruses and <BR>dangerous content by <A=20 > href=3D"http://www.mailscanner.info/"></B><B>MailScanner</A>, and is=20 > <BR>believed to be clean. </B></BLOCKQUOTE></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. > </HTML> > > ------_=_NextPart_001_01C7C3E6.1619019E-- -- This message has been scanned for viruses and dangerous content by MailScanner, and is believed to be clean.Received on Wed Jul 11 12:18:43 2007
This archive was generated by hypermail 2.1.8 : Wed Jul 11 2007 - 12:19:04 PDT