Subject: Re: Fwd: [sv-ac] Erratta on implication operator.
From: John Havlicek (john.havlicek@motorola.com)
Date: Sun Nov 02 2003 - 08:12:23 PST
All:
I agree with Adam from the point of view of defining whether
an attempt for a property passes or fails.
I do not know what, if anything, this says about when the
action blocks execute or how coverage is collected.
For example, if this property form is put in a coverage
statement, should the first_match rule still apply?
It is also possible that, due to distinct local variable
contexts, there is more than one thread that achieves
the first match.
Best regards,
John H.
>
> Adam had sent this erratum some time ago.
> This was left off the original errata list.
>
> Please review this and send any comments.
>
> We can go over this and take a vote at
> one of the upcoming meetings.
>
> Regards,
>
> Arif
> --------------
>
> >Date: Tue, 26 Aug 2003 09:02:57 -0500
> >From: Adam Krolnik <krolnik@lsil.com>
> >User-Agent: Mozilla/5.0 (X11; U; SunOS sun4u; en-US; rv:1.0.1)
> >Gecko/20020920 Netscape/7.0
> >X-Accept-Language: en-us, en
> >To: sv-ac@eda.org
> >Subject: [sv-ac] Erratta on implication operator.
> >Sender: owner-sv-ac@eda.org
> >X-pstn-levels: (C:80.8653 M:99.4056 P:95.9108 R:95.9108 S:33.9901 )
> >
> >
> >
> >Good morning;
> >
> >I have an erratta concerning the implication operator.
> >
> >To this list of points in 17.7.11, I would like to add the following
> >before the last
> >point (which may be removed pending other proposals.)
> >
> >
> >WAS:
> ><nothing>
> >
> >Proposed:
> >
> >o Only zero or one match of the consequent sequence_expr will occur. There
> >is an implicit first_match operator applied to the consequent. For example.
> >
> > antecedent_expr |-> consequent_expr
> >
> >is really evaluated as:
> >
> > antecedent_expr |-> first_match (consequent_expr)
> >
> >
> >There is a reference to this in section 17.10 (pg 176.) but it should be
> >explicitly
> >noted here next to the operator, in addition to the section on properties.
> >
> > Thanks.
> >
> > Adam Krolnik
> > Verification Mgr.
> > LSI Logic Corp.
> > Plano TX. 75074
This archive was generated by hypermail 2b28 : Sun Nov 02 2003 - 08:13:15 PST