RE: [sv-ac] Is result of disable iff (true_expression) vacuous or true success?

Hi Ben,

I agree with your suggestion, it should be a vacuous success.

ed
 

> -----Original Message-----
> From: owner-sv-ac@eda.org [mailto:owner-sv-ac@eda.org] On 
> Behalf Of vhdlcohen@aol.com
> Sent: Friday, August 19, 2005 12:20 AM
> To: sv-ac@eda.org
> Subject: [sv-ac] Is result of disable iff (true_expression) 
> vacuous or true success? 
> 
> IEEE P1800/D5 and SV 3.1a LRM 17.11 is unclear on this issue. LRM 
> states "If prior to the completion of that evaluation the reset 
> expression becomes true, then the overall evaluation of the 
> property_spec is true."
>   But a true evaluation can be considered as success, which is not 
> really the correct interpretation of a reset of an assertion. 
> If fact, 
> in PSL an abort, which is equivalent to a SVA disable, causes an 
> "immediate termination of current and future obligations of a 
> property.
> 
>   The problem is that a tool vendor can interpret a disable iff 
> (true_expression) as success or as vacuous success. That issue needs 
> clarification.  I suggest that we clarify the LRM to state something 
> like ""If prior to the completion of that evaluation the reset 
> expression becomes true, then the overall evaluation of the 
> property_spec is true, and is considered a vacuous success".
>  Ben
>   
> --------------------------------------------------------------
> ------------
>  Ben Cohen Trainer, Consultant, Publisher (310) 721-4830
>  http://www.vhdlcohen.com/ ben_ f rom _abv-sva.org
>  * Co-Author: SystemVerilog Assertions Handbook, 2005 ISBN 
> 0-9705394-7-9
>   * Co-Author: Using PSL/SUGAR for Formal and Dynamic 
> Verification 2nd 
> Edition, 2004, ISBN 0-9705394-6-0
>   * Real Chip Design and Verification Using Verilog and VHDL, 
> 2002 isbn 
> 0-9705394-2-8
>  * Component Design by Example ", 2001 isbn 0-9705394-0-1
>   * VHDL Coding Styles and Methodologies, 2nd Edition, 1999 isbn 
> 0-7923-8474-1
>   * VHDL Answers to Frequently Asked Questions, 2nd Edition, isbn 
> 0-7923-8115
>   
> --------------------------------------------------------------
> -------------------
>