[sv-ac] vacuity in coverage

All,

I think the "vacuous cover hit" = "bad coding". Thus we should not 
define/use vacuity
for cover properties. Let me try to explain myself

There are a lot of definitions for vacuity, the way I see it is that 
vacuity is a way
to extract cover goals from assertions. The main purpose of assertions 
is to define
the right behavior for a design. Thus, the semantics, which defines an 
omega-regular
language for every assertion, defines the language of all "legal" 
computations.

As a by-product, the vacuity concept enables the extractions of coverage 
goals.
The idea is that when a user write an assertions, she intend every part 
of the
assertions to be evaluated on some computation of the design. Furthermore,
every part of the assertion should "influence" the evaluation of the 
property
on some computation. The vacuity coverage goal is to find such a 
computation.

In the vacuity defined in the LRM, an extracted cover property "R"
is being extracted from assertion of the form "R |-> P$. The cover
property "R" describes a necessary path to the evaluation of "P".
When an assertion does not pass non-vacuously in any computation,
it is usually means (like in any coverage hole) that there is something
wrong in either the design, the testbench, or the assertion.

Note that the extracted coverage goal, depends on the coding style of 
the designer.
For example the following three properties are semantically equivalent.

1. a ##1 a |-> b .
2. a |-> (!a or a ##1 b)
3. !a or (a ##1 !a) or (a ##1 a ##1 b)

In the first, form the coverage goal 'a ##1 a' is extracted, in the 
second the coverage
goal 'a' is extracted and in the third, no coverage goal is extracted.

Thus, vacuity testing is a (useful) by-product of the assertions, which 
extract coverage goals.

On the other hand, the main purpose of cover properties is to define
a behavior that should happen in the design. Thus, the semantics, which 
defines an omega-regular
language for every cover property, defines the language of all "desired" 
computations.
Since coverage is the main goal, I don't see any point of using a mechanism
like vacuity to redefine the coverage goals. Why using a by-product that 
is less expressive
and depends on user coding style, when we have the real thing?

On a practical note, I believe that once we add "followed_by" as a 
derived operator, writing
"good code" that does not need the vacuity tweak, is as easy to come 
with as "bad code".


Doron