Subject: RE: PSL 1.x LRM: Proposal: named block around the assertion statement
From: Avner Landver (alandver@verplex.com)
Date: Tue Jun 10 2003 - 10:50:38 PDT
Another option exists if we wish to avoid introducing a new concept
("labeled assertion").
We can allow the following syntax:
assert PROPERTY_A_THEN_B := always ({a[*3]} |=> {[*4]; b});
which would be equivalent to the following syntax:
property PROPERTY_A_THEN_B := always ({a[*3]} |=> {[*4]; b});
assert ASSERT_A_THEN_B;
Avner Landver
Verplex Systems
-----Original Message-----
From: owner-vfv@eda.org [mailto:owner-vfv@eda.org]On Behalf Of Gal Vardi
Sent: Tuesday, June 10, 2003 1:03 AM
To: Accellera VFV
Subject: Re: PSL 1.x LRM: Proposal: named block around the assertion
statement
So what exactly is the differnet between a named property and it's label ?
(1) named property :
property PROPERTY_A_THEN_B := always ({a[*3]} |=> {[*4]; b});
assert ASSERT_A_THEN_B;
(2) labeled assertion :
ASSERT_A_THEN_B: assert always ({a[*3]} |=> {[*4]; b});
The differences I find :
1. a label cannot have parameters, but a named property can.
2. a label labels a specific assertion (used in specific context, under
specific vunit) while a named property can be multi-instanciated anywhere
in any context.
3. A gui /tool should display all the assrtions that has to be proven (the
list of rules/formulas/properties).
with named properties, the tool should display :
Vunit/Vprop_name.Property_name
but with labeled assertions the tool can simply display the unique
assertion label !
This is shorter, but I find this confusing. do we really need this
duality ?
Ben - any other benefits I missed ?
Gal.
VhdlCohen@aol.com wrote:
In a message dated 6/8/2003 2:39:21 PM Pacific Standard Time,
VhdlCohen@aol.com writes:
This would enable the display of the label when the assertion needs to
be displayed by a tool. For example:
psl ASSERT_A_THEN_B: always ({a[*3]} |=> {[*4]; b});
That should have been:
ASSERT_A_THEN_B: assert always ({a[*3]} |=> {[*4]; b});
Forgot the verification directive.
SO what I am proposing is an optional label in front of the verification
directive.
Ben
-----------------------------------------------------------------------
-----
Ben Cohen Publisher, Trainer, Consultant (310) 721-4830
http://www.vhdlcohen.com/ vhdlcohen@aol.com
Author of following textbooks:
* Using PSL/SUGAR with Verilog and VHDL
Guide to Property Specification Language for ABV, 2003 isbn
0-9705394-4-4
* 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
------------------------------------------------------------------------
------
--
\\\|/// ))))|((((
\\ ~ ~ // / ^ _ \
( @ @ ) ( (o) (o) )
*=oOOo=(_)=oOOo===oOOO====(_)====OOOOo==*
| Gal Vardi |
| Formal Verification |
| Marvell Semiconductor Israel Ltd |
| tel: (+972) 04-9951274 |
| vardi@il.marvell.com |
*====================Oooo.==============*
.oooO ( )
( ) ) /
\ ( (_/
\_)
This message may contain confidential, proprietary or legally privileged
information. The information is intended only for the use of the individual
or entity named above. If the reader of this message is not the
intended recipient, you are hereby notified that any dissemination,
distribution or copying of this communication is strictly prohibited. If you
have received this communication in error, please notify us immediately by
telephone, or by e-mail and delete the message from your computer.
This archive was generated by hypermail 2b28 : Tue Jun 10 2003 - 10:50:18 PDT