[sv-ac] SVA: Issue with coverage // need for a "full_paths" coverage?

Before I write a mantis, I would like to hear your comments on the
following issue.
If a property succeeds only with the LHS of an *or* in my testcases, there
could be a case where the RHS is false if it were exercised, but my
testcases have not exercised the RHS. My concern is the thoroughness of
the testcases. When I write coverage, how can I be assured that all
sequences or properties were covered?
If I have the following:
cover property(a |-> seq1 or seq2);
assert property(a |-> seq1 or seq2);
  I am not guaranteed that my testcases have covered both seq1 and seq2
even if the assertion is covered. This is because if seq1 succeeds,
coverage s true.
With vacuity in something like
cover property(a |-> (c |-> seq1) or (d->seq2)) ;
I have the same issue.
That puts a penalty on the writers of coverage code to have to split the
cover statements to the cover of sub-sequences or sub-properties.
It would be nice to have a qualifier that ensures that a successful
coverage means that all sub-sequences or sub-properties vere covered.
For example:
cover property(full_paths(a |-> seq1 or seq2));
cover property(full_paths(a |-> prop1 or prop2));
Ben Cohen

-- 
This message has been scanned for viruses and
dangerous content by MailScanner, and is
believed to be clean.