RE: [sv-ac] Issue 805

Hi Doron,

I agree with your property coverage generalization with followed_by, but
I see several usability problems with this approach:
* Property coverage (A|->B) becomes meaningless. This is problematic
because the cover property statement may be located under a conditional
statement, and then it has an implicit enabling condition
* The reset condition handling is still problematic
* Using followed_by in assertions may be difficult for simulators, and
when introduced this operator should be supported everywhere. I think
that this operator should be introduced only in case if SVA is extended
with LTL operators (similarly to PSL). Otherwise its applicability is
questionable since in the most interesting cases in SVA it may be
replaced by sequence fusion (##0)

Therefore I am suggesting defining
cover property (disable iff(rst) A |-> B) as assert property (disable
iff A |-> not B) where the failures of the latter statement are
considered to be cover points of the former one.

See details in Mantis 1383.

Sorry for the late answer.
Dmitry  

-----Original Message-----
From: Doron Bustan [mailto:dbustan@freescale.com] 
Sent: Wednesday, March 01, 2006 12:45 AM
To: Korchemny, Dmitry
Cc: sv-ac@eda.org
Subject: 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
>