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

Hi All,

My comments are included.

Thanks.
Manisha


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.

MK: I agree and I have already mentioned this previously.

In the following we outline a possible solution:

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

MK: I support this.

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

MK: agree

- 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.

MK: I like the idea of no default execution of success action statement
for vacuous success. Now that we are saying that disabled is not a
success, I do not think it is needed to provide the task call
assertdisableon to enable execution of pass statement. Are you
suggesting this for backward compatibility ?

- 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.

MK: I think we only need covered (no need for covered vacuously and
covered disabled). Probably tools can choose to report more than what
LRM requires if the users demand that information.

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). )

MK: I agree that cover property should only report non-vacuous
non-disabled coverage.



- 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.

MK: agree. I would prefer to avoid any system tasks as there is no real
need for them.

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).

MK: agree.

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.

MK: that will definitely make it easier to distinguish them.


Best regards,

ed&surrendra