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

Hello Vinaya,

I am not convinced that restricting the use of not on implications is
good. For example,
not (s1 |-> not s2) is a useful operator, s1 followed_by s2. 

ed


> -----Original Message-----
> From: owner-sv-ac@eda.org [mailto:owner-sv-ac@eda.org] On 
> Behalf Of Vinaya Singh
> Sent: Tuesday, March 21, 2006 1:09 PM
> To: Doron Bustan
> Cc: Kulshrestha, Manisha; Eduard Cerny; sv-ac@eda.org
> Subject: 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
> >
> >
> >
> >
> >
> >
> > 
> >
> 
> 
> 
> 
> 
>