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

Dana,
I like your idea of a *strong cover. *However, I see your point. My goal
was to make it is easier for the author of those assertions. Take the case
where I have 100 assertion statements, and many of those have several
sub-sequences with the *and* or *or *operator, then if I were interested in
seeing that all of these sub-sequences were covered, I would need to dig
into these assertion statements and start to split them and use the *cover
sequence* statement.
If fact, if I had a preference, I would rather not even be forced to write
all these cover statements, and have some tool command that informs the
tool that for all the assertions I would like a *strong cover* of all the
sub-sequences that are ANDed or ORed.
Another alternative, would be for a script that does this splitting and the
creation of a file with the *strong cover* of all the sub-sequences that
are ANDed or ORed.
Bottom line, maybe this should be a "tool" issue rather than a "language
issue"
Thanks,
Ben Cohen

On Wed, Mar 21, 2012 at 2:35 PM, Dana Fisman Ofek
<Dana.Fisman@synopsys.com>wrote:

> Hi Ben,****
>
> ** **
>
> My view is that you are putting too much into the notion of cover. A
> property either holds or does not hold on a given set of traces. And a
> cover of a property is defined to hold if the property holds on one of the
> given traces. So indeed it may hold vacuously. In PSL the argument of cover
> is a sequence not a property. So it passes if there is a match to that
> sequences. So there would be no antecedent vacuity for a PSL cover. Though,
> similarly, if an OR is used in the sequence it might be that only one
> operands of OR is covered.****
>
> ** **
>
> I think that if one is interested in seeing both operands of OR covered it
> should divide that into two covers. Putting them in one says “I want to see
> that this scenario is covered, while I don’t particularly care in which way
> (operand of OR) it is”. ****
>
> ** **
>
> One could try to define a notion of *strong cover *which tries exercises
> all ways to satisfy the formula and cover all of those, but I think we will
> fall into the same areas of disagreement as there are in vacuity. For
> instance, in p until q, would you require p to hold at least once? Would
> you demand q to hold at the end? (Note that the property uses the weak
> until so q need not occur at the end, and one could choose s_untilinstead. Still you can describe same property as (always
> p) or ( p s_until q ) in which case if you favor going over all operands
> of OR you should require to demand to see q as well).****
>
> ** **
>
> Bottom line, I think this would be hard to define, and this can be solved
> by splitting the property into several if you care for each is separately.
> ****
>
> ** **
>
> Best,****
>
> Dana****
>
> ****
>
> ** **
>
> *From:* owner-sv-ac@eda.org [mailto:owner-sv-ac@eda.org] *On Behalf Of *Miller
> Hillel-R53776
> *Sent:* Wednesday, March 21, 2012 5:08 PM
> *To:* 'hdlcohen@gmail.com'; 'sv-ac@eda-stds.org'
> *Subject:* Re: [sv-ac] SVA: Issue with coverage // need for a
> "full_paths" coverage?****
>
> ** **
>
> You would need the same for and if one of sides always passed vacuously
> ****
>
> *From*: Ben Cohen [mailto:hdlcohen@gmail.com]
> *Sent*: Wednesday, March 21, 2012 03:46 PM
> *To*: sv-ac@eda-stds.org <sv-ac@eda-stds.org>
> *Subject*: [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* <http://www.mailscanner.info/>, and is
> believed to be clean.
> --
> This message has been scanned for viruses and
> dangerous content by *MailScanner* <http://www.mailscanner.info/>, and is
> believed to be clean. ****
>

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