RE: [sv-ac] RE: Mantis #805

Hi Manisha, 

Yes on 1st paragraph below. In addition to the snippet's "For any
assertion ..." preceding formula, there is another stmt earlier on same
page stating this clearly: "- For assertion handle, the coverable
entities are assertions." As we discussed before the word "cover[able]"
is talking here about measurement of the "assert", not the "cover"
directive. [BTW, this clause was written independently before the
assertion chapter caught up.] 

So, the stmt is already there explaining current meaning (can be
clarified more ...). Of course clarifying more/changing one or both is
always an option, albeit for covers I thought we had decided *not* to
explicitly count the disabled, reason that portion is the way it is.

** Summary: As it stands, snippets talking about separate things: assert
vs. cover. We can revisit what they should be, then clarify/change one
or both.

Thx.
-Bassam.

-----Original Message-----
From: owner-sv-ac@eda.org [mailto:owner-sv-ac@eda.org] On Behalf Of
Kulshrestha, Manisha
Sent: Monday, August 21, 2006 9:54 AM
To: Eduard Cerny
Cc: sv-ac@eda-stds.org
Subject: [sv-ac] RE: Mantis #805

Hi,

This issue has confused few of us already (including me). Based on the
discussions I had with Bassam while modifying this proposal some time
back, the formula and all the vpi routines apply to assertions (i.e
assert directives and not cover directives). 

Bassam, please comment on this as Lisa had similar doubts earlier. May
be we need to add something in the LRM which makes it clear or we need
to modify the cover directives section to include disabled count.

Thanks.
Manisha

-----Original Message-----
From: Eduard Cerny [mailto:Eduard.Cerny@synopsys.com]
Sent: Friday, August 18, 2006 8:32 AM
To: Kulshrestha, Manisha
Cc: sv-ac@eda-stds.org
Subject: Mantis #805

Hi Manisha,

I looked at the proposal for #805 and there is something I do not
understand.

It state on the 1st page:

"The results of coverage statement for a property shall contain the
following:
- Number of times attempted
- Number of times succeeded
- Number of times failed
- Number of times succeeded because of vacuity"

and also

"The coverage counters for success, failure or vacuous success do not
include disabled evaluations. The attempt counter includes the attempts
which result in disabled evaluation."


Then on the 2nd page it has

"For any assertion, the number of attempts that have not yet reached any
conclusion (success or failure) can be derived from the
formula:
in progress = attempts - (successes + vacuous success + disabled +
failures)"

But if there is no counter for disabled, there is no way to obtain the
number of attempts in progress.

Should there also be a counter for disabled?

Thanks,
ed