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"
>