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

Richard,

UCIS has become a flexible standard giving it a better chance for success. However we still should encourage anyone defining new coverage to do it in a consistent fashion.

I agree with you second point.

Regards
Hillel

From: Ho, Richard [mailto:Richard.Ho@DEShawResearch.com]
Sent: Tuesday, March 27, 2012 3:28 PM
To: Miller Hillel-R53776; Dana Fisman Ofek; 'hdlcohen@gmail.com'; 'sv-ac@eda-stds.org'
Cc: ucis@lists.accellera.org; Ho, Richard
Subject: RE: [sv-ac] SVA: Issue with coverage // need for a "full_paths" coverage?

From a UCIS perspective, we’ve made progress by acknowledging that the semantics of coverage are not well defined for many metrics. We have focused our efforts on a unified data model and exchange mechanism. We expect that for many of the well-defined coverage metrics, the semantics will align well between implementations. But we have stalled whenever we try to “force” an agreement on semantics where significant differences exist in implementations.

For the idea of a “full paths” notion of coverage -- this bears similarities to our discussion on expression/conditional coverage (some would say that it is the same discussion). I think that some ideas can be crafted in committees, while others are best prototyped by the user community and then brought to committee for standardization. The argument about what coverage is necessary in an expression or sequence should be first hashed out in the community with prototyping help from vendors if necessary before we try to solve it in committee I think. We need to be cognizant of the limited bandwidth available to our standards committees and try to be efficient with it.

Best,
Richard

From: ucis@lists.accellera.org [mailto:ucis@lists.accellera.org] On Behalf Of Miller Hillel-R53776
Sent: Thursday, March 22, 2012 6:08 AM
To: Dana Fisman Ofek; 'hdlcohen@gmail.com'; 'sv-ac@eda-stds.org'
Cc: Miller Hillel-R53776; ucis@lists.accellera.org
Subject: [Accellera:ucis] RE: [sv-ac] SVA: Issue with coverage // need for a "full_paths" coverage?

Dana,

I believe that for coverage we can take a different approach.


1. Code coverage goal selection has typically been ad-hoc in the worst case and algorithmic in the best case. There is no semantic driven definition. Saying that we still have good success with code coverage tools. Since there is not a strong need for a correctness requirement, we can compromise and be loose. This is very different to defining the semantics of correctness. For example, in case of disagreement we can select as a goal “all of the above”. We can see SVA coverage as an additional extension to code coverage.

2. Accellera UCIS committee are in a constant battle to align coverage definitions, we don’t need to give them more work. They are very well on their way solving some of the alignment with the existing adhoc/algorithmic code coverage. I added them if they would like to give feedback.

Regards
Hillel

From: Dana Fisman Ofek [mailto:Dana.Fisman@synopsys.com]
Sent: Wednesday, March 21, 2012 6:37 PM
To: Miller Hillel-R53776; 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?

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