FW: [sv-ac] Issue 805. Correction

Instead of "never holds", should be "always holds".

 

Dmitry

 

________________________________

From: owner-sv-ac@eda.org [mailto:owner-sv-ac@eda.org] On Behalf Of
Korchemny, Dmitry
Sent: Thursday, February 09, 2006 6:20 PM
To: sv-ac@eda.org
Subject: [sv-ac] Issue 805

 

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