I agree with Ed Doron Eduard Cerny wrote: >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 >>> >>> >>> >>> >>> >>> >>> >>> >>> >>> >> >> >> >> >> > > >Received on Tue Mar 21 10:47:44 2006
This archive was generated by hypermail 2.1.8 : Tue Mar 21 2006 - 10:47:57 PST