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

The attached messages came to the SV-EC reflector but are more appropriate for the SV-AC committee.

Regards

David

-----Original Message-----
From: owner-sv-ec@eda.org [mailto:owner-sv-ec@eda.org] On Behalf Of VhdlCohen@aol.com
Sent: Friday, April 09, 2004 3:04 PM
To: David.Smith@Synopsys.COM; sv-ec@eda.org
Cc: sri@noveldv.com
Subject: [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. <http://www.vhdlcohen.com/> 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
------------------------------------------------------------------------------

attached mail follows:

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. <http://www.vhdlcohen.com/> 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
------------------------------------------------------------------------------

attached mail follows:

Hi Ben;

The LRM example you show

>LRM 17.11 The property definition states on page 236
>property rule2;
> @(clkev) disable iff (foo) not a |-> b ##1 c ##1 d;
>endproperty"

Hmmm, I thought we were going to drop the "not" from this example - or was it another?

There is one other problem with this property. It suffers from incorrect precedence
assumption. It is really parsed as:

(not a) |-> b ##1 c ##1 d

Since the operator 'not' has highest precedence (over implication) you don't really get
what you may want (maybe twice).

    Adam Krolnik
    Verification Mgr.
    LSI Logic Corp.
    Plano TX. 75074
    Co-author "Assertion-Based Design"

attached mail follows:

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. <http://www.vhdlcohen.com/> 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
------------------------------------------------------------------------------

attached mail follows:

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. <http://www.vhdlcohen.com/> 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 11:52:24 2004