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

LRM 17.11 The property definition states on page 236
"This allows for the following examples:
...
property rule2;
@(clkev) disable iff (foo) not a |-> b ##1 c ##1 d;
endproperty"
That implies that the LRM blesses the structure "not a |-> b"
I still believe that this should not be allowed, per my previous email,
because if
"a" is false, then the property expression "a |-> b" is true, and the
property is false, or fails.
The way it stands, per LRM "not a |-> b" has the following meaning:
a b a|-> b not a|-> b
0 0 true false
0 1 true false
1 0 false true
1 1 true false
Thus, "not a |-> b", is same as a |-> !b
and is not the same meaning as "! (a && b)
The way the definition stand, the implication operator with the "not" is
very confusing.
On the surface "not a |-> b" does not look like it means a |-> !b.
This gets even more confusing when you have a cascade of implication
operators, like
not a |-> b |-> c |->d
I recommend that the committee re-examines the legality and application of
this property expression.
In a message dated 4/9/2004 3:06:45 PM Pacific Standard Time,
VhdlCohen@aol.com writes:

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 Sat Apr 10 22:35:44 2004