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

Thanks Doron and ED for you comments.
 
I did not get a coherent answer for Q1.
Should we allow 'not' on property which could have "vacuous success"? 
Since, it is not useful on properties, which could have "vacuous success", may
be we should have restriction in the LRM. 
For example, PSL simple subset has restriction on 'never' operator. 
 
Thanks,
-Vinaya
 

________________________________

From: Doron Bustan [mailto:dbustan@freescale.com]
Sent: Mon 3/20/2006 8:21 PM
To: Vinaya Singh
Cc: Kulshrestha, Manisha; Eduard Cerny; sv-ac@eda.org
Subject: Re: [sv-ac] SV-AC: on cover property, disable if and reporting...



Hi Vinaya,

here are my 2 cents

>Hello All,
>
>  I have couple of basic questions.
>
>Q1. What is complement of "vacuous success"? Is this "vacuous failure"? This is in
>        context of assertion operator "not". Is this a failure without any counter example?
>
>
I think that all failure are interesting and should be reported. In that
sense, there are no complimented vacuous successes.

>Q2. It is good that, you are distinguishing two forms of covers i.e. "cover property" and "cover sequence".
>       However if we drop "non-vacuous and non-disabled" coverage in the
>        property then what is the difference between the two.
>        Is "cover ( S1 |-> S2)" not same as "cover (S1 ##0 S2)".
>        Is "cover property" a convenience feature?
>
>
First,  "cover property ( S1 |-> S2)" and "cover property (S1 ##0 S2)"
are not equivalent.
consider the properties "P1 = a[*1:2] |-> b" and "P2 = a[1:2] ##0 b" and
a computation "w" where "a" holds in the first
two cycles, and b holds only at the first cycle. In this case "w" does
not satisfy "cover property (P1)" and "w" satisfies
"cover property (P2)".

More generally, I think once we define (redefine) the dual of "disable
iff", and use it in cover properties, all successes should be reported,
and there should not be a category of vacuous success for coverage.

>Q3. We can a situation when assertion (S1 |-> S2) is a "no-vacuous and non-disabled" success.
>       However "cover (S1 ##0 S2)" fails. I am considering truncated paths in S2 (cul-de-sac paths).
>      What does " cover (S1 |-> S2) mean, when all paths in S2 are  truncated?
>

For the neutral and strong semantics , the LRM defines it as a failure,
for the weak semantics, as a success. So, if a tool supports
strong/neutral/weak
semantics, the user should be able to choose what should it be.
I cannot think of an example where it makes sense to use a weak
semantics for a cover property,
but I didn't thought too much about it.

Doron

>
>Thanks,
>-Vinaya
>
> 
>
>________________________________
>
>From: owner-sv-ac@eda.org on behalf of Kulshrestha, Manisha
>Sent: Fri 3/17/2006 11:15 PM
>To: Eduard Cerny; sv-ac@eda.org
>Subject: 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
>
>
>
>
>
>
> 
>