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

Hi Hillel,

Ø In FSL we took assertion coverage above and beyond, there is a lot to do in this area.

Can you share some pointers for this?

Thanks,
Dana

From: Miller Hillel-R53776 [mailto:r53776@freescale.com]
Sent: Wednesday, March 21, 2012 5:57 PM
To: hdlcohen@gmail.com; Dana Fisman Ofek
Cc: sv-ac@eda-stds.org
Subject: RE: [sv-ac] SVA: Issue with coverage // need for a "full_paths" coverage?

Ben,

Tool is the easy way out. This would lead to inconsistencies between vendors. Better to make first attempt on the sv-ac.

In FSL we took assertion coverage above and beyond, there is a lot to do in this area.

Thanks
Hillel

From: Ben Cohen [mailto:hdlcohen@gmail.com]
Sent: Wednesday, March 21, 2012 4:50 PM
To: Dana Fisman Ofek
Cc: Miller Hillel-R53776; sv-ac@eda-stds.org
Subject: 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<mailto: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_until instead. 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> [mailto: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<mailto:hdlcohen@gmail.com>'; 'sv-ac@eda-stds.org<mailto: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<mailto:hdlcohen@gmail.com>]
Sent: Wednesday, March 21, 2012 03:46 PM
To: sv-ac@eda-stds.org<mailto:sv-ac@eda-stds.org> <sv-ac@eda-stds.org<mailto: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.