[sv-ac] coverage

From: Doron Bustan <dbustan_at_.....>
Date: Thu Mar 23 2006 - 06:49:24 PST
It seems that we need to decide on the items below before a cover
proposal could be written.  Once we decide on these item, defining the
coverage semantic should not be hard.  Because of the interdependencies,
it is difficult to write independent proposals for each item.

1. Add a new operator "reject on" (or some other syntax) as the dual
   of "disable iff".  Here are some alternatives.
   a. Overload the "disable iff" so it behaves as 
      before in an "assert property" or an "assume property", but
      behaves as "reject on" in a "cover property".
   b. Add two new dual operators, "reject on" and "accept on".
      "accept on" behaves like "disable iff" in an "assert property"
      or an "assume property".
   c. Both a. and b.
      
2. Whether or not to add new operators "followed by", "followed nexttime by"
   (some syntax "x-y", "x=y" with suitable characters "x" and "y" might work) 
   as the duals of |-> and |=>.

3. Whether or not vacuity should be defined for coverage.

4. Whether or not disabled or rejected cover attempts should be defined/reported 
   for coverage.

5. Whether or not to add a new directive "cover sequence".

Did we forgot some thing?

Our opinions:

1. We should pick alternative c.  We can keep "disable iff" as a top-level
   operator only, so the overloading is not confusing.  "accept on" and 
   "reject on" can be made general operators now or in the future.

2. We should add the duals of |-> and |=>.

3. Vacuity should not be defined for coverage.

4. Disabled or rejected attempts should not be reported in coverage.

5. We should add the cover sequence directive

DB & JH
Received on Thu Mar 23 06:49:28 2006

This archive was generated by hypermail 2.1.8 : Thu Mar 23 2006 - 06:49:51 PST