Re: [sv-ac] Issue 805

I suggest that the definition of the semantic of coverage goal be as 
follows:

Let 'w' be a computation, and P be a property, then w satisfies cover 
property (P)
iff for some 0 <= i < |w|, we have that w^{i..}, {} |= P.

Where the |= relation is the one defined in appendix E.3.5.

I agree that sometime people mistakenly write cover properties of the 
form R |-> P, when
they want to identify a match of R followed by a satisfaction of P. This 
should be written
as "not (R |-> not P)". I suggest that we will defined a derived 
operator "followed_by"
(similar to forespec) such that "R followed_by P" is equivalent to "not 
(R |-> not P)". This
will enable a more intuitive form of writing cover properties.

Doron

Korchemny, Dmitry wrote:

> Hi all,
>
> I would like to understand what the request incentive is: a need in 
> proper /cover/ statement semantics definition or a need to collect a 
> richer statistics – how many times the reset signal rose. I don’t have 
> anything against reporting reset statistics, except for minor comments 
> given below, but I guess that the main point of the enhancement 
> request is the statement semantics and this request is aimed to 
> disable pathological coverage reporting. Therefore I would like to 
> address mainly the latter issue.
>
> The semantics of the /cover/ statement is not defined anywhere in the 
> LRM, and there are only several words about property coverage 
> collection in the dynamic simulation environment. We need to define a 
> formal semantics for /cover/ statement both to avoid ambiguity in the 
> LRM interpretation, to be confident that the coverage concept is 
> always meaningful and to allow cover statement usage by formal 
> analysis tools.
>
> The informal semantics of the /assert/ statement is to make sure that 
> the property is (*always*) correct. When the property is violated then 
> the counter-example is either generated by formal analysis tools or is 
> provided as a simulation trace fragment by dynamic simulation tools. 
> The informal semantics if the /cover/ statement is to make sure that 
> the property is feasible, i.e., it *may be* correct, and the tools 
> should provide witness for it: the formal analysis tools should 
> generate such a witness, while dynamic simulation tools should provide 
> a trace fragment along with the collected statistics.
>
> Let’s try to define the /cover/ statement semantics formally. I will 
> be using in the sequel the following LTL pseudo-code:
>
>     * globally says that the property is checked each clock phase
>     * eventually means some time in the future
>
> and will assume all clock events to be fair. I also assume in all 
> below examples that the assertions are written outside of an initial 
> block, i.e., implicit /always/ semantics is applicable to them.
>
> The first attempt would be to define /cover/ /property/ as /assert/ of 
> its negation. Then the assertion counter-example is a coverage 
> witness. But this straightforward definition won’t reflect our 
> intention. Consider the simplest cover statement:
>
> (always) cover property (@(clk) a); // a is a Boolean expression
>
> Its pseudo code notation is:
>
> cover property (@(clk) globally a);
>
> After negation we get:
>
> assert property (@(clk) eventually !a);
>
> I.e., the property is covered if a never holds, this is apparently not 
> our intention: the property is covered when a eventually holds.
>
> Here is the second take:
>
> cover property (@(clk) globally p) succeeds iff assert property 
> (@(clk) globally not p)) fails
>
> In the case when p is a Boolean expression, or even a sequence this 
> definition works: if at some moment p is high (or the sequence is 
> matched), the property is covered.
>
> But in the common case, when p is a property, the problem persists:
>
> cover property ((@clk) globally a |=> b) succeeds iff? assert property 
> ((clk) globally a ##1 !b); fails
>
> Has the property been covered if a never happens? According to LRM it 
> has, but it has been covered vacuously for the antecedent never 
> happens. This definition of coverage is problematic: e.g., it is 
> always recommended to avoid writing such /cover/ properties. More than 
> that, this LRM definition of coverage is contradictory. The section 
> 17.13.5 “Embedding concurrent assertions in procedural code”: reads
>
> Another inference made from the context is the enabling condition for 
> a property. Such derivation takes place when a property is placed in 
> an if...else block or a case block. The enabling condition assumed
>
> from the context is used as the antecedent of the property.
>
> *property *r3;
>
> @(*posedge *mclk)(q != d);
>
> *endproperty*
>
> * *
>
> *always *@(*posedge *mclk) *begin*
>
> *if *(a) *begin*
>
> q <= d1;
>
> r3_p: *assert property *(r3);
>
> *end*
>
> *end*
>
> The above example is equivalent to the following:
>
> *property *r3;
>
> @(*posedge *mclk)a |-> (q != d);
>
> *endproperty*
>
> r3_p: *assert property *(r3);
>
> *always *@(*posedge *mclk) *begin*
>
> *if *(a) *begin*
>
> q <= d1;
>
> *end*
>
> *end*
>
> According to this definition if we substitute in the above examples 
> /assert/ with /cover/, our property will be covered (even though 
> vacuously) if a never happened! Such definition of coverage is 
> somewhat counter-intuitive.
>
> Therefore, it seems to me that the acceptable definition of the 
> /cover/ statement semantics would be:
>
> cover property ((@clk) globally disable iff (rst) s |-> p)) succeeds 
> iff assert property ((@clk) globally disable iff (rst) s |-> *not* p)) 
> fails
>
> or in pure SVA:
>
> cover property ((@clk) disable iff (rst) s |-> p)) succeeds iff assert 
> property ((@clk) disable iff (rst) s |-> *not* p)) fails
>
> Such semantics solves also the reset problem: when the reset 
> expression is true, the assertion cannot fail, and therefore the 
> original property cannot be covered. Therefore it looks to me that the 
> reset being high is not a coverage event, and should not be reported 
> as such.
>
> Below is the summary.
>
> Suggestion:
>
> ========
>
> I suggest defining the /cover property/ semantics as:
>
> cover property ((@clk) disable iff (rst) s |-> p)) succeeds iff assert 
> property ((@clk) disable iff (rst) s |-> *not* p)) fails
>
> The /cover /statement reports coverage when the corresponding 
> assertion fails for any property of the form s|->p, where s is a 
> sequence and p is a property. The formal definition is:
>
> For the property of the form A |-> B (when A |=> B is considered to be 
> A|-> ##1 B)
>
> cover property ((@clk) disable iff (rst) A |-> B)) succeeds iff assert 
> property ((@clk) disable iff (rst) A |-> *not* B)) fails
>
> Otherwise
>
> cover property ((@clk) disable iff (rst) B)) succeeds iff assert 
> property ((@clk) disable iff (rst) *not* B)) fails
>
> If the /cover/ statement is located inside a conditional statement, 
> the inferred condition is automatically taken into account. E.g.,
>
> If a property
>
> cover property (a); has an inferred enabling condition en, the equivalence
>
> cover property (a) succeeds iff assert property(not a) fails is still 
> valid, since both statements are actually
>
> cover property (en |-> a) succeeds iff assert property(en |-> not a) fails
>
> Discussion:
>
> ========
>
>    1. I suggest adding a specification of /cover/ statement for formal
>       analysis tools: a /cover/ statement is equivalent to a
>       corresponding /assert/ statement, but the generated
>       counter-example should be called witness and the tool should
>       report success. If the corresponding assertion passes, the tool
>       should report the coverage failure.
>    2. The coverage action statement should be executed each time the
>       property is covered (like else in the assertion). According to
>       the proposed definition the action statement won’t execute when
>       reset is high or a triggering condition was not met.
>    3. “Number of times succeeded” means the number of times the dual
>       assertion fails
>    4. “Number of times the property failed” is not quite clear. Does
>       it mean that /cover property(p)/ fails when /assert property
>       (p)/ fails?
>    5. “Number of times succeeded because of vacuity” is no longer
>       valid. The accurate statement would be number of times triggered
>       (I would even say attempted, but it probably has another
>       meaning). Should we report this number when the antecedent is
>       trivial (always true)?
>    6. The definition of sequence coverage should be refined (if it is
>       needed at all). Do we have a case of sequence coverage when B is
>       a sequence (in the above definition)? But in this case the
>       number of times triggered is still relevant.
>    7. “Number of time matched” for sequences is not clear – does it
>       coincide with the number of times succeeded? (see previous item)
>    8. If wanted, the information about reset signal can also be
>       collected (this is the actual content of #805), but instead of
>       “Number of times succeeded because of disabling” it should be
>       something like “Number of times the reset rose”
>    9. All stated above is applicable to the corresponding vpi calls as
>       well.
>   10. The case of a cover property inside an initial block is
>       syntactically identical. Semantic difference is that the
>       implicit /globally/ operator should be dropped in both /assert/
>       and /cover/ statements.
>   11. Completely different observation: adding more and more
>       requirements to the data to be collected will negatively affect
>       the simulation performance, and the standard should give the
>       user means to control the reporting level.
>
> General Disclaimer:
>
> ==============
>
> Since I don’t always have enough time to collect the feedback from 
> other Intel people, my position in some cases may change when this 
> feedback becomes available. I won’t add this disclaimer to my 
> subsequent messages, but it always remains valid.
>
> Thanks,
>
> Dmitry
>