Subject: PSL LRM 1.01 comments
From: Gal Vardi (vardi@il.marvell.com)
Date: Sun Jun 15 2003 - 07:16:03 PDT
PSL LRM 1.01
comments for LRM typos and extensions subcommittees
3.1.39 non-zero range : "range" applies both to sub-vectors and to
time-range. [5..4] is zero-range if it describes time slots, but not
boolean sub-vectors. there we want both directions [4..5] and [5..4] to
be legal.
3.1.52 - what about constants and "integer" numbers (how do they
interpret to boolean ? is 2=TRUE ?) is it tool dependent ?
4.2.1 Keywords - I still feel that using the word "always" (former
pronunciation of the CTL operator "A") for the good old operator "G"
(which should be pronounced "Globally") is improper, and should be
avoided. I guess this is "theological" issue. people who never used the
CTL operatr "A" will find it difficult to understand my objection...
4.2.3. Macros - %for, %if are mentioned here, but not defined
elsewhere in the document. It must be clear that they are not part of
any layer (probably "preprocessor layer"?) and may be used at any layer.
It must be stated that cpp directives are precompiled *before* PSL
macros (and in verilog flavour, also verilog directives like 'include
and 'define).
- Add "step" keyword to the %for to allow decreasing range : %for i
in 3 .. 0 step -1 do ...
4.2.4 comments - it is advisable that EDL flavor will support both
kinds of comments. // and -- and /*
reasoning : verifying a golden model in EDL, the using the same
files for the real verilog design.
should we add definition of smart comments (like // synopsys
full_case in verilog ) or let each venodr choose his ?
4.4.5 - Simple subset - bad name. does not say what it means. may I
suggest OTF : "On-The-Fly subset ?"
- Here we detail only the FL properties requirements to be
OTF-subset. What about CTL props ? some of them are still "simple".
4.4.6 - finite/infinite - Is there an alternative semantics to the
finite paths ? do we force any of the suggested semantics ?
If we do, then it must be declared here.
5.1 HDL expressions : clarify what can be inside an "if" condition :
is a bus-name accepted as IF condition (== if the bus is
not all-zeroes ->TRUE)?
enumerated types in EDL ?
a variable with non-deterministic behaviour ?
an "x" or "z" value as in verilog standard ?
- multiple definitions of same name - I suggest full
hierarchy, and scope of definition exactly like "C" language.
The name of an identifier , if ambiguous, is resolved from
the innermost vunit that was inherited.
6.1.1.1 - The definition of clocked property ("extracting from a given
path exactly....") is fine as long as the clock is a boolean event.
Generally , it is incorrect following the real design clock , e.g. when
we use @posdge(clk).
The simplest example is describing the behaviour of a single Flip-Flop,
where ff_d is the input of the FF, ff_q is the output of the FF, and
it is gated by the clock "clk" , and the input ff_d is drived from a
faster clock, thus may change in between the ticks where clk is active.
property posedge_triggered_flip_flop { G (ff_d = 0) -> X (ff_q =
0) } @ posedge(clk)
time 0 1 2 3 4 5 6 7
clk 0 0 1 1 0 0 1 1
posedge(clk) 0 0 1 0 0 0 1 0
ff_d 1 1 0 1 1 1 1 1
ff_q 1 1 1 1 1 1 1 1
The clocked formula extracts only cycles #2 and #6 , where the formula
does not hold.
6.1.1.1.6 definition of goto A[->c] : The count c does not have to be
positive.MACROs may result an empty count, exactly like A[=0].
6.1.2.1 in box 23 - sequence declaration : sequence_ParamKind : why not
sequence_ParamType ?
6.2.1.6.5 Logical NOT, restrictions : the operand must be boolean. why ?
"!F(p)" is exactly "G(!p)" and can be computed OTF.
Issues from Erich comments-list (submitted as PDF doc) :
## 40 - repetistion operators are higher than ";" ? I feel it is wrong.
a ; b ; c [=3] should be interpreted as {a ; b ; c[=3] } and not
{a;b;c}[=3] .
Thanks,
Gal.
--
\\\|/// ))))|((((
\\ ~ ~ // / ^ _ \
( @ @ ) ( (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 : Sun Jun 15 2003 - 06:19:13 PDT