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

Hi Hillel,

I see the value of having things defined by the committee, rather than having each tool interpret things slightly differently.

However, I don’t think it is a good idea to put in the standards things which are not well defined. As mentioned below a notion for strong cover would suffer the same problems as the notion of vacuity does. There is a lot of debate on vacuity defs and which constitutes an interesting vacuity, and which is just a burden to the user. Doesn’t seems like the debate is going to ever end… I believe with strong cover we’ll run into the same issues.

Best,
Dana

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

I believe Ben’s goal is to make things easier for the user. I also believe that we can leave this to the tool vendor to implement. However that would lead to inconsistencies. Better the committee do their best in defining it upfront for the simple cases to avoid inconsistencies coming from multiple vendors in the future..
Regards

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

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] 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.