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.