RE: [sv-ac] cover in procedural context

Hi Joseph,

except that for covers, I believe that the inferred enabling condition
should be connected to the rest using followed_by and not by |->.

I think we need two forms of followed_by, one overlapping and one
non-overlapping. either we use a similar approach to define overlap as
in PSL, e.g., 
followed_by_  overlapping
followed_by   non-overlapping.

Or we define a new symbol, e.g., 
#-  overlapping
#= non-overlapping

ed


 

> -----Original Message-----
> From: owner-sv-ac@eda.org [mailto:owner-sv-ac@eda.org] On 
> Behalf Of Joseph Lu
> Sent: Tuesday, March 14, 2006 12:30 PM
> To: sv-ac@eda.org
> Subject: RE: [sv-ac] cover in procedural context
> 
> 
> Hi,
> 
>   I agree with John and Ed about providing enabling/qualification
> conditions to work with a cover property. The enabling/qualification
> should be apart from the the precondition of |->. We have been using
> this enabling condition to tell the tool when it should collect the
> coverage information on "cover property (a |-> b)"
> 
> Regards,
> 
> 
> Joseph 
> 
> 
> -----Original Message-----
> From: owner-sv-ac@eda.org [mailto:owner-sv-ac@eda.org] On 
> Behalf Of John
> Havlicek
> Sent: Tuesday, March 14, 2006 8:14 AM
> To: sv-ac@eda.org
> Subject: [sv-ac] cover in procedural context
> 
> All:
> 
> I like Ed's idea about defining enabling conditions
> to work as preconditions of followed_by for a cover property.
> 
> I'm not sure that there is clear language in the LRM
> today that says that the enabling condition behaves like
> the precondition of |-> for a cover property.
> 
> In Annex E, we said that for assert property, the enabling
> condition behaves like the precondition of |->.
> 
> I agree with Ed that we already have "followed_by" in
> the language.  I don't see the connection to the LTL operators.
> 
> I think that if people are writing implication properties,
> they intend them to be checked as correctness properties
> and they expect the tool also to collect coverage on how
> thoroughly the correctness properties have been exercised.
> 
> I think that it will be confusing for users to tell them 
> that when they write
> 
>   cover property (a |-> b)
> 
> they are getting the same thing as
> 
>   cover property (a ##0 b)
> 
> I agree with Dmitry that we still need to address the problem
> of disable iff for covers.
> 
> Best regards,
> 
> John H.
> 
> 
> 
>