RE: [sv-ac] Porposal assertion action control tasks

Hello,

I agree with Manisha on her interpretation of the effect of disable iff.

Regarding the vacuity in the presence of chains of implications, we
could perhaps derive it by rewriting the chain into concatenations
except for the last implication. I.e., (si is a sequence)
s1 |-> s2 |-> ... |-> sn |-> p 
is equivalent to
s1 ##0 s2 ##0 ... ##0 sn |-> p   (similarly for |=>, with ##1
replacement)

In other words, if the concatenation s1 ##0 s2 ##0 ... ## sn does not
match in the attempt, the success of the attempt is vacuous.
Defining vacuity once the attempt reaches successfully into p is another
matter (assuming that all leading implications are taken out in front)
and I do not think that we should attempt to put anything in the LRM for
that case.

ed
 

> -----Original Message-----
> From: owner-sv-ac@eda.org [mailto:owner-sv-ac@eda.org] On 
> Behalf Of Kulshrestha, Manisha
> Sent: Wednesday, February 22, 2006 11:56 AM
> To: Korchemny, Dmitry; sv-ac@eda.org
> Subject: RE: [sv-ac] Porposal assertion action control tasks
> 
> Hi Dimitry,
> 
> The answer to question (2) is 'no'. 
> 
> As per LRM: "The disable iff clause allows preemptive
> resets to be specified. For an evaluation of the 
> property_spec, there is
> an evaluation of the underlying
> property_expr. If prior to the completion of that evaluation the reset
> expression becomes true, then the overall
> evaluation of the property_spec is true."
> 
> So, in this case 'rst' will be checked before 'a' and the 
> property will
> have a disabled success. Since $assertdisableoff has been called for
> this scope, the pass action 'action1' will not execute. 
> 
> I also agree that we need more clear definition of vacuous success.
> Specially in the cases of multiple implication operators and also when
> implication is used along with other operators (and, or etc.).
> 
> Thanks.
> Manisha
> 
> -----Original Message-----
> From: Korchemny, Dmitry [mailto:dmitry.korchemny@intel.com] 
> Sent: Wednesday, February 22, 2006 1:46 AM
> To: Kulshrestha, Manisha; sv-ac@eda.org
> Subject: RE: [sv-ac] Porposal assertion action control tasks
> 
> Hi Manisha,
> 
> Here are my comments:
> 
> 1) To define the action of $asservacuouson/of for assertions we need
> first a clear definition of vacuous success of an assertion.
> 
> 2) $assertdisabledon/off for assertions. Let's have the following
> property:
> 
> assert property (disable iff(rst) a) action1 else action2;
> 
> Suppose both rst and a are high and $assertdisableoff has been issued.
> Will action1 still take place?
> 
> 3) cover statement. As I wrote in my previous mail, the definition of
> cover statement itself needs a refinement. In my proposal the 
> notions of
> vacuous and disabled success for cover directives are irrelevant.
> 
> 4) I definitely think that this is another errata item (if you are
> talking about #805)
> 
> Thanks,
> Dmitry
> 
> 
> -----Original Message-----
> From: owner-sv-ac@eda.org [mailto:owner-sv-ac@eda.org] On Behalf Of
> Kulshrestha, Manisha
> Sent: Tuesday, February 21, 2006 7:25 PM
> To: sv-ac@eda.org
> Subject: RE: [sv-ac] Porposal assertion action control tasks
> 
> Hi All,
> 
> I am including a proposal for controlling action block 
> execution. Please
> send your feedback. Do we need another errata on this issue or this
> proposal can be added to the errata on disable iff (which already has
> another proposal).
> 
> Thanks.
> Manisha
> 
>