RE: [sv-ac] Issue 805

Hi Ed,

Probably I was not clear enough, but I meant that in *** the most
interesting cases *** in SVA it may be replaced by sequence fusion
(##0). Sure you cannot always use the sequence fusion for that. But the
only interesting scenario for the coverage is the sequence fusion,
therefore I am saying that there is no need for followed_by if we are
talking about coverage only.

Thanks,
Dmitry

-----Original Message-----
From: Eduard Cerny [mailto:Eduard.Cerny@synopsys.com] 
Sent: Tuesday, March 14, 2006 3:22 PM
To: Korchemny, Dmitry; Doron Bustan
Cc: sv-ac@eda.org
Subject: RE: [sv-ac] Issue 805

Hello Doron, Dmitry,

I agree with Doron, followed_by as the dual of |-> is needed, because
##0 cannot be used with property on the RHS. 
If a cover property is under a condition it shouuld be converted to
followed by rather than |->, where the condition is on the LHS. 
I do not see much of a problem implementing followed_by.  
Should there be two forms, one overlapping and one non-overlapping?

ed


> -----Original Message-----
> From: owner-sv-ac@eda.org [mailto:owner-sv-ac@eda.org] On 
> Behalf Of Korchemny, Dmitry
> Sent: Tuesday, March 14, 2006 8:14 AM
> To: Doron Bustan
> Cc: sv-ac@eda.org
> Subject: 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
> >
> 
>