Re: [sv-ac] 1768 review

Hi Bassam:

Let us use "cover property" then!

I am encouraged that we are converging on 1768.

J.H.

> x-mimeole: Produced By Microsoft Exchange V6.5
> Content-class: urn:content-classes:message
> X-Former-Content-Transfer-Encoding: base64
> Date: Thu, 5 Jul 2007 07:51:46 -0700
> Thread-Topic: [sv-ac] 1768 review
> Thread-Index: Ace/El0MSnVL3iJLRrqElfYMKSHOfwAAaVO+
> From: "Bassam Tabbara" <Bassam.Tabbara@synopsys.com>
> Cc: <Bassam.tabbara@synopsys.com>, <piper@cadence.com>, <sv-ac@eda-stds.org>
> X-OriginalArrivalTime: 05 Jul 2007 14:51:47.0229 (UTC) FILETIME=[02E6F4D0:01C7BF14]
> 
> Makes sense, propably clearer to tie to cover property.
> 
> THX. 
> -Bassam
> 
> -----Original Message-----
> From: John Havlicek <john.havlicek@freescale.com>
> To: Eduard.Cerny@synopsys.COM <Eduard.Cerny@synopsys.COM>
> CC: john.havlicek@freescale.com <john.havlicek@freescale.com>; Bassam.Tabbara@synopsys.COM <Bassam.Tabbara@synopsys.COM>; piper@cadence.com <piper@cadence.com>; sv-ac@eda-stds.org <sv-ac@eda-stds.org>
> Sent: Thu Jul 05 07:39:46 2007
> Subject: 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

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