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
>>>
>>>      
>>>
>
>  
>