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