Subject: Re: LRM issues: macro and replicator
From: Avigail Orni (ORNIA@il.ibm.com)
Date: Tue Dec 09 2003 - 05:15:09 PST
Hi Neeraj,
I want to thank Gal for answering, and add a few lines of my own.
1)
The current status of the standard regarding pre-processing is the
following
(taken from Section 4.2.3)
"All flavors support cpp-style
pre-processing directives (e.g., #define, #ifdef, #else, #include, and
#undef). All flavors
also support special macros for %for and %if, which can be used to
conditionally or iteratively generate PSL
statements."
This means that all flavors should support C-style macros and comments.
We have already noticed that this creates several problems:
(a) It is not clear whether vpp (Verilog Pre-Processor) directives are
allowed in Verilog flavor.
(b) The use of several different pre-processors creates problems of
coordination.
For example, the order in which they are activated is important.
(c) The cpp in itself is not a standard, and depends on implementation.
This leads to the suggestion mentioned by Gal, that the pre-processing
should not
be a part of the language at all.
Another proposal that has been raised in committee meetings is that the
Verilog flavor should only
use vpp directives, and the EDL/GDL flavor should only use cpp directives.
2)
> Can i use 'parameter' in range or count?
Yes, a Verilog parameter is statically computable, so it can be used for
ranges and repetition counters.
> If Yes, then there can be an expression leading to negative value (e.g.
> { a;b[*(8 - 2*width)} |-> ...
> which is statically computable). How come a parser identify such an
> error.
This error can also occur if you simply allow numerical expressions
such as (8 - 2*5). This type of error cannot be discovered in purely
syntactical
parsing, but it can easily be identified using semantic checks which
accompany
the syntactical parsing.
Regards,
Avigail
________________________________________________________
Avigail Orni
Formal Methods Group
IBM Haifa Research Laboratory
Tel: 972-4-829-6396 ornia@il.ibm.com
Gal Vardi
<vardi@il.marvell To: Neeraj Chandak <neerajc@noida.interrasystems.com>
.com> cc: Avigail Orni/Haifa/IBM@IBMIL
Subject: Re: LRM issues: macro and replicator
07/12/2003 21:58
Hi Neeraj,
For those questions, there is an updated clarification in the mail
reflector, here :
PSL LRM : replicating properties operator "forall" (Thu Nov 20 2003 -
02:55:01 PST)
1) the preprocessing is not defined in the LRM. our suggestion is to leave
it out. any user will parse with his tools. Our wish is that each vendor
will give a way to generate clean PSL files , after preprocessing, but this
might come out quite unreadable.
2) ??
3) A PSL replicator is the variable identifier used to refer to the forall
range.
The sentence in your questioon #3 means that this identifier must be
unique, except for the case where you have several foralls , then you can
use the same identifier again :
vunit my_foralls
{
forall i : 0 .. 2 : assert always x[i] - > y[i];
forall i : 0 .. 3 : assert always x[i] - > next (y);
forall i : 0 .. 4 : assert always z[i] -> next[i] done;
-- but when wrapping , use different identifiers.
forall i : 1 .. 5 :
forall j : 2 .. 3 :
assert { a ; b ; c[->i] } |=> {d[*j]}!
}
Regards,
Gal.
Cindy Eisner wrote:
neeraj,
thanks for your questions. by way of this email, i am asking my
colleague
avigail orni to respond.
regards,
cindy.
--------------------------------------------------------------------
Cindy Eisner
Formal Methods Group
IBM Haifa Research Laboratory
Haifa 31905, Israel
Tel: +972-4-8296-266
Fax: +972-4-8296-114
e-mail: eisner@il.ibm.com
Neeraj Chandak <neerajc@noida.interrasystems.com>
@noida.interrasystems.com
on 04/12/2003 17:18:02
Sent by: neerajc@noida.interrasystems.com
To: Cindy Eisner/Haifa/IBM@IBMIL, vfv@eda.org
cc:
Subject: LRM issues: macro and replicator
Hi Cindy,
I am currently working on PSL and have some doubts
regarding macros, non wrapping PSL
replicator var, parameter values used in replicator operators range.
1. PSL LRM does not say any word regarding the format or syntax
should
be used with directives
define. It says no limitation of define directives. Is it to be
used
as we use in C++ or
like VERILOG. Examples suggests its use like C++. Similer
confusion
persists for other directive
like include, ifdef etc.
2. Replicator operator require range to be positive or zero. Can i
use
'parameter' in range or count?
If Yes, then there can be an expression leading to negative value
(e.g.
{ a;b[*(8 - 2*width)} |-> ...
which is statically computable). How come a parser identify such an
error.
Also in VHDL, can be use statically computable function as replicator
count.
3 In a mail by GAL VARDI dated Sep-04 2003 (link
http://www.eda.org/vfv/hm/1105.html) , he
mentioned that The replicator name /var/ is any legal PSL identifier
name. It cannot be similar to any
other identifier (variable, unit name, design signal etc.) except
another non wrapping PSL
replicator var.
Does this nonwrapping PSL replicator var means name used in forall
property?
Your response is highly obliged especially regarding macros
Regards
Neeraj
--
\\\|/// ))))|((((
\\ ~ ~ // / ^ _ \
( @ @ ) ( (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 Dec 09 2003 - 05:14:01 PST