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 ---------------------------------------------------------------------------------Received on Thu Aug 18 21:20:23 2005
This archive was generated by hypermail 2.1.8 : Thu Aug 18 2005 - 21:24:10 PDT