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.