RE: [sv-ac] Issue 805

 Hello,

I agree that disable iff for covers could be defined as a primary.

For the example of using followed_by

	assert property (a ##1 b followed_by !g[*1:$] |-> f);

yes, the user may not know what exactly it means, but perhaps some
methodology and linting would help here. It is already possible to write
assert property (not (a ##1 b |-> not( !g[*1:$] |-> f)));

which is the same thing. Correct?

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 9:57 AM
> To: Doron Bustan
> Cc: sv-ac@eda.org
> Subject: RE: [sv-ac] Issue 805
> 
> 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
> 
>