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

In a message dated 4/11/2004 8:34:45 AM Pacific Standard Time,
john.havlicek@motorola.com writes:

I do not agree that these forms should be illegal in SVA.
They are legal in PSL.
You're correct from an LRM viewpoint that they are legal in PSL. However,
I know of one tool vendor (I haven't tried others) that will not compile such
a structure.

I agree that their use is generally suspect, so I would
promote warnings and linting messages to make sure people
intend what they are getting with these forms.

However, making them illegal complicates the language
in ways that I think are not necessary.

I'll go along with that. However, a note of caution should be added.
If vendors do the same thing with the "not" as with the PSL "never" with an
implication operator (i.e., disallow it), then we should modify the example on
 page 236 to a simple sequence, something like:
property rule2;
@(clkev) disable iff (foo) not a ##1 b ##1 c ##1 d;
endproperty"
Instead of
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"
-----------------------------------------------------------------------------
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 Sun Apr 11 08:54:02 2004