RE: [sv-ac] Issue 805

Doron,

OK, I see your point. I was sure that the coverage was intended to
monitor the events which have actually happen, and not to register the
events which never happened, as in your examples. E.g., you can claim
that the queue was never empty if before the end of the simulation you
have never seen it empty. If we have to take these scenarios into
account then we do need followed_by and need to distinguish it from |->.
I should modify my proposal accordingly.

We still have to address the following issues:
* either to define disable_iff behavior for coverage or (better) to
introduce a dual operator reject_on
* find an appropriate solution for the inferred enabler in cover
property.

Thanks,
Dmitry

-----Original Message-----
From: Doron Bustan [mailto:dbustan@freescale.com] 
Sent: Tuesday, March 14, 2006 6:24 PM
To: Korchemny, Dmitry
Cc: sv-ac@eda.org
Subject: Re: [sv-ac] Issue 805

Dimitry,

I am still learning your comments, but just a general clarification.

I don't suggest to restrict the use of implication in cover properties,
nor
the use of followed_by in assertions. All I am saying is that in many
cases
when people write a cover property of the form "R|->P", they really mean
"R followed_by P", and thus this operator should be available.

I can imagine people using |-> in cover properties in cases like :

cover property (1[*:$] |-> !empty), which identifies computations where 
the queue is never empty.

cover property (
    1[*:$] followed_by
    1[*:$] |-> !empty
),

which identifies computations where  from some point
queue is never empty.

cover property
(
send ##1
!ack [*1:$] ##0 fail
followed_by
(
   1[*1:$] ##0 resend
    |=>
   !ack [*1:$] ##0 fail
)
),
which identify a message which fail in the first send and then in every 
resend.

Thanks

Doron

Korchemny, Dmitry wrote:

>Hi Doron,
>
>Please, see my comments below.
>
>Thanks,
>Dmitry
>
>-----Original Message-----
>From: owner-sv-ac@eda.org [mailto:owner-sv-ac@eda.org] On Behalf Of
>Doron Bustan
>Sent: Tuesday, March 14, 2006 4:19 PM
>To: Korchemny, Dmitry
>Cc: sv-ac@eda.org
>Subject: Re: [sv-ac] Issue 805
>
>Hi Dmitry,
>
>
>  
>
>>* 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
>>
>>    
>>
>
>I see your point, but you could say the same about using sequences in 
>assertions
>(without implications) and we don't try to forbid that. We assume that 
>people
>will use the language correctly.  The followed_by allows to use an 
>enabling condition.
>
>---
>D.K. The pure sequences in assertions are meaningful. E.g., assert
>property (##[1:$] b) - = eventually b.
>
>Implications in the coverage statement become absolutely meaningless,
>and in your suggestion they should be forbidden in the language. What
>bothers me is the case
>
>if (en) cover property (a); which is implicitly rewritten as cover
>property (en |-> a); Therefore you should either provide a different
>meaning for if (en) cover property (a) (i.e., cover property (en
>followed_by a)) or you should cope with the implications somehow.
>---
>
>  
>
>>* The reset condition handling is still problematic
>>
>>    
>>
>
>I agree, I think that we need the dual of disable iff in the language 
>(similar to ForSpec's reject).
>The problem is that we cannot define it as a derived operator because 
>currently disable iff
>has to be the top operator.
>
>---
>D.K. 
>
>We can define it as a primary operator. There should be no problem with
>this.
>---
>
>  
>
>>* 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)
>>
>>    
>>
>If I understand correctly, checking followed_by in cover property
should
>
>be the same as checking |->
>in assertions, am I missing something?
>
>Can you explain the LTL's operators issue? I don't understand that.
>
>---
>D.K.
>
>I am saying that the people will start writing assertions like:
>
>assert property (a ##1 b followed_by !g[*1:$] |-> f);
>
>and the tools will have to simulate this correctly.
>
>As for the LTL operators, I am saying that followed_by is useful when
>you want to write sequence followed_by property. If you want to write
>sequence1 followed_by sequence2, you can write sequence1 ##0 sequence2
>instead. In SVA the only properties that are not sequences are
>implications, sequence negations and implication negations. We want to
>enforce the usage of the followed_by in coverage only, where the only
>meaningful scenario is sequence1 followed_by sequence2, which does not
>require the introduction of followed_by.
>
>From the other hand, we usually want to count the number of the
attempts
>for the coverage. Without explicitly specifying the triggering
>conditions this information is completely lost.
>
>Consider the following example:
>cover property (a && b ##1 c ##0 d);
>
>If it written in this style what is its triggering condition: a, a &&
b,
>a && b ##1 c or none?
>
>--- 
>
>Thanks
>
>Doron
>
>  
>