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

Hello Vinaya,

my subjective opinion, please see below.

ed
 

> -----Original Message-----
> From: Vinaya Singh [mailto:vinaya@cadence.com] 
> Sent: Saturday, March 18, 2006 12:37 AM
> To: Kulshrestha, Manisha; Eduard Cerny; sv-ac@eda.org
> Subject: RE: [sv-ac] SV-AC: on cover property, disable if and 
> reporting... 
> 
> 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?

Yes in the case of a not, it is a failure (not distinguished) Ususally
if you use a "not" in a property, it does not contain an implication (at
least I have not seen a useful situation like that.)

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

The diff between cover property and cover sequence is the same as
defined in the LRM, the change is that it is also reflected in the
verification statement directives. Cover property = first match only,
cover sequence all matches.

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

If for a given attempt S1 |-> S2 is a non-vacuous non-disabled success,
I do not see how, for the same attempt (start clock tick) S1  ##0 S2
could have failure. Please explain.


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