RE: [sv-ac] Issue 805

Hi Dmitry,

my point is that followed_by already existis if you write not(s |-> not
p) and followed_by would just make it clearer. I think it is useful to
have and I would prefer that inferred conditions for covers be done
using followed by, but I can see the issue with having a;ready an
implication in the cover (as you last example showed). I generally
discourage people from using implications in cover statements, but...

ed
 

> -----Original Message-----
> From: Korchemny, Dmitry [mailto:dmitry.korchemny@intel.com] 
> Sent: Tuesday, March 14, 2006 10:01 AM
> To: Eduard Cerny; Doron Bustan
> Cc: sv-ac@eda.org
> Subject: 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
> > >
> > 
> > 
>