RE: [sv-ac] Issue 805

Agree...
ed
 

> -----Original Message-----
> From: Doron Bustan [mailto:dbustan@freescale.com] 
> Sent: Tuesday, March 14, 2006 10:31 AM
> To: Eduard Cerny; sv-ac@eda.org
> Subject: Re: [sv-ac] Issue 805
> 
> Hi Ed,
> 
> >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?
> >  
> >
> I guess we need both, on one hand I can imagine people wanting to fuse
> R and P, on the other hand, for multi-clocking we need the non fusing 
> version.
> 
> Doron
> 
> >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
> >>>
> >>>      
> >>>
> >
> >  
> >
> 
> 
>