RE: [sv-ac] disabling action blocks for vacuous and disabled attempt

Hi,

The feedback I have got so far from users is that pass action block in
assertions is useless because it gets executed for vacuous successes. I
believe it will be very rare case that someone wants to enable execution
of pass actions for vacuous/disable success. That is why I prefer if we
make the default as non-execution of pass action block. I understand
that this is not backward compatible.

Another question which came to my mind about execution of pass action on
disabled success is: Does the pass action block get executed at every
clock edge the property remains disabled or it happens only when reset
condition becomes true ? 

Thanks.
Manisha

-----Original Message-----
From: owner-sv-ac@eda.org [mailto:owner-sv-ac@eda.org] On Behalf Of John
Havlicek
Sent: Tuesday, January 31, 2006 6:24 AM
To: krolnik@lsil.com
Cc: sv-ac@eda.org
Subject: Re: [sv-ac] disabling action blocks for vacuous and disabled
attempt

Hi Adam:

The transformation you refer to can be difficult.

We are talking about partitioning the possible dispositions of assertion
attempts into "success", "failure", and "disabled".
The "success" set can be further partitioned into "vacuous success"
and "non-vacuous success".

The question still open is for which dispositions the action blocks
should execute.  The users I have worked with do not want the "pass" 
action block to execute for an attempt that is "disabled" or that is a
"vacuous success".

Best regards,

John H.

> 
> Hi All;
> 
> For verilog users, the disable statement (from which the disable iff 
> was
> modeled) discontinues execution of
> said block.  Given this initial understanding, it would follow that 
> the 'disable iff' statement would perform a similar operation for the 
> covered properties.
> 
> I have seen disable clauses used for reset sequences, thus given this 
> and the above model, it would be consistent to allow the property to 
> terminate without a success.
> 
> If this solution is chosen, is it not possible for a property to be 
> transformed by removal of the disable clause and adding the expression

> to the consequent of the property to obtain the other solution 
> proposed - success due to a disable expressions returning true?
> 
>    Thanks.
> 
> -- 
>     Adam Krolnik
>     ZSP Verification Mgr.
>     LSI Logic Corp.
>     Plano TX. 75074
>     Co-author "Assertion-Based Design"
>