RE: [sv-ac] 1768 review

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 
> 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; 
> piper@cadence.com; sv-ac@eda-stds.org
> Subject: Re: [sv-ac] 1768 review
> 
> Hi Bassam:
> 
> > BT>> "top level" means (top) property in current LRM. 
> Before we get into
> > the directive level, we need a sequence layer disable iff 
> 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 
> iff ..." does
> > not in general as currently defined.
> 
> I did not understand this.
> 
> It is intuitively clear to me that whatever the semantics of
> 
> (1)  cover sequence (disable iff (blah) S);
> 
> we should get exactly the same number of hits per attempt as 
> we get executions of "$disable("bleh")" in
> 
> (2)  assert property (disable iff (blah) S |-> (1'b1, 
> $display("bleh")));
> 
> I assume, of course, that $display("bleh") does not appear in S.
> 
> 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.
> 
> 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.
> 
> I thought that this would be enough semantic basis to go ahead 
> with 1768.
> 
> What do you think?
> 
> 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.
> 
> J.H.
> 
> 
> > 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) 
> FILETIME=[A8A2B560:01C7BE5D]
> > 
> > Hi John=20
> > 
> > Some comments below with BT>>.
> > 
> > Thx.
> > -Bassam.
> > 
> > -----Original Message-----
> > From: John Havlicek [mailto:john.havlicek@freescale.com]=20
> > 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
> > 
> > Hi Bassam:
> > 
> > > Again, the semantics of such syntax is not defined for 
> sequence --=20
> > > disable iff is at top level only so the production you have=20
> > > effectively
> > > says: cover sequence (property_spec).
> > >=20
> > > Now, I thought the proposal intent was to distinguish the=20
> > > property_spec/sequence_expr confusion (see motivation), 
> and merely add
> > 
> > > a cover sequence syntax for the old cover property 
> (sequence_expr),=20
> > > hence my #2 below. If there is more to it, then this 
> needs to be=20
> > > clarified/defined and/or new syntax introduced.
> > 
> > My understanding of the proposal and Lisa's comments is 
> that there is
> > something new, namely the ability to add the "disable iff" 
> to the "cover
> > sequence" directive and still have all match semantics.
> > 
> > BT>> Indeed -- so do I after Lisa's comments.
> > 
> > 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 
> the "cover
> > sequence" directive level and cannot be embedded within the
> > sequence_expr.
> > 
> > BT>> "top level" means (top) property in current LRM. 
> Before we get into
> > the directive level, we need a sequence layer disable iff 
> 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 
> iff ..." does
> > not in general as currently defined.
> > 
> > For the semantics, I think it is intuitively clear that 
> each sub-attempt
> > of a sequence_expr that completes its match without the 
> occurrence of
> > the "disable iff" condition should count towards the all 
> match total for
> > that attempt.  Any sub-attempt that is in progress and not 
> yet complete
> > at the occurrence of the "disable iff" condition should be aborted.
> > 
> > Lisa, can you add some language like this to the proposal 
> that describes
> > the way the "disable iff" behaves together with all match coverage?
> > 
> > BT>> Must also update the formal semantics (in addition to 
> consistency I
> > mention above).=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 
> "disable iff"=20
> > interacts with an all match evaluation of a sequence_expr under the
> > existing LRM.  For example, we can write a sequence_expr S 
> that has been
> > instrumented with $display match items at the ends of various
> > subexpressions and ask which $displays execute for an attempt of
> > 
> >    assert property (disable iff (blah) S |-> 1'b1);
> > 
> > A precise definition of the semantics could be derived by a 
> resolution
> > of Mantis 0921.
> > 
> > BT>> Ok I see what you are getting at, still you are 
> picking a special
> > case of *property* i.e. implication. The concept of 
> 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 
> context, a casual
> > introduction will not do.
> > 
> > J.H.
> > 
> > > X-Authentication-Warning: server.eda-stds.org: majordom 
> set sender to=20
> > > 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: 
> Ace7/tvvRp2OS1iRQaaXh+QgQIDg1AB7b54AAAFrPvUAAAjtQAADvXMg
> > > From: "Bassam Tabbara" <Bassam.Tabbara@synopsys.com>
> > > X-OriginalArrivalTime: 04 Jul 2007 07:05:20.0544 (UTC)=20
> > > FILETIME=3D[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=20
> > > server.eda-stds.org id l6475XtM016515
> > > Sender: owner-sv-ac@eda.org
> > > X-eda.org-MailScanner-Information: Please contact the ISP 
> for more=20
> > > information
> > > X-eda.org-MailScanner-From: owner-sv-ac@server.eda.org
> > >=20
> > > Hi Lisa,
> > >=20
> > > Again, the semantics of such syntax is not defined for 
> sequence --=20
> > > disable iff is at top level only so the production you have=20
> > > effectively
> > > says: cover sequence (property_spec).
> > >=20
> > > Now, I thought the proposal intent was to distinguish the=20
> > > property_spec/sequence_expr confusion (see motivation), 
> and merely add
> > 
> > > a cover sequence syntax for the old cover property 
> (sequence_expr),=20
> > > hence my #2 below. If there is more to it, then this 
> needs to be=20
> > > clarified/defined and/or new syntax introduced.
> > >=20
> > > Thx.
> > > -Bassam.
> > >=20
> > > -----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
> > >=20
> > > Hi Bassam,
> > >=20
> > > The real difference between cover property and cover 
> sequence is=20
> > > whether the first match or all match semantics is used.  
> As it turns=20
> > > out, the all match semantics only makes sense for 
> sequences, hense=20
> > > cover sequence.  But it is still desireable to not count 
> some cases,=20
> > > such as reset.
> > >=20
> > > I agree that disable iff goes with property_spec and not=20
> > > sequence_expr, which is why it needed to be added to the syntax.
> > >=20
> > > lisa
> > >=20
> > > -----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
> > >=20
> > > Hi Lisa,
> > >=20
> > > To be more specific, what I was getting at is that a 
> disable iff goes=20
> > > with property_spec and not a sequence_expr currently. 
> Same reasoning=20
> > > in LRM would apply here for cover sequence, leaving the 
> disable at=20
> > > property level with cover property.
> > >=20
> > > THX.=20
> > > -Bassam
> > >=20
> > > -----Original Message-----
> > > From: Lisa Piper <piper@cadence.com>
> > > To: Bassam Tabbara <Bassam.Tabbara@synopsys.COM>; 
> sv-ac@eda-stds.org=20
> > > <sv-ac@eda-stds.org>
> > > Sent: Tue Jul 03 20:47:14 2007
> > > Subject: RE: [sv-ac] 1768 review
> > >=20
> > > Hi Bassam,
> > >=20
> > > Thanks for the comments. I agree with all except #2. 
> There may be=20
> > > times when you don't want to report coverage of a 
> sequence, such as=20
> > > during reset. I think it applies.
> > >=20
> > > I have uploaded a revised copy of 1768 to Mantis, attached for=20
> > > convenience.
> > >=20
> > > Lisa
> > >=20
> > > -----Original Message-----
> > > From: owner-sv-ac@eda.org [mailto:owner-sv-ac@eda.org] On 
> Behalf Of=20
> > > Bassam Tabbara
> > > Sent: Sunday, July 01, 2007 12:43 PM
> > > To: sv-ac@eda-stds.org
> > > Subject: [sv-ac] 1768 review
> > >=20
> > > Hi Lisa,
> > > =20
> > > Here's my feedback:
> > >=20
> > > 1) Syntax 16-16
> > >=20
> > > Change "Cover_.... :=3D" to "cover_..."
> > >=20
> > > 2) "disable iff" does not make sense in above production 
> since this is
> > 
> > > a
> > > *sequence*
> > >=20
> > > 3) ditto on (1)/(2) for A.6.10
> > >=20
> > > 4) 16.14.3 change "e.g. cover property" to "i.e. cover property"
> > >=20
> > > 5) For 16.14.3 see (2) above and update
> > >=20
> > > 6) Last sentence "Whether cover property or cover 
> sequence is used is=20
> > > dependent on whether one match or multiple match semantics is
> > desired."
> > >=20
> > > Change to
> > >=20
> > > "Whether cover property or
> > > cover sequence is used depends on whether one match or 
> multiple match=20
> > > semantics is desired respectively.
> > >=20
> > > =20
> > > Thx.
> > > -Bassam.
> > >=20
> > > --
> > > This message has been scanned for viruses and dangerous 
> content by=20
> > > MailScanner, and is believed to be clean.
> > >=20
> > >=20
> > >=20
> > > --
> > > This message has been scanned for viruses and dangerous 
> content by=20
> > > 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.
> 
> 

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