Re: [sv-ac] 1768 review

Hi Ed:

Yes, this can be done.  We define the semantics of "cover sequence" in
terms of evaluation of a related assertion directive on an implication
property with a match item.

I don't think it matters whether the related assertion directive is
"assert property" or "cover property" since we are interested in the
number of executions of the match item.

J.H.

> X-MIMEOLE: Produced By Microsoft Exchange V6.5
> Content-class: urn:content-classes:message
> Date: Thu, 5 Jul 2007 07:23:05 -0700
> Thread-Topic: [sv-ac] 1768 review
> Thread-Index: Ace/BkwHNlBv3xv/R8S/LtaxPEmPgAACTM7Q
> From: "Eduard Cerny" <Eduard.Cerny@synopsys.com>
> Cc: <piper@cadence.com>, <sv-ac@eda-stds.org>
> X-OriginalArrivalTime: 05 Jul 2007 14:23:06.0457 (UTC) FILETIME=[013DFC90:01C7BF10]
> 
> hi,
> 
> shouldn't then the meaning of "cover sequence" be defined or explained
> using that assert statemnt? Actually, it could be
> 
> cover property (disable iff (rst) S |-> (1'b1, increment_count()));
> 
> and the coverage be the number of times the task increment_count() is
> executed?
> 
> regards,
> ed
> 
> 
> 
> > -----Original Message-----
> > From: owner-sv-ac@eda.org [mailto:owner-sv-ac@eda.org] On=20
> > Behalf Of John Havlicek
> > Sent: Thursday, July 05, 2007 9:10 AM
> > To: Bassam.Tabbara@synopsys.COM
> > Cc: john.havlicek@freescale.com; Bassam.Tabbara@synopsys.COM;=20
> > piper@cadence.com; sv-ac@eda-stds.org
> > Subject: Re: [sv-ac] 1768 review
> >=20
> > Hi Bassam:
> >=20
> > > BT>> "top level" means (top) property in current LRM.=20
> > Before we get into
> > > the directive level, we need a sequence layer disable iff=20
> > definition,
> > > only then can a "... sequence" directive (only cosmetics in my mind)
> > > allow the matches, e.g. one could think of "assert sequence".
> > > "sequence_expr" already means multiple matches, "disable=20
> > iff ..." does
> > > not in general as currently defined.
> >=20
> > I did not understand this.
> >=20
> > It is intuitively clear to me that whatever the semantics of
> >=20
> > (1)  cover sequence (disable iff (blah) S);
> >=20
> > we should get exactly the same number of hits per attempt as=20
> > we get executions of "$disable("bleh")" in
> >=20
> > (2)  assert property (disable iff (blah) S |-> (1'b1,=20
> > $display("bleh")));
> >=20
> > I assume, of course, that $display("bleh") does not appear in S.
> >=20
> > If this is not the case, then we have a different notion of "all
> > matches" for "cover sequence" than we do for matching the antecedent
> > of an implication, and that seems very bad to me.
> >=20
> > Currently, we do not have formal definitions of multiplicity of
> > matching or of the semantics of execution of match items, so the
> > semantics of neither (1) nor (2) is precisely defined.  But I still
> > think the relation I stated above should hold.
> >=20
> > I thought that this would be enough semantic basis to go ahead=20
> > with 1768.
> >=20
> > What do you think?
> >=20
> > I still want to get to resolution of 0921, which I think will provide
> > the precise definitions.  Whether we will be able to do this in the
> > 2008 effort is not so clear.
> >=20
> > J.H.
> >=20
> >=20
> > > x-mimeole: Produced By Microsoft Exchange V6.5
> > > Content-class: urn:content-classes:message
> > > Date: Wed, 4 Jul 2007 10:06:26 -0700
> > > Thread-Topic: [sv-ac] 1768 review
> > > Thread-Index: Ace+S7H1lwLvmPGeQ7+Sp5uKBkRjVQACXcAg
> > > From: "Bassam Tabbara" <Bassam.Tabbara@synopsys.com>
> > > Cc: <sv-ac@eda-stds.org>
> > > X-OriginalArrivalTime: 04 Jul 2007 17:06:27.0382 (UTC)=20
> > FILETIME=3D[A8A2B560:01C7BE5D]
> > >=20
> > > Hi John=3D20
> > >=20
> > > Some comments below with BT>>.
> > >=20
> > > Thx.
> > > -Bassam.
> > >=20
> > > -----Original Message-----
> > > From: John Havlicek [mailto:john.havlicek@freescale.com]=3D20
> > > Sent: Wednesday, July 04, 2007 7:58 AM
> > > To: Bassam.Tabbara@synopsys.COM; piper@cadence.com
> > > Cc: sv-ac@eda-stds.org
> > > Subject: Re: [sv-ac] 1768 review
> > >=20
> > > Hi Bassam:
> > >=20
> > > > Again, the semantics of such syntax is not defined for=20
> > sequence --=3D20
> > > > disable iff is at top level only so the production you have=3D20
> > > > effectively
> > > > says: cover sequence (property_spec).
> > > >=3D20
> > > > Now, I thought the proposal intent was to distinguish the=3D20
> > > > property_spec/sequence_expr confusion (see motivation),=20
> > and merely add
> > >=20
> > > > a cover sequence syntax for the old cover property=20
> > (sequence_expr),=3D20
> > > > hence my #2 below. If there is more to it, then this=20
> > needs to be=3D20
> > > > clarified/defined and/or new syntax introduced.
> > >=20
> > > My understanding of the proposal and Lisa's comments is=20
> > that there is
> > > something new, namely the ability to add the "disable iff"=20
> > to the "cover
> > > sequence" directive and still have all match semantics.
> > >=20
> > > BT>> Indeed -- so do I after Lisa's comments.
> > >=20
> > > I think that this is a good thing for the reasons that Lisa cited.
> > > This "disable iff" is still top level -- it is attached at=20
> > the "cover
> > > sequence" directive level and cannot be embedded within the
> > > sequence_expr.
> > >=20
> > > BT>> "top level" means (top) property in current LRM.=20
> > Before we get into
> > > the directive level, we need a sequence layer disable iff=20
> > definition,
> > > only then can a "... sequence" directive (only cosmetics in my mind)
> > > allow the matches, e.g. one could think of "assert sequence".
> > > "sequence_expr" already means multiple matches, "disable=20
> > iff ..." does
> > > not in general as currently defined.
> > >=20
> > > For the semantics, I think it is intuitively clear that=20
> > each sub-attempt
> > > of a sequence_expr that completes its match without the=20
> > occurrence of
> > > the "disable iff" condition should count towards the all=20
> > match total for
> > > that attempt.  Any sub-attempt that is in progress and not=20
> > yet complete
> > > at the occurrence of the "disable iff" condition should be aborted.
> > >=20
> > > Lisa, can you add some language like this to the proposal=20
> > that describes
> > > the way the "disable iff" behaves together with all match coverage?
> > >=20
> > > BT>> Must also update the formal semantics (in addition to=20
> > consistency I
> > > mention above).=3D20
> > >=20
> > > By the way, I think that this is not really a new semantic concept.
> > > I think that we have the same semantic question of how=20
> > "disable iff"=3D20
> > > interacts with an all match evaluation of a sequence_expr under the
> > > existing LRM.  For example, we can write a sequence_expr S=20
> > that has been
> > > instrumented with $display match items at the ends of various
> > > subexpressions and ask which $displays execute for an attempt of
> > >=20
> > >    assert property (disable iff (blah) S |-> 1'b1);
> > >=20
> > > A precise definition of the semantics could be derived by a=20
> > resolution
> > > of Mantis 0921.
> > >=20
> > > BT>> Ok I see what you are getting at, still you are=20
> > picking a special
> > > case of *property* i.e. implication. The concept of=20
> > multiple matches is
> > > not totally foreign I agree, still disable of a sequence needs to be
> > > defined as such on its own outside of the directive=20
> > context, a casual
> > > introduction will not do.
> > >=20
> > > J.H.
> > >=20
> > > > X-Authentication-Warning: server.eda-stds.org: majordom=20
> > set sender to=3D20
> > > > owner-sv-ac@eda.org using -f
> > > > x-mimeole: Produced By Microsoft Exchange V6.5
> > > > Content-class: urn:content-classes:message
> > > > Date: Wed, 4 Jul 2007 00:05:19 -0700
> > > > Thread-Topic: [sv-ac] 1768 review
> > > > Thread-Index:=20
> > Ace7/tvvRp2OS1iRQaaXh+QgQIDg1AB7b54AAAFrPvUAAAjtQAADvXMg
> > > > From: "Bassam Tabbara" <Bassam.Tabbara@synopsys.com>
> > > > X-OriginalArrivalTime: 04 Jul 2007 07:05:20.0544 (UTC)=3D20
> > > > FILETIME=3D3D[AF1FFA00:01C7BE09]
> > > > X-eda.org-MailScanner: Found to be clean, Found to be clean
> > > > X-Spam-Status: No, No
> > > > X-MIME-Autoconverted: from quoted-printable to 8bit by=3D20
> > > > server.eda-stds.org id l6475XtM016515
> > > > Sender: owner-sv-ac@eda.org
> > > > X-eda.org-MailScanner-Information: Please contact the ISP=20
> > for more=3D20
> > > > information
> > > > X-eda.org-MailScanner-From: owner-sv-ac@server.eda.org
> > > >=3D20
> > > > Hi Lisa,
> > > >=3D20
> > > > Again, the semantics of such syntax is not defined for=20
> > sequence --=3D20
> > > > disable iff is at top level only so the production you have=3D20
> > > > effectively
> > > > says: cover sequence (property_spec).
> > > >=3D20
> > > > Now, I thought the proposal intent was to distinguish the=3D20
> > > > property_spec/sequence_expr confusion (see motivation),=20
> > and merely add
> > >=20
> > > > a cover sequence syntax for the old cover property=20
> > (sequence_expr),=3D20
> > > > hence my #2 below. If there is more to it, then this=20
> > needs to be=3D20
> > > > clarified/defined and/or new syntax introduced.
> > > >=3D20
> > > > Thx.
> > > > -Bassam.
> > > >=3D20
> > > > -----Original Message-----
> > > > From: Lisa Piper [mailto:piper@cadence.com]
> > > > Sent: Tuesday, July 03, 2007 9:24 PM
> > > > To: Bassam Tabbara; sv-ac@eda-stds.org
> > > > Subject: RE: [sv-ac] 1768 review
> > > >=3D20
> > > > Hi Bassam,
> > > >=3D20
> > > > The real difference between cover property and cover=20
> > sequence is=3D20
> > > > whether the first match or all match semantics is used. =20
> > As it turns=3D20
> > > > out, the all match semantics only makes sense for=20
> > sequences, hense=3D20
> > > > cover sequence.  But it is still desireable to not count=20
> > some cases,=3D20
> > > > such as reset.
> > > >=3D20
> > > > I agree that disable iff goes with property_spec and not=3D20
> > > > sequence_expr, which is why it needed to be added to the syntax.
> > > >=3D20
> > > > lisa
> > > >=3D20
> > > > -----Original Message-----
> > > > From: Bassam Tabbara [mailto:Bassam.Tabbara@synopsys.com]
> > > > Sent: Wednesday, July 04, 2007 12:18 AM
> > > > To: Lisa Piper; Bassam.tabbara@synopsys.com; sv-ac@eda-stds.org
> > > > Subject: Re: [sv-ac] 1768 review
> > > >=3D20
> > > > Hi Lisa,
> > > >=3D20
> > > > To be more specific, what I was getting at is that a=20
> > disable iff goes=3D20
> > > > with property_spec and not a sequence_expr currently.=20
> > Same reasoning=3D20
> > > > in LRM would apply here for cover sequence, leaving the=20
> > disable at=3D20
> > > > property level with cover property.
> > > >=3D20
> > > > THX.=3D20
> > > > -Bassam
> > > >=3D20
> > > > -----Original Message-----
> > > > From: Lisa Piper <piper@cadence.com>
> > > > To: Bassam Tabbara <Bassam.Tabbara@synopsys.COM>;=20
> > sv-ac@eda-stds.org=3D20
> > > > <sv-ac@eda-stds.org>
> > > > Sent: Tue Jul 03 20:47:14 2007
> > > > Subject: RE: [sv-ac] 1768 review
> > > >=3D20
> > > > Hi Bassam,
> > > >=3D20
> > > > Thanks for the comments. I agree with all except #2.=20
> > There may be=3D20
> > > > times when you don't want to report coverage of a=20
> > sequence, such as=3D20
> > > > during reset. I think it applies.
> > > >=3D20
> > > > I have uploaded a revised copy of 1768 to Mantis, attached =
> for=3D20
> > > > convenience.
> > > >=3D20
> > > > Lisa
> > > >=3D20
> > > > -----Original Message-----
> > > > From: owner-sv-ac@eda.org [mailto:owner-sv-ac@eda.org] On=20
> > Behalf Of=3D20
> > > > Bassam Tabbara
> > > > Sent: Sunday, July 01, 2007 12:43 PM
> > > > To: sv-ac@eda-stds.org
> > > > Subject: [sv-ac] 1768 review
> > > >=3D20
> > > > Hi Lisa,
> > > > =3D20
> > > > Here's my feedback:
> > > >=3D20
> > > > 1) Syntax 16-16
> > > >=3D20
> > > > Change "Cover_.... :=3D3D" to "cover_..."
> > > >=3D20
> > > > 2) "disable iff" does not make sense in above production=20
> > since this is
> > >=20
> > > > a
> > > > *sequence*
> > > >=3D20
> > > > 3) ditto on (1)/(2) for A.6.10
> > > >=3D20
> > > > 4) 16.14.3 change "e.g. cover property" to "i.e. cover property"
> > > >=3D20
> > > > 5) For 16.14.3 see (2) above and update
> > > >=3D20
> > > > 6) Last sentence "Whether cover property or cover=20
> > sequence is used is=3D20
> > > > dependent on whether one match or multiple match semantics is
> > > desired."
> > > >=3D20
> > > > Change to
> > > >=3D20
> > > > "Whether cover property or
> > > > cover sequence is used depends on whether one match or=20
> > multiple match=3D20
> > > > semantics is desired respectively.
> > > >=3D20
> > > > =3D20
> > > > Thx.
> > > > -Bassam.
> > > >=3D20
> > > > --
> > > > This message has been scanned for viruses and dangerous=20
> > content by=3D20
> > > > MailScanner, and is believed to be clean.
> > > >=3D20
> > > >=3D20
> > > >=3D20
> > > > --
> > > > This message has been scanned for viruses and dangerous=20
> > content by=3D20
> > > > MailScanner, and is believed to be clean.
> > > >=3D20
> > > >=3D20
> >=20
> > --=20
> > This message has been scanned for viruses and
> > dangerous content by MailScanner, and is
> > believed to be clean.
> >=20
> >=20

-- 
This message has been scanned for viruses and
dangerous content by MailScanner, and is
believed to be clean.