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