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

In a message dated 4/12/2004 8:47:44 PM Pacific Standard Time,
john.havlicek@motorola.com writes:

I do not think these forms should be illegal in SVA.
They are not illegal in PSL. "not" in SVA correponds
to negation in PSL, not to "never".

They are restricted in the simple subset.
Also I know of a tool vendor that restricts that style.
I'll go along with allowing them, provided we put a note of caution.
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"
... bu the way the above is in error same as
(not a) |-> b ##1 c ##1 d;
-----------------------------------------------------------------------------
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 Mon Apr 12 21:08:01 2004