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.

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

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


Thanks

Doron