FW: [sv-ac] SV-AC: on cover property, disable if and reporting...

Ed,

I asked Johny whether we can work on enhancements and he said yes.

Shalom

-----Original Message-----
From: owner-sv-ac@eda.org [mailto:owner-sv-ac@eda.org] On Behalf Of
Eduard Cerny
Sent: Wednesday, March 15, 2006 11:10 PM
To: sv-ac@eda.org
Subject: [sv-ac] SV-AC: on cover property, disable if and reporting... 

Hello,

There are currently several intertwined issues that relate how to report
disabled and vacuous successes, how to control when action blocks
execute and how to formally define cover properties and the effect of
disable iff, condition inference, action blocks, etc. on such
statements.

What is the simplest thing for the user? Clearly, vacuous and disabled
attempts should not be included in reporting coverage or assertion
successes. Similarly, there is need to not execute action blocks under
such conditions. Also, formal semantics for covers are missing. 

What changes are likely to get through to the LRM given that no
enhancements are allowed and yet some of the changes are clearly needed?

We can try to make changes that maintain complete backward
compatibility, such as the execution of success action statements on
vacuous and real successes of assertions, as reflected in #805 (and of
which I (ed) was also a proponent), but it makes the use model more
complicated. Therefore, after some discussions among ourselves, we
arrived at the conclusion that it is preferable to do the right
modification, even if it does  change the default behavior.

In the following we outline a possible solution:

- Change "disabled success" to simply "disabled" category.

- Remove referring to disabled assertions as having vacuous successes.
Name these cases as simply "disabled".

- Add a note that a disabled assertion does not execute the success
action statement if not enabled by the assertdisableon task call. 
Similarly for assertions that pass vacuously - by default no execution
of the success action statement.

- cover properties: instead of using the terminology success, failure,
vacuous success, etc. that is the same as for assert statements, let's
define coverage, covered, covered vacuously, and disabled.

define coverage of cover property (disable iff (rst) a |-> p) along the
lines Dmitry suggested as the failure of assert property( disable iff
(rst) a |-> not p). 
It would allow using the current inference of condition into the cover
property to be the same as for assert property, i.e., condition ##0 a
|-> b, and yet report only non-vacuous and not disabled coverage.
Disabled is reported as not covered. 
(If there is no explicit implication, e.g., cover property (disable
iff(rst) p), the cover is that of the failures of assert property(
disable iff (rst) 1'b1 |-> not p). )

- cover property action block executes only covered non-vacuously and
not disabled. Probably we do not need any system task to enable
execution when disabled or when vacuous, but there is no immediately
visible obstacle to allow such tasks like for the assert statements.

The changes to existing tools are thus limited to the addition of tasks
that control the action blocks in assert/cover statements, and default
reporting and pass action block execution only on non-vacuous,
non-disabled assert and cover statements.

We also recommend that the LRM does not require reporting on the number
of attempts for every assert / cover statement, because this imposes
unnecessary overhead. In all cases, the number of attempts is the number
of clock ticks and it is the same for all assertions running on the same
clock. This could be reported by the tools in a separate category or the
user could write a separate cover property just to count the ticks (or
detect whether the clock was dead).

Finally, as discussed among several members of sv-ac, we should
distinguish the two forms of cover statement that currently exist under
the same statement, namely, to have separate "cover property" and "cover
sequence" statements. It does not introduce any new keywords and makes
the intent clear.


Best regards,

ed&surrendra