[sv-ec] not (a |->b), not(a |=> b) disallowed?

The following property expressions should be disallowed in the LRM:
not (a |->b), // by "a" or "b" I mean the sequences "a" "b"
not(a |=> b)
Rationale: from FROM LRM: 17.11.1 Implication
"If there is no match of the antecedent sequence_expr from a given start
point, then evaluation of the implication
from that start point succeeds vacuously and returns true"
Thus, is "a" is false, (a |-> b) or (a |=>b) become TRUE, and "not(a |->
b)" or "not(a |=>b)" becomes FALSE, or failure.
That is not the intent here.
In PSL, we disallow a "never {a} |-> {b}" or "never {a} |=> {b}"
By the way, one could express the never implication with sequences as:
(a |-> b |-> 'false)
Ben
-----------------------------------------------------------------------------
Ben Cohen Trainer, Consultant, Publisher (310) 721-4830
_http://www.vhdlcohen.com/_ (http://www.vhdlcohen.com/) vhdlcohen@aol.com
Author of following textbooks:
* 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 Fri Apr 9 15:04:25 2004