Erich,
I agree with all of Cindy's comments, and I have a few of my own to add.
They appear below with the prefix ">>>>>Comment AO:"
Regards,
Avigail
=========================================================================
STOPPED HERE during 30 March meeting.
All meeting participants requested to send in comments on the remaining
chapters (what you
agree with, what you don't, etc.) by cutting out the following text,
inserting their comments,
and emailing the result to Erich
=========================================================================
-- general discussion required about just how free an implementation is to
decide when to sample
Chapter 6
========
SR: section 6, 6th paragraph: should be "... a sequential expression holds
tightly on a given trace IF AND ONLY IF that trace models tightly...." (CE
also)
--yes
KW: 6.1.1.1 - why does the LRM say "A;B holds on a path" rather than "A;B
holds tightly on a path"?
CE: 6.1.1.x - remove new restriction on sere operators fusion, within, |,
&, && (but see later comment from AO)
CE: 6.1.1.x - remove wording "non-boolean" in informal semantics of fusion,
within, |, &, && (but see later comment from AO)
AO: 6.1.1.x - now agree that restrictions for the operands of &&,&,| are
necessary
A more detailed explanation would be helpful: "if && has two operands that
are both sequences, then the && operator is the PSL length-matching AND
operator; if && has an operand that is a Boolean, then the && is not the
PSL length-matching AND operator, therefore (in the Verilog flavor) it must
be the Verilog && operator." A possible location for this explanation is in
Section 6.1.1, under "NOTES", before section 6.1.1.1.
EM: 6.1.1 ff - make the following clear: if the "immediate" operands of &,
&&, | - i.e., the tokens that appear between that operator and the next
operator to the left of that operator (or the beginning of the expression),
and the tokens that appear between that operator and the next operator to
the right of that operator (or the end of the expression) - can be parsed
as a Sequence (as defined by the nonterminal Sequence), then this is a PSL
operator; otherwise it is a Verilog operator.
-- general discussion required - this relates to operator precedence
questions
SR: 6.1.1.2 (and 6.1.1.6) - Bool && SERE should be treated the same as bool
: SERE (I don't have a strong preference wethere it is legal or illegal in
PSL).
BC: 6.1.1.3 - restriction of right operand of within to be Boolean is
vacuous because operands are SEREs
SR: 6.1.1.3 - missing space in the last line "iff <space> the SERE..."
CE: 6.1.1.3, first line - "wthin" -> "within"
BC: 6.1.1.4 - restriction of operands of | to be not Boolean is vacuous
because operands are SEREs (same for &, &&)
KW: 6.1.1.6 (and App. B) - adjust semantics of && so that {{a} && {a;a}}
holds on (finite) trace {a}
KW: 6.1.1.6 SERE length-matching and (&&) - In the restrictions, the symbol
"&" should be replaced by "&&"
DB: 6.1.1.6 SERE length-matching and (&&) - Restrictions: & should be && in
"Each operand of & must not be Boolean"
SR: 6.1.1.6 (and 6.1.1.2) - Bool && SERE should be treated the same as bool
: SERE (I don't have a strong preference wethere it is legal or illegal in
PSL).
KW: 6.1.2 and A.3.5 - The definition of Sequence is different in the two
sections (while still equivalent).
>>>>>Comment AO: I think the definitions in 6.1.2 contain the updated BNF,
while A.3.5 still has the old BNF.
CE: 6.1.2.1 - remove restriction that the first operand be a Boolean or
sequence (this is ensured by precedence rules)
DB : 6.1.2.1 - The language allows for composition of consecutive
repetitions: a[*2][*1:2][+] is a legal SERE according to the LRM. Some
mention could be made of the meaning of such a construct, and of the fact
that it cannot be represented by a single consecutive repetition construct.
DB: 6.1.3.2 - [0:3] should be [*0:3]
DB: 6.1.3.2 - [0:5] should be [*0:5]
SR: 6.2.1.2 - "operator operator" -> "operator"
CE: 6.2.1.2 - remove note about nested clocks
EM: 6.2.1.2 - or change it to the following, to parallel the note in
6.1.2.5:
NOTE—When clocks are nested, the inner clock takes precedence over the
outer clock. That is, the property (a -> b@clk2)@clk is equivalent to
the property (a@clk -> b@clk2), with the outer clock applied to only
the unclocked sub-properties (if any). In particular, there is no
conjunction of nested clocks involved.
KW: 6.2.1.6 - either state that {r} (f) and {r} |-> (f) are semantically
equivalent, or drop the old form {r} (f) (which is inconsistent with style
of other operators)
NC: 6.2.1.6.1 - pg 67, line 30 , suffix Implication |=> In line 2:
2) the FL Property that is the right operand holds in the cycle
after any cycle C
such that the Sequence that is the left operand hold
tightly from the given cycle to C.
"right operand holds in the cycle after any cycle C" should be like "right
operand holds in the cycle immediately after any cycle C" as only use of
after is giving me a liberty to start the FL_property after x cycle from C.
CE: 6.2.2.x.y - pg. 70-74 OBE operator font appears too big
KW: 6.2.3 - says forall index represents a non-static variable, and that it
can be used as a repetition count, yet 6.1.2.1 says repetition counts are
static.
Chapter 7
========
KW: 7.1 - what is the scope of a label? how does vunit inheritance and
binding affect labels?
JA: 7.1.2 - p. 84: I don't see the reason why for instance replicated
properties may not be used in an assume directive.
JA: 7.1.3 - p. 85: See above (but for assume_guarantee this time)
JA: 7.1.7 - p. 87: The directive "assume GF p;" is not legal PSL. Shouldn't
it rather be "assume G F p;"
JA: 7.2: p. 88: line 5: assume (GF p) -> (GF q) should probably be assume
(G F p) -> (G F q)
JA: 7.2: p. 88: line 29: VerificationPSL_Directive ->
Verification_Directive (?)
KW: 7.2 - page 88, lines 32 – 34: Redundant "is not explicitly bound" makes
the sentence incorrect.
NC: 7.2 - pg 88, line 35 - mangled sentence: "If the Hierarchical_HDL_Name
is not present, then the verification unit binds to the top-level module of
the design under verification is not explicitly bound."
JA: 7.2: p. 88: lines 35-40: Something is strange with this paragraph.
Maybe the "is not explicitly bound" should be removed on lines 38-39.
DB: 7.2 - this paragraph was not updated correctly:
"If the Hierarchical_HDL_Name is present, then indicates the verification
unit is explicitly bound to the specified design module or module instance
to which the verification unit is bound. If the Hierarchical_HDL_Name is
not present, then the verification unit binds to the top-level module of of
the design under verification is not explicitly bound. See 7.2.1 for a
discussion of binding."
JA: 7.2: p. 88: line 47: clock declaration -> default clock declaration
BC: 7.2 etc. - need VHDL examples
BC: 7.2 - need to adapt pathname to support VHDL entity(arch) names
Hierarchical_HDL_Name ::=
module_Name { Path_Separator instance_Name }
module_name :: Verilog_module_name || VHDL_module_name
Verilog_module_name ::= Identifier_for_name_of_module
VHDL_Module_name ::= Identifier_for_name_of_entity (
identifier_for_name_of_architecture)
NC: 7.2 - how to use a declaration in a vunit in embedded PSL?
NC: 7.2 - what happens if there is more than one default clock in scope -
error, or all default clocks ignored? (e.g., one in each of several vunits
bound to module)
NC: 7.2.2 - pg 91, line 10, 'onehot' is a PSL keyword and is used as name
of psl property
Chapter 8
========
Appendix A
==========
DB: A.3.4 - CLOCK_EXPRESSION should be Clock_Expression
KW: 6.1.2 and A.3.5 - The definition of Sequence is different in the two
sections (while still equivalent).
KW: A.3.5 - need to update to match syntax in 6.1.2
KW: app. A - definition of PSL_Identifier is missing (from the appendix -
is present in 4.2)
Appendix B
==========
KW: 6.1.1.6 (and App. B) - adjust semantics of && so that {{a} && {a;a}}
holds on (finite) trace {a}
Index
=====
CE: index - pg 118 - index should point to page 27 for simple subset, not
(only to) page 3
Issues
=====
1. Operator precedence changes
- always a -> b is interpreted as (always a) -> b, but this is not very
useful, and it is not in the simple subset
- always {a} |-> {b} is interpreted as (always {a}) |-> {b} by precedence
(always higher than |->) but this is not legal according to the syntax
AF: since the syntax does not allow FL_Property |-> Sequence, this will be
interpreted as always Sequence |-> Sequence
EM: but we have tried to remove such conflict (between syntax and operator
precedence rules) by clarifying operator precedence
BC: Can we add a statement that states that the compiler should find the
always {SERE} implication_operator {SERE}
is interpreted as
always ({SERE} implication_operator {SERE})
BC: always and never [should] be placed in the precedence list, above or
below the implication operators (all of them).
rationale:
Backward Compatibility with legacy code.
Create more readable code with less parentheses.
PSL 1.1 now requires parentheses after every "always".
SR: operators ->, <-> traditionally have lowest precedence in both CTL and
LTL
>>>>>Comment AO: I agree with Sitvanit's opinion, I think PSL should be
compatible with CTL and LTL.
AF: consider moving |->, |=> above always, never, but leaving ->, <-> with
lowest precedence
AF: interpreting always a->b as (always a)->b by default opens the door to
potential false positives - PSL v1.01 precedence would be preferable
BC: precedence of the within should be moved to above the sequence AND OR
operators
HH: Please restore the [original, relative] precedence of the FL -> <-> |->
and |=> operators.
2. Distinction between PSL and HDL expressions
KW: problem with {{a} & {b}} |=> c ... {a}, {b} could be aggregates or
seres
proposal: require {} on HDL-Expressions in properties, () on
HDL-Expressions in SEREs
EM: This will be addressed by the pending clarifications on interpretation
of operator symbols (as HDL operators, with HDL operator precedence, if
their immediate operands are Booleans; otherwise as PSL operators).
3. Size of the language
(KW) PSL (syntax and especially semantics) as defined in the current LRM is
too complex for most
users, and simply too large. It is more likely to be used if it can be
presented in a concise way.
This criticism refers both to syntax and semantics:
• There are too many redundancies and even ambiguities, see above.
>>>>>Comment AO: from our experience, these redundancies make the language
convenient for a wide
range of users. Most PSL properties can be written in many different ways:
using pure LTL operators (X),
or syntactic sugar (next), or sequences, or even OBE. Different users (or
projects) prefer different
styles of writing.
As for implementation, it is usually not difficult to implement additional
constructs
that are equivalent to existing ones.
• The semantics must be described completely within the LRM itself, on a
reasonable
number of pages. As long as additional references to about 80 pages of
scientific papers
are needed to clarify open issues, the language will simply not be accepted
by practising
engineers.
Furthermore, there are too many changes between different releases of the
LRM. This indicates
that as a whole, the language is not yet mature enough to be a standard.
Therefore standardization should be split into at least two part. The first
PSL standard should
only define a small subset of the current language, which should be
syntactically and
semantically clean. Extensions of this subset should be postponed.
Possible starting points for the core language could be (to be discussed):
• a subset aligned with SVA
• the simple subset.
Parts of the language which should better be kept out of the core language
in order to keep it
manageable and clear include:
• OBE,
• clocked expressions,
• redundancies such as “X” (= “next”),
• inheritance for unbound modules.
________________________________________________________
Avigail Orni
Formal Methods Group
IBM Haifa Research Laboratory
Tel: 972-4-829-6396 ornia@il.ibm.com
Received on Sun Apr 4 08:35:39 2004
This archive was generated by hypermail 2.1.8 : Sun Apr 04 2004 - 08:37:12 PDT