LRM Issues:
6,45, 46, 48, 62, 74,
71, 72, 73,74, 77, 80,
87, 97, 104, 108, 119,
121,129,130, 135.
Extensions Issues:
5, 19, 23,
26, 33, 39,
40, 42, 43,
49, 54, 56, 58,
59,
62, 63, 64, 65,
66, 67, 68, 69,
70,
75, 76,
78, 79,
82, 83, 84, 85,
86, 88, 89,
90, 91, 92, 93,
94, 95, 96,
98, 99, 100, 101,
102, 103,
105, 106,
109, 110, 111,
112, 113, 114,
115, 116, 117,
118, 120, 122,
123, 124, 125,
126, 127, 131,
132, 133, 134,
136, 137.
Rejected Issues:
30,81.
Out of Scope Issues:
Not Yet Dispositioned Issues:
119.
Issues Not Yet Grouped: issues 74, 91, 118,123, 128, 129, 130.
Group C.1: [3.2] vunit binding, reusable verification IP,
scope and visibility of names, overriding definitions: issues
5, 19, 64,
65, 75, 77,
92,
100, 101, 103
23, 30, 33,
54, 76, 93,
26, 56, 112,113,
114, 116, 119,
120.
Group D.1: [4.2] named parameters: issues
98, 110 .
Group E.1: simple subset: issues
99, 109.
Group F.1: vhdl: issues
63, 79, 81,
84, 85,
86,102,127.
Group K.1: cover: issues
42, 43, 59, 89.
Group L.1: [4.6] LRM (editorial) items: issues
62, 70, 71,
72, 73, 80,
87, 97, 104,
120, 135.
Group M.1: [3.8] clocking and sampling: issues
39, 45, 46,
48, 88, 96, 115,124,125.
Group N.1: [5.0] numeric vs. integer expression: issues
6.
Group O.1: [3.0] SystemC flavor: issues
78.
Group P.1: Assertion control capabilities: issues 49,
66, 67,122.
Group Q.1: verification directives: issues
83,
90, 94, 105,
106, 107, 108,
111, 126, 133,
134.
Group R.1: generate: issues 68, 82.
Group S.1: concept and terminology: issues 58, 95.
Group T.1: built-in functions: issues 40, 117.
Group U.1: New temporal operators: issues 69, 69,
137.
Group V.1: Formal semantics: issues 131, 132.
LRM Issues:
1, 2, 3, 4,
27, 37, 51, 52,
53, 55, 57, 60.
Extensions Issues:
5, 6(L),
7, 8, 9,
10, 11, 12, 13(L),
15,
17, 19, 20, 21,
23, 25, 26, 30,
31, 33, 36(L),
38, 39,
40, 41, 42, 43,
44, 50.
Rejected Issues:
14, 16, 18, 22,
24, 28, 29, 32,
35, 61.
Out of Scope Issues:
34.
Not Yet Dispositioned Issues:
45, 46, 47, 48,
49, 54, 56, 58,
59.
Group A: clocks - modeling layer: issues
7, 40.
Group B: prev/rose/fell - corner cases: issues
9, 10, 11, 12
Group D: [4.2] named constructs: issues
8, 38.
Group E: simple subset: issue
13
Group F: vhdl: issues
15, 17, 27.
Group G: [3.0] abort: issue
20
Group H: [4.0] portability: issue
21
Group I: [2.8] forall: issues
16(R), 25, 36, 41,
47, 50.
Group J: [4.0] non-determinism: issue
31
Group L: [4.6] LRM items: issues
1, 2, 3, 4,
27, 37, 51, 52,
53, 55, 57, 60.
Group O: [3.0] SystemC flavor: issues
44.
Each of the following issues is prefixed with an indication of its disposition: L = LRM E = Extension R = Rejected OOS = Out of Scope ? = not yet determined For each LRM or Extension issue, the priority is also indicated: 5 = highest ... 1 = lowest ? = not yet determined.
1. (L:5) Error in old form of suffix implication syntax:
{ Sequence } ( FL_Property ) should be { SERE } ( FL_Property )
[SY 29Jun04]
2. (L:5) Redundant production for SERE: remove the production SERE ::= Sequence_Instance, because it is redundant [SY 29Jun04]
3. (L:5) Equivalence between W and until needs parens: LTL operators - [a W b] should be equivalent to (a until b), not just a until b - ditto for [a U b] vs. a until! b [EM 30 Jun 04]
4. (L:5) Appendix B, Table 1 needs to be updated for SV: Table 1 of Appendix B (typed-text symbols in the different flavors) needs to be updated to incorporate SystemVerilog flavor [DF 8 Jul 04]
5. (E:4) Clarify implications of multiple vunits bound to same module: PSL LRM should say that multiple vunits bound to the same module are implicitly conjoined - i.e., that assumptions in one may be used to check assertions in the other, etc. [AS 9 Jul 04]
6. (L:5) Correct 6.2.4.2 to refer to numeric expression: The PSL v1.1 LRM says the following (in section 6.2.4.2, Property instantiation): "For a const formal parameter, the actual parameter shall be a statically evaluable integer expression." In this context, an "integer expression" is intended to refer to the type class "numeric expression" defined in section 5.1.4. So there is at least one problem here - for the LRM to be consistent, section 6.2.4.2 should refer to "numeric expression" rather than to "integer expression". [EM 9 Aug 04]
7. (E:5) Clarify effect of default clock declarations: Default clocks apply to directives that don't have a clock. Should they also apply to declarations that don't have a clock? In particular, to endpoint declarations, which may be used in contexts that don't have a clock? And for that matter, does it ever make sense to define a sequence without specifying the clock (or applying the local default clock)? By extension, wouldn't it also make sense to specify (or apply) a clock when declaring a multi-cycle property? [EM 11 Aug 04]
8. (E:5) Allow variable parameters of arbitrary type: Need the ability to pass variable parameters of arbitrary type, as well as to pass constant parameters of arbitrary type. Perhaps we should (a) relax the type class of 'const' params to be AnyType, and add a 'var' param also of AnyType. [EM 11 Aug 04]
9. (E:5) Clarify definition of prev() at time 0: Define the value of prev() in the first cycle, or define that it is not defined. [CE 2 Sep 04]
10. (E:5) Clarify definitions of rose(), fell() at time 0: If prev() is not defined in the first cycle, define the values of rose() and fell() in the first cycle. [CE 2 Sep 04]
11. (E:5) Clarify definition of prev(v(i)): Disallow prev(v(i)), where v is a vector and i is not a constant, or define which value of i should be used (the current value or the previous value). [CE 2 Sep 04]
12. (E:5) Clarify definition of prev(f(i)): Disallow prev(f(i)), where f is a function and i is not a constant, or define which value of i should be used (the current value or the previous value). [CE 2 Sep 04]
13. (L:4) Further restrict the Simple Subset: Next_e and Next_event_e may need to have Boolean operands within the simple subset, because - next_e[1:2](f) = next (f | next f) - next_event_e(b)[1:2](f) = next_event(b)(f | next_event(b)(f)) and in each case the LHS of the "or" operator needs to be Boolean. [SW,CE 2 Sep 04]
14. (R:1) If-then-else assertions:
PSL should support 'if-then-else' assertions provided that the if
condition is Boolean - e.g., always a -> {b; c; d} else {e; f; g};
[JM/DA 3 Sep 04]
15. (E:5) Clarify how PSL Boolean interpretation is applied to VHDL: If a,b are of different VHDL types that are both interpreted as Boolean, does this mean that (a AND b) is legal, using the AND operation on type Boolean? If so, what are the implications for overload resolution? If not, need to clarify the LRM. [EM 20 Sep 04]
16. (R) Clarify how names work for replicated properties: Is there one name for all 'instances', or are there are multiple names, one for each 'instance' (and if so, what they are). [CE 21 Sep 04] [Note that the name of interest is actually the directive name, not the property name. This may interact with a possible extension to allow 'forall' to apply to directives.]
17. (E:5) Clarify the return type for built-in functions in the VHDL
flavor:
If rose/fell are considered Booleans, does this mean that in the VHDL
flavor they return STD.standard.Boolean, or that they are overloaded
to return each of the types that are interpretable as Boolean in PSL?
(The latter includes Boolean, Bit, and std_ulogic.) The more strict
interpretation would mean that, for std_logic signals clk, ena, the
expression (rose(clk) and ena) would be illegal. The more relaxed
interpretation would require overloaded versions of rose, fell,
etc. for VHDL, but it might also lead to the PSL tools doing overload
resolution in flavors that do not inherently support overloading
(e.g., SystemVerilog). [EM 24 Sep 04]
18. (R) Define new operator =>. New precedence rules now require parentheses in nested "-> next" operations. This could be alleviated by defining an operator => meaning "-> next", analogous to |=>, with the same precedence as ->. [EM 28 Sep 04]
19. (E:3) Hierarchical scoping in vunits based on the HDL language Some people have suggested that PSL vunits should have the same kind of hierarchical scoping as the HDLs they apply to. In particular, vunits can be viewed as being similar to packages in VHDL, with 'inherit' providing the same function as 'use' in VHDL. This needs to be discussed in the context of the VHDL standard, and the resolution should then be folded back into the PSL standard.
20. (E:3) The semantics of ({{a} && {a;b}{ abort b).
This is a minor issue (extreme corner case) in the formal semantic
definition of both PSL and SVA and needs to be resolved in parallel in
both languages.
21. (E:4) Portability of PSL. While PSL is defined to work with multiple HDLs, PSL code written for one HDL may not work for an equivalent description written in another HDL, if the PSL depends upon language-specific constructs. This may involve essentially interpreting Verilog-flavor operators in a VHDL (or SystemC) context.
22. (R) The meaning of unclocked, multi-cycle assertions. This amounts to the question of how time is measured in a given language, and in a given tool. PSL does not define this, because different tools have different models of time. The solution needs to support modeling self-timed circuits. (see Anthony McIsaac's writeup about baseline sampling semantics)
23. (E:4) Support for reusable verification IP. This amounts to somehow enabling declaration and instantiation of groups of properties (and auxiliary modeling code), e.g., by adding parameters (of specific data types) to verification units. See (here) for more details.
24. (R) Consider extending simple subset restrictions.
The Simple Subset allows {r} until b, for sequence {r}, boolean b, but
this seems to be not very useful.
25. (E:3) Allow forall to apply to directives.
26. (E:2) Add module name to path for instance-based vunit binding. Need module name in instance-based vunit binding (for implementations that are done are parse time, before design hierarchy is known)
27. (L:4) Clarify interpretation of std_logic 'H', 'L'. Need to clarify how other values of std_ulogic are interpreted as Boolean: 'H' => True, 'L' => False, others => False.
28. (R) Encryption for PSL. PSL should adopt the same encryption mechanism being adopted by VHDL and Verilog.
29. (R) Strong operators on LHS of implication. Check to make sure that strong operators are disallowed on the LHS of an implication, or at least that they are not treated as strong if they appear on the LHS of an implication.
30. (E:4) Better support for reusable verification IP.
31. (E:4) Non-determinism. Need better support for non-determinism in PSL, especially if we intend to use the Verilog flavor as the basis for portable PSL.
32. (R) Clocking of 'next' in modeling layer. Need to specify what the clocking condition is for built-in function `next' in the modeling layer - perhaps specify that the default clock applies to this usage as well.
33. Parameterized vunits: Regarding your issue about what is important for a future PSL standard. I just wanted to say that I feel that the most important feature that any standardization committee should address is the question of reusable verification IP. What is needed is a better mechanism of reusing property via a library approach. Perhaps parametrized vunits is the way to go. Clearly, for VHDL it would be quite simple to extend the current PSL standard to address these issues (simply (oh well...) make it possible for a "function" to take properties as parameters and make it possible to return properties as results. Or rather the other way around, let property declarations take the complete range of VHDL types as parameters. For Verilog, this approach is not viable, and it will be cumbersome to have a different approach here as then verification IP cannot be shared among VHDL and Verilog designs in a coherent way. [JA 04]
34. (OOS) Need a machine-readable form for the PSL formal semantics, to
drive semantic validation without the need for intermediate (and
error-prone) transcription, as well as to drive other sorts of
semantics-driven tools. Note that Mike Gordon is starting a
research project in this area. [MG 23 Sep 04]
35. (R) Need to be able to support modeling of serial protocols in
PSL. This generally involves data-dependent decisions - e.g.,
using 'count' transmitted by the protocol to determine how many
bytes of 'data' are expected to follow.
36. (L:2) Need to clarify whether 'replication' associated with forall
actually involves creation of multiple copies of the
assertion. [BC 5Oct04]
37. (L:?) Section 5.1, Expression Type Classes, does not follow
capitalization conventions used in the rest of the document (first
work capitalized; others not). Some other sections have the same
problem (e.g., A.3). [EM 6Oct04]
38. (E:?) Allow parameters of any of the type classes that we define:
Bit, BitVector, Boolean, Numeric, String. The built-in functions
essentially have parameters of these type classes, so if you want
to pass a parameter to a property, and that property applies a
built-in function to that parameter, you will have to know whether
the parameter is legal for the built-in function, hence it must be
possible to specify the type class of the parameter. For example,
this would allow passing buses as BitVector class parameters to
properties that check relationships among the bits of the
bus. [LB/EM 07Oct04]
>> Related to item 8. [EM 11Oct04]
39. (E:?) Clarify the (default) input sampling mechanism in order to
avoid "races" between property sampling and design update. This is
particularly an issue with simulation-based evaluation of PSL in
(System)Verilog. (Related to item 22.) [BT 08Oct04]
40. (E:?) Clocking of endpoints, prev etc.
Currently, the formal semantics does not deal with clocking "inside"
booleans, which is very strange. This means that the clocking operator
does not touch anything inside (compound) booleans, thus
endpoint e = { a;b;c }
assert always e@(posedge clk);
disregards the @(posedge clk) altogether, and e is clocked with some
"system clock", which is tool dependent. The same is true for
eg. prev(). [JA 11Oct04]
41. (E:?) Generalization of forall.
forall should not be restricted to top-level usage. This is something
which is tied to a specific implementation issue, which should not
shine through to the user. Instead, forall should be just like any
other operator, eg.
assert always a -> next forall i in [0:3] : a[i] > 2 ||
!enable[i];
should be legal PSL.
[JA 11Oct04]
42. (E:?) Data-oriented coverage: Need to be able to use a cover directive more effectively to do data-oriented coverage (as opposed to control-oriented coverage). [EM 11Oct04]
43. (E:?) Transaction-oriented coverage: Need to be able to use a cover directive to recognize a transaction and extract data values being transferred by the transaction for later processing (e.g., for more detailed coverage analysis, or for debugging). [EM 11Oct04]
44. (E:?) SystemC Flavor of PSL Need to define a SystemC flavor of PSL, to allow PSL to be used in system-level models. [EM 11Oct04]
45. (?:?) Clarify that time is discrete: Nowhere in the LRM does it say explicitly that time is discrete. Proposal: Add the following sentence to the defition of evaluation cycle in 3.1.18: "Note that this implies that time is discrete." [CE 26Oct04]
46. (?:?) Clarify that time is context-independent: Nowhere in the LRM does it say that time is context-independent. In other words, that time ticks the same for formula f and for formula g, even if they contain different signals. (We are talking about the finest granularity of time here). Proposal: Add the following sentence to the end of section 4.4.1: "Note: while PSL does not dictate how time ticks for an unclocked property, it does assume that the ticking of time is independent of the property being checked. That is, while two tools may see different sequences of signal values, two properties being checked with the same tool will see the same sequence of signal values." [CE 26Oct04]
47. Typed 'forall':
The forall construct introduces a variable whose type is not specified.
This creates problems when the variable is used in expressions,
particularly in the VHDL flavour.
Also, the following extensions would improve the "forall" construct:
- allow both directions (to and downto) in IndexRanges.
- allow enumeration elements as elements of ValueSet
- allow an enumeration type as Value set
some examples:
forall c: color in { red, green, blue } : ...
forall v: signed(3 downto 0) in std_ulogic : ...
forall v: unsigned(0 to 2) in { '0', '1', 'X' } : ...
[KW 19Oct04]
48. (?:?) Clarify explanation of clock expressions: On page 39, for both Verilog and SystemVerilog, the LRM says "... such a clock expression is considered to hold in those cycles in which it generates an event ...". It is not completely clear that 'such' here is referring only to non-Boolean clock expressions, i.e., clock expressions that are HDL-specific (e.g., posedge clk). Proposal: Add the qualifier "non-Boolean" to the above sentence, in both occurrences, so that it reads in both cases "... such a non-Boolean clock expression is considered to hold in those cycles in which it generates an event...". [CE 17Nov04]
49. Assertion Control Capability: Need an abstract API definition plus language bindings for control of assertion language execution in simulation. [BC 15 Nov04]
50. Parameterized AND/OR operators:
Define AND and OR operators with replication parameters to enable
forall-like conjunction (or disjunction) of instances of a parameterized
property or sequence. An example might be something like
&& [i in {1:10}] (a[i] -> b[i])
or
|| [i in {1:10}] (a[i] -> b[i])
or
|| [i in {1:10}] {a; b==i; d; d==i}
[DF/EM 23 Nov 2004]
51. Incorrect note, or unnecessary restriction:
In section 6.1.2.5, Clocked SERE, the PSL v1.1 LRM says:
NOTE—When clocks are nested, the inner clock takes precedence
over the outer clock. That is, the SERE {a;b@clk2;c}@clk is
equivalent to the SERE {a@clk; b@clk2; c@clk}, with the outer
clock applied to only the unclocked sub-SEREs. In particular,
there is no conjunction of nested clocks involved.
However, 'a@clk', 'b@clk2', and 'c@clk' are all properties, and the
syntax for SEREs does not allow properties as SEREs or elements thereof.
So technically this note should read
NOTE—When clocks are nested, the inner clock takes precedence
over the outer clock. That is, the SERE {a;{b}@clk2;c}@clk is
equivalent to the SERE {{a}@clk; {b}@clk2; {c}@clk}, with the
outer clock applied to only the unclocked sub-SEREs. In
particular, there is no conjunction of nested clocks involved.
But this seems more verbose than necessary, similar to the problem we
used to have with &&, &, | which required extra braces for the operands,
until we removed that requirement in PSL v1.1. So instead of requiring
braces around a Boolean that has an explicit clock expression and appears
within a SERE, could we not allow clocked Booleans as SERE elements, and
implicitly treat them as clocked SEREs containing the single Boolean?
[EM 2 Dec 2004]
52. Appendix B fuzzy makes it difficult to distinguish symbols: Appendix B defines three very similar symbols, which are approximately ||= for Boolean satisfaction, |= for Property satisfaction, and |== for SERE satisfaction (where the '==' part is really three horizontal lines in a column). Unfortunately the process of generating PDF from LaTeX, and then cutting and pasting the PDF into the Frame document, has resulted in all of Appendix B being slightly blurred, and as a result these three symbols are very difficult to distinguish in some places. Either a better process (one that will produce a less blurred result) or different symbols are needed. [EM 2 Dec 2004]
53. Clarification of formal semantics terms
Appendix B defines these terms:
An empty word v = €epsilon has length 0,
a finite word v = (€ell_0€ell_1€ell_2...€ell_n) has length n+1,
and an infinite word has length €infty.
This seems to imply that 'finite word' is defined to mean one that has
length greater than 0, both by contrast to the other two cases, and
because the definition of the length of a finite word (n+1) would seem
to require n to be negative for it to include the empty word. This
should be revised to make it clear that an empty word is also a finite
word. [EM/DF 8 Dec 2004]
54. Need for explicit identification of overriding definitions In 7.2.3, pp. 93-94 (Verification unit scoping rules), it is stated "If a verification unit that is bound to a given HDL instance contains a modeling layer declaration, then that verification unit's declaration takes precedence over any other declaration of the same name, either in a verification unit bound to the same HDL instance in its inherited context, or in the HDL instance itself. This allows a verification unit to redeclare and/or give new behavior to a signal in the design under verification." I propose that for this replacement semantics to be used, the declaration have to include a keyword like "replace" or "override". The problem with the current semantics is that the user has to know the names of the internal signals in the design to make sure that he does not declare a signal with the same name which then overrides the design behavior. In case a declaration is not using the keyword, it is simply added as a new declaration independent of the declarations of the design, that can only be used in the verification unit. [JA 9 Dec 2004]
55. Errors in heading numbers in appendix B. Following are the headings in appendix B: B.1 Typed-text representation of symbols B.2 Syntax B.3 Semantics B.3.1 Semantics of FL formulas B.3.1.1 Unclocked Semantics B.3.1.1.1 Semantics of unclocked SEREs B.3.1.1.2 Semantics of unclocked FL B.3.1.2 Clocked Semantics B.3.1.2.1 Semantics of clocked SEREs B.3.2.2 Semantics of clocked FL <-- should be 3.1.2.2 B.2.2 Semantics of OBE formulas <-- should be 3.2 B.4 Syntactic Sugaring B.3.1 Additional SERE operators <-- should be 4.1 B.3.2 Additional FL operators <-- should be 4.2 B.3.4 Forall <-- should be 4.3 B.5 Rewriting rules for clocks [EM 15 Dec 2004]
56. Definition of vunit binding There is a contradiction between two parts of the LRM. Page 91, lines 42-43 reads "If the verification unit is explicitly bound to a module, then this is equivalent to duplicating the contents of the verification unit and binding each duplication to one instance. Contrast this with page 92, where the "second example" is said to be equivalent to a _pair_ of vunits. See (here) for more details. [JA 21-Dec-04]
57. Typo in 6.2.1.2.1 In PSL v1.1, section 6.2.1.6.1, on page 69, under informal semantics, second bullet, item 2, "immeditately" should be "immediately". [EM 4-Jan-05]
58. Is 'failure' associated with a property or a directive? In Section 4.4.5, Finite-length versus infinite-length behavior, some of the terminology used to talk about whether (and to what extent) a property holds seems to imply that a property is obligated to hold, independent of whether it is asserted. In particular, we use the terms "bad states", "future obligations", and "fails" in that section. This has apparently led some users to conclude that it is inappropriate to talk about an assertion "failing"; that only a property can "fail". I believe we agreed long ago that a property by itself has no obligation to hold. Only when a property is asserted is there any obligation created for the property to hold. So one could argue that Section 4.4.5 should use neutral terms rather than the apparently biased terms "bad", "fail", etc. See (here) for more details. [EM 6-Jan-05]
59. Need for a 'cover all paths' extension A request was made on the Verification Guild forum for PSL to extend the 'cover' directive to have semantics something like "cover all the specific sequences that satisfy this sequence". See (here) for more details. [EM 6-Jan-05]60. Grammar Error in Appendix A There is an error in the grammar: in Appendix A, Flavor Macro HDL_EXPR = SystemVerilog: /SystemVerilog/_Expression / Verilog: /Verilog/_Expression / VHDL: Extended_VHDL_Expression / GDL: /GDL/_Expression contains a reference to Extended_VHDL_Expression, yet we no longer define this nonterminal. Correction: change Extended_VHDL_Expression to /VHDL/_Expression (where /VHDL/ means 'VHDL' in italics). Note that the flavor macro is correct in the body of the LRM; no change is needed there. [EM 9-Jan-05]61. Syntax of prev() A user suggested the following new syntax for the prev: built-in function prev[Number](Any_Type) that will replace the current syntax prev(Any_Type [ , Number]). I think that it makes sense because numbers and ranges are usually enclosed in square brackets and the number parameter of prev is the only exception. Moreover, the prev function and the next operator are quite the same in the eyes of the user. The new syntax suggests similar syntax for both. [SR 20-Dec-04]62. Appendix B Typo in IEEE-1850 Release LRM I was just using my handy complimentary copy of ieee 1850 and noticed a typo in appendix b: on page 130, top of the page, there is a note that should begin "We define". however, it reads "efine" - the first word and the first letter of the second word are missing. [CE 06-Nov-05]63. Hierarchical Signal Access A major limitation of the VHDL flavor of PSL today is the inability to access HDL signals that are not defined in the scope to which a verification unit binds. In many cases you will want a property to refer to signals at multiple different levels of hierarchy within a design and in order to do this today you have to rely on tool specific features that allow such accesses. Usage of such tool specific features makes the PSL unportable, and therefore greatly reduces the value of PSL being a standardized language in the cases where such cross hierarchical references are needed. I provide two suggestions of how this could be implemented support for such accesses in PSL. [JM 25-Nov-05]64. Signal references qualified by inherited vunit name If v1 is a verification unit that binds to an entity e1 and v2 is a verification unit that binds to an entity e2, and v1 inherits v2, then any signal that is accessible by v2 is accessible by v1 through a construct<v2>::<sig> if there is only one instance of v2 in the design tree. Pros: Infrastructure for inheritance already exists in PSL and could be leveraged by this functionality. Cons: Verification units would have to be created specifically to access signals in blocks that would not normally have any verification units bound to them. [JM 25-Nov-05] 65. Hierarchical signal access - aliasing of names Add to the modeling layer a declaration that would be used to declare a new signal that connects to a signal in the hierarchy like this: connect <new sig>to <instance> :: <sig>; Pros: Allows accesses to any level of design hierarchy. Cons: Requires a new declaration for each signal being accessed. If there are a lot of these signals then this can become cumbersome. [JM 25-Nov-05] 66. The action block Add an action block a la SVA. For simplicity, the action block can modify the value of any variable in the design. The user can then expand on the action to be taken based on this assignment. From a language viewpoint, VHDL offers the biggest challenge because of the driver implications. However VHDL users can use the 'active of 'transaction attributes to know when a new assignment (different or same ) was made onto a signal. The action block may also include the display of variables local to the assertion, or variables of the design. [BC 14-Nov-05]67. Local variables Add local variable to sequences and assertions. Local variables adds great flexibility in coding style of assertions. [BC 14-Nov-05]68. HDL Generate Allow the HDL "generate" statement to embrace an assertion. Ben [BC 15-Nov-05]69. Add a first_match function The following link demonstrates a user requirement for an assertion. The solution involved the use of a local variable and a first_match function. http://verificationguild.com/modules.php?name=Forums&file=viewtopic&p=4060#4060 Below is the SVA solution, but with PSL supporting local variables and first_match, a very similar solution can be implemented. logic scl_enb, SCL; `define true 1 property p_SclSda; int v_count; @ (posedge clk2 && scl_enb && SCL) (check && SDA==1'b1, v_count=1) |=> first_match((`true, v_count+=1)[*0:$] ##1 (v_count==9)) |-> SDA==1'b1; endproperty : p_SclSda assert property (p_SclSda) else $display("%t SDA error on 9th SCL, sampled SDA %b", $time, $sampled(SDA)); endmodule : test The first_match is needed in the consequent of the the first implication because that consequent IS the antecedent of the second property. Thus, in "antecedent |=> consequent1 |-> consequent2" the consequent1 is the antecedent of consequent2. If antecedent succeeds and consequent1 fails, the property succeeds vacuously, and keeps on trying (with the [*0:$]). Thus the property as a whole cannot fail. The first_match fixes all of that. See (here) for more details. [BC 15-Nov-05]70. LRM Font Problem IEEE 1850 PSL LRM, clause 5.2.2, Informal Semantics, par. 2, first line: expression "a -> b" is in normal font; should be in "code" font. [EM 06-Mar-06]71. LRM Index All the built-in functions are missing from the index. [SR 22-Feb-06]72. LRM Missing Keywords in Table 1 In the IEEE 1850 PSL LRM, the grammar contains the production PSL_Type_Class ::= 'boolean' | 'bit' | 'bitvector' | 'numeric' | 'string' (see Syntax 6-77, p94) However, in Table 1, Keywords, in clause 4.2.2, Keywords, only 'boolean' is listed. The other four type class names should be listed in the table also. [EM 20-Feb-06]73. Editorial issue with the within operator In the IEEE 1850 PSL LRM, the 'within' operator is referred to as the "sequence within" operator in clause 4.2.3.2, in Table 2 on page 18, and also in clause 4.2.3.2.4 on page 19. However, this operator is referred to as "SERE within" in clause 6.1.1.2.4 on page 54. [EM 17-Feb-06]74. Syntax of "within" In clause 6.1.1.2, the syntax box requires the left operand of the 'within' operator to be a Compound_SERE. This is consistent with the requirement for a Compound_SERE left operand for the operators &&, &, and |. However, unlike those operators, which would be ambiguous if the left operand were a simple Boolean (because those operators are also Verilog logical operators), 'within' would not be ambiguous if its left operand were a Boolean. Furthermore it would make some semantic sense to be able to talk about a Boolean event occuring 'within' a Sequence, e.g., Reset within [*5] without having to turn the left operand into a Braced_SERE in order to make it a Compound_SERE: {Reset} within [*5] So perhaps we should consider relaxing the syntax to allow the left operand of 'within' to be any SERE, and not restricted to a Compound_SERE. [EM 17-Feb-06]75. vunit scoping rules i know that we have an open issue about vunit scoping rules. can this url be added to the issue text: See details here ? just so that we make sure we have addressed the point. [CE 16-FEB-06]76. Issues related to overriding assignments in vunits There are several related questions that seem to need clarification in the PSL LRM, all having to do with the notion of an assignment in a vunit 'overriding' assignments in the design. I would like to see these all resolved in the next version of IEEE 1850 PSL. Clause 7.2.3 says the following: "If a design signal name is redeclared in a verification unit bound to a given module or instance, and that name is assigned a value in that verification unit, then the declaration in the verification unit overrides the declaration in the design module or instance and in any inherited verification units bound to the same design module or instance, and the assignment to that name in the verification unit overrides all assignments to the signal with that name in the design and in any inherited verification units bound to the same design module or instance." Other than an occurrence of an overriding assignment in an example later in the same clause, there appears to be no other reference to overriding assignments in the LRM. Questions: 1. If an assignment in a vunit assigns to a design signal that is NOT redeclared in the vunit, what is the effect? Is this illegal? If legal, does the assignment override assignments in the design? Or does it simply add another assignment to the same signal (in which case HDL assignment resolution rules apply)? 2. Are there any restrictions on what values or expressions an overriding assignment can assign to a design signal? The working group has primarily talked about assigning nondeterministic values to design signals, when we have talked about this at all. Is the intent to allow only such assignments? Or is it legal to assign to a design signal the value of an arbitrary expression, including expressions that are functions of other design signals, thus changing the functionality of the design rather than merely abstracting it? 3. One can also use an assume directive to constrain the values of a design signal. Is there any difference between using an assume directive (e.g., "assume S==nondet(...)") and using an overriding assignment? If so, what is the difference? If not, why do we need both? 4. If two vunits (for example, A and B, where A inherits B) both contain overriding assignments to the same design signal, what is the result? Does one assignment override the other? Or do they both apply (and then HDL multiple-driver resolution semantics come into play)? 5. Same question as (4), except that A and B are both bound to the same design module or instance, but neither inherits the other? Or is it intended (though the LRM does not say this) that at most one vunit can be bound to a given design module or instance? 6. Same question as (5), except that vunit A and vunit B are bound to different modules, but contain assignments to the same signal (e.g., using OOMRs) or to the same net (e.g., if A assigns to design signal Sa, and B assigns to design port Sb, and in the design Sa is associated with Sb)? Or is there an implicit assumption that at most one vunit is bound to any part of the design? [I doubt it.] 7. What is the meaning of an overriding assignment (if any) in a simulation context? A related question is this: 8. The Simple Subset is that subset of PSL temporal layer constructs that can be applied easily in both formal verification and simulation. It does this by excluding temporal constructs that (in the general case) are difficult to implement efficiently in simulation. Should the Simple Subset be extended to exclude constructs in other layers that are not applicable to both formal verification and simulation? If so, and if overriding assignments only have meaning in formal verification, should they be excluded from the Simple Subset? Finally, there is a concern that the user might accidentally override a design signal when he actually intended to declare and use an auxiliary signal in the vunit, and the auxiliary signal just happens to end up with the same name as a signal in the design. Is there something we can do to avoid this problem? Also see: http://www.eda-stds.org/ieee-1850/ieee-1850-issues/hm/0102.html [EM 10-Feb-06]77. Issues with PSL flavors Following is an issue raised by a PSL user regarding the definition of flavors within PSL: Clause 4.3.2 HDL dependencies, says "PSL is defined in several flavors, each of which corresponds to a particular hardware description language with which PSL can be used. Flavor macros reflect the flavors of PSL in the syntax definition. A flavor macro is similar to a grammar production, in that it defines alternative replacements for a nonterminal in the grammar. A flavor macro is different from a grammar production, in that the alternatives are labeled with an HDL name and, in the context of a given HDL, only the alternative labeled with that HDL name can be selected." The phrase "in the context of a given HDL" is not defined here or anywhere else in the PSL LRM. Originally, this phrase referred to the HDL used in the design module (or instance) to which a given vunit is bound. Given the new text in clause 7.2.3, which allows the flavor of a vunit to be different from the HDL of the corresponding design module, it seems no longer possible to assume that "the context of a given HDL" is implicit in the association of a vunit with a given design module. Instead, it would appear to be necessary to determine the HDL context from the vunit itself. If so, the LRM needs to specify more clearly how this should be done. We might even need to add syntax to make it clear what HDL context is to be assumed. The LRM should also specify more clearly the scope of a flavor - i.e., does it apply to an entire file, or to a verification unit within a file, or to a region within a verification unit, etc. If the flavor determination remains implicit, this will need to be clarified. If we add syntax to explicitly specify a flavor, we will need to consider this scope issue in deciding what syntax to add. There is also a question whether all PSL vunits must be of one flavor or another, or whether it is possible to have a 'neutral' flavor vunit that only contains declarations to be inherited into other PSL vunits. Since flavors primarily affect the Boolean and Modeling layers, a vunit that consists only of Temporal layer items (e.g., property and sequence declarations) in which all Booleans are parameters of PSL declarations would not need to be of any particular flavor. See (here) for more details. [EM 06-Feb-06]78. Ambiguity w.r.t. a->b in SystemC flavor An ambiguity exists in the current IEEE 1850 LRM, regarding interpretation of the -> operator in the SystemC flavor. In particular, the expression a->b could be interpreted as involving either the PSL implication operator or the C/C++/SystemC pointer dereference operator. This problem was noted when the working group discussed adding a SystemC flavor, and a resolution was proposed (but apparently did not make it into the LRM). In the last draft for Group O: SystemC Flavor (see http://www.eda-stds.org/ieee-1850/ieee-1850-extensions/hm/0165.html), the following appeared: 6.2.1.7.1 [which became 6.2.1.7.2] Logical implication - under Restrictions, add a new paragraph that reads: "In the SystemC flavor, if the operator '->' appears in an expression and its left operand is the name of a pointer to an object that has a member whose name is the right operand, then the '->' operator is interpreted as the SystemC member operator, not as the logical implication operator." However, this restriction did not make it into the LRM, so it needs to be added in the next revision. Note that the ambiguity also exists with the PSL operator -> in clause 5.2.2, but this was not mentioned in the proposal for a SystemC flavor. A similar statement to the above needs to be made in clause 5.2.2. Note that, as always with HDL operators overloaded for use in PSL, there is an issue of operator precedence, since all HDL operators have higher precedence than all PSL operators. See (here) for more details. [EM 02-Feb-06]79. VHDL Hierarchical Reference many people seem to think that because vhdl does not allow hierarchical references, they are not allowed in the vhdl flavor of psl. this was never the intention, and i would like to clarify in the lrm that this is not the case. doing so may involve editing the grammar, since a boolean expression is based on an hdl expression, and perhaps the grammar of vhdl is such that hierarchical references are prohibited synactically rather than semantically. See (here) for more details. [CE 01-Feb-06] When we consider this, we should be careful about the way we treat the path separators used for hierarchical references. In the current syntax, either "." or "/" is allowed in any flavor. That's OK as long as hierarchical references only appear in the names of modules or instances used for vunit binding. However, if we allow this in boolean expressions, then we have to prevent ambiguity between "/" as a path separator and "/" as a division operator. [AO 18-May-06]80. Keyword Table Ommision In the IEEE 1850-2005 PSL LRM, table 1, Keywords, the keyword 'for' (used in "paramterized SEREs" and "parameterized properties") is not listed. This needs to be corrected in the next version. Also, in table 2, Operator Precedence, neither 'for' nor 'forall' is listed. It could be argued that neither is really an operator, so the question of precedence is not an issue, but if that is the position we want to take, the LRM should contain a note to that effect. [EM 14-Dec-06]81. Should keywords be case sensitive in VHDL? VHDL users are used to having the flexibility of case-sensitive identifiers (same name different meaning depending on case). According to IEEE Std 1850-2005, section 4.2.2, keywords are reserved "identifiers" in PSL. And according section 4.2.1, "identifiers" are case-insensitive in VHDL flavor. [AS 06-Feb-06]82. Generate statement for directrives Allow verification directives in generate statements (Verilog and VHDL). Allow the use of verification directives inside HDL generate blocks inside vunits. Revise the HDL_STMT of the vunit_item to include verification directives in the appropriate locations in the HDL grammar (generate items). This proposed update to the native HDL grammar is similar to the how built-in functions are included in the HDL expressions of the modeling layer code. Use of generated directives is very important for creation of library components. This request duplicates Ben Cohen's request. [AS 29-Nov-05]83. Semantic clarification for restrict Clarification: Semantics of restrict. Restrict is a form of constraint. What is the exact semantics? Should add semantics and clarify the explanation. In the example in the LRM, restrict {!rst;rst[*3];!rst[*]}, is rst required to hold low after the fourth cycle? There sequence specifies that there can be zero or more cycles of !rst. The text specifies that rst is ?low forever afterwords?. [AS 29-Nov-05]84. VHDL binding clarification Clarification: VHDL binding clarification. In the HDL_Module_NAME of a binding, in VHDL, can the design unit that the vunit is bound to include a lib name? e.g. LIB.e(A). If so, is some prior library clause required? May need more clarification on the composition of HDL_Module_NAME for VHDL. [AS 29-Nov-05]85. VHDL use clause and vunit Enhancement: VHDL: Allow use clause outside and just before a vunit. A use clause is allowed before a design unit in HDL_UNIT, but strictly it should only apply to the next VHDL design unit, and not extend to any next design unit or vunit. Can a library clause and/or use clause be placed just before a vunit? It should, but the formal syntax does not allow it. [AS 29-Nov-05]86. VHDL define and entity_aspect Clarification: In section A.3 on page 117, the VHDL non-terminal is entity_aspect is listed but no longer is elsewhere in the LRM. Also entity_aspect is not in the VHDL grammar. [AS 29-Nov-05]87. LRM editing error (remove "/") Clarification: In section 4.2.4.1 %for, the use of slashes as in /var/ in the syntax is confusing to users because it is not clear if the slashes are part of the syntax or not. In the same section, the examples are of GDL, which is not described in detail and has been confusing to users. [AS 29-Nov-05]88. Clock context inheritence: There is a small problem with the definition of clock context inheritance: In IEEE 1850 PSL, we replaced endpoint declarations with the ended() built-in function. We also clarified the rules for clock context inheritance. However, we failed to address the new ended() function in the new clock context inheritance rules. The LRM says the following regarding the clock context of a sequence: For a property or sequence, the clock context is - specified by the @ operator, if present; otherwise - inherited from the immediately enclosing property or sequence, if any; otherwise - inherited from the property or sequence in which it is instantiated, if any; otherwise - (for a top-level property or sequence) specified by the applicable default clock declaration, if any; otherwise - True. This needs to be extended to include the case in which a sequence appears within an immediately enclosing built-in function call (specifically, within a call to ended()). The extended rules should be as follows: For a property or sequence, the clock context is - specified by the @ operator, if present; otherwise - inherited from the immediately enclosing property, sequence, or built-in function call, if any; otherwise - inherited from the property, sequence, or built-in function call in which it is instantiated, if any; otherwise - (for a top-level property or sequence) specified by the applicable default clock declaration, if any; otherwise - True. See (here) for more details. [EM 25-Oct-05]89. Covergroup construct: Add a SystemVerilog style covergroup. The covergroup construct offers an alternative way to specify functional coverage to the SVA cover directive. See (here) for more details. [JM 25-Nov-05]90. Clarify informal semantics for assume guarantee directive: The assume_guarantee directive is described somewhat vaguely in the PSL (1850) LRM: # The Assume Guarantee Directive, [..] instructs the verification tool # to perform two different but related tasks: one is to perform a # verification constrained with the property in question (as described # in 7.1.2) the other one isto verify independently that the property # holds. This should be interpreted to mean that the property should be used as an assume in one verification task and as an assert in another. It is not specified however with respect to what modules the two different task should be performed. This was deliberately left open partly because there was no time to specify this exactly, so the exact interpretation of this is left to the respective tools. You could well argue that this is unfortunate because it prevents portability across different tools. I think this should be specified further and maybe we would also need some enhanced syntax to somehow specify the two environments that are presupposed. See (here) for more details. [JM 25-Nov-05]91. Global reset: Add a global reset concept in order to simplify properties. What is intended here is to add something like a default abort = rst; declaration to mirror the 'default clock = clk' declaration. The semantics would presumably be to add an 'abort rst' on the top level of any formula in a directive where this makes sense. (A cover directive might be a place where it doesn't make sense for instance.) See (here) for more details. [JM 25-Nov-05]92. Multiple levels of inheritance: In section 5.2.1, the rules for determining the meaning of a name can be interpreted as allowing only 4 levels of inheritance. This should be clarified, to unambiguously describe a model with multiple levels of inheritance. [AO 29-Nov-05]93. "original" built-in function: Since the modeling layer may override the behavior of a signal, there is a need for the built-in function "original()": original(S) gives the original behavior of signal S. [AO 29-Nov-05]94. formal semantics for directives: Need to define formal semantics for all verification directives. [AO 29-Nov-05]95. Levels of satisfiability: Need to informally clarify the 4 levels of satisfiability [AO 29-Nov-05]96. Clock context definition for built-in functions: Consider the following property: assert always ( a -> rose(b, rose(c))); According to the current definition, the inner rose is the explicit clock context for the outer rose. But the inner rose has no explicit clock, so by the LRM definition, it's clock context is defined by the enclosing built-in function -- which is the outer rose. It should be specified that this rule does not apply for a built-in function clock context. [AO 29-Nov-05]97. "const numeric" parameters -- improving the examples In Section 6.3.2.1. Sequence declaration, the following example appears: "sequence BusArb (boolean br, bg; const n) = { br; (br && !bg)[*0:n]; br && bg };" This example uses "const n", which is actually shorthand for "const numeric n". Although this is legal, I think it would be better style to write "const numeric n" in the example. It seems to me that the "const n" shorthand is old-fashioned LRM 1.1 style, which we have maintained for backward compatibility, but we should encourage the use of the newer style (which currently is not demonstrated in the LRM -- there are no examples with the keyword "numeric"). The same suggestion holds for the two examples in Section 6.3.2.2 Property declaration. [AO 16-Apr-06]98. Problems with restrictions on parameterized SEREs/properties and replicated properties 1. IEEE 1850-2005, clause 6.1.1.2.5, Parameterized SERE, under /Restrictions/, 2nd par., 4th bullet says "The parameter name shall be used in one or more expressions in the Property, or as an actual parameter in the instantiation of a parameterized SERE, so that each of the instances of the SERE corresponds to a unique value of the parameter name." This section is only about Parameterized SEREs, so the reference to Property here should be to SERE instead. Also, the reference to "the instantiation of a parameterized SERE" is clearly not intended to refer to the subject of this clause, but rather to a Sequence_Instance, since the latter has actual parameters, while the subject of this clause does not. So the clause should probably read as follows: "The parameter name shall be used in one or more expressions in the SERE, or as an actual parameter in a Sequence Instance, so that each instance of the parameterized SERE corresponds to a unique value of the parameter name." Now one could argue that if the SERE in the parameterized SERE is a Sequence Instance, and the parameter name appears as an actual in that Sequence Instance, then it also appears in the SERE, so this paragraph need not mention a Sequence Instance explicitly. So the bullet could be shortened to "The parameter name shall be used in one or more expressions in the SERE, so that each instance of the parameterized SERE corresponds to a unique value of the parameter name." At the same time, it is not clear what this restriction is really trying to accomplish. If the point is to ensure that each instance of the parameterized SERE is different from every other instance of the parameterized SERE, we first need a definition for (in)equivalence of SEREs. I assume that two SEREs would be considered equivalent if they both hold tightly on the same traces, but I doubt if implementation of such a definition would be feasible. If the intent is simpler--namely, that each SERE instance is syntactically different from every other SERE instance--then something more needs to be said about Sequence Instances than simply that the parameter name appears as an actual parameter, since there is no requirement that the definition of a sequence make use of every formal parameter, nor is it guaranteed that formals (representing actuals) would be used in such a way to generate unique sequence instances. We might also consider deleting this bullet entirely because it is unenforceable. 2. Similarly, in clause 6.2.1.7.1, Parameterized property, under /Restrictions/, the same bullet text as above appears. In this case, the references to SEREs are inappropriate and should be deleted or changed. With the same reasoning as above, the bullet could be reduced to "The parameter name shall be used in one or more expressions in the Property, so that each instance of the Property corresponds to a unique value of the parameter name." or else deleted entirely because it is unenforceable. 3. In both cases, the original text comes from clause 6.2.3, Replicated properties, under /Restrictions/, par. 5, which says "The parameter name shall be used in one or more expressions in the Property, or as an actual parameter in the instantiation of a parameterized Property, so that each of the replicated instances of the Property corresponds to a unique value of the parameter name." Here again, the reference to "parameterized Property" was not intended to refer to the topic of this clause, but rather to a "property instantiation" (clause 6.3.3.2) which can have actual parameters. In this case, we don't have a nonterminal to refer to, so the (corrected) paragraph should probably refer to clause 6.3.3.2 explicitly, if the working group feels it is necessary to keep the reference at all. But as above, one could argue that the reference is unnecessary, and that the paragraph could be reduced to "The parameter name shall be used in one or more expressions in the Property, so that each replicated instance of the Property corresponds to a unique value of the parameter name." or else deleted entirely because it is unenforceable. [EM 17-Apr-06]99. Simple subset rule for until* In IEEE 1850 PSL, the Simple Subset requires that the left operand of an overlapping until* operator be Boolean (in addition to the requirement that the right operand of any until* operator be Boolean). This restriction on the LHS operand of overlapping until* is both theoretically and practically unnecessary. We should consider replacing the two rules - The right-hand side operand of a non-overlapping until* operator is a Boolean. - Both operands of an overlapping until* operator are Boolean. with the single, simpler rule - The right-hand side operand of an until* operator is a Boolean. [EM 19-Apr-06]100. Uniqueness of names in HDL expressions (lookup algorithm inconsistency) In the IEEE 1850 PSL, clause 5.2.1 HDL expressions, p37, it says For each name and operator symbol in the HDL expression, the meaning of the name or operator symbol is determined as follows: [steps a through f] It is an error if more than one declaration of a given name appears in the current verification unit [in step a)], or in the transitive closure of all inherited verification units [in step b)], or in the default verification mode [in step c)], or if the name is ambiguous at the end of the associated design module or instance [in step d)]. It would appear that the paragraph following the list is out-of-date w.r.t. the list, since it only mentions 4 items instead of 6. It would appear that the paragraph should be amended to read as follows: It is an error if more than one declaration of a given name appears in the current verification unit [in steps a or b)], or in the transitive closure of all inherited verification units [in step c)], or in the default verification mode [in step d)], or if the name is ambiguous at the end of the associated design module or instance [in step e)]. [EM 1-May-06]101. Name space of labels In the IEEE 1850 PSL, clause 7.1 Verification directives, p101, it says A verification directive may be preceded by a label. If a label is present, it must not be the same as any other label in the same verification unit. Labels enable construction of a unique name for any instance of that directive. Such unique names can be used by a tool for selective control and reporting of results. The intent seems to be that labels are uniquely defined. However, the LRM does not say anywhere whether a label can be the same as the name of a PSL declaration. Note that in clause 6.3 Property and sequence declarations, p94, the LRM says The name of the declaration shall not be same as any other declaration in the same verification unit. So property and sequence names are similarly defined to be unique w.r.t. each other - but labels are not mentioned here. In the absence of any further restrictions, this appears to create two distinct name spaces: that of labels, and that of all other declarations. This can be confusing to users, especially given that labels in HDLs do not occupy a separate namespace. The above statements ought to be generalized to ensure that every name defined in a PSL verification unit should be unique, whether the name is a label or a declaration name. [EM 1-May-06]102. Type Classes in a VHDL context create ambiguity for overload resolution. VHDL allows a given operator symbol or function name to be declared multiple times--with different meanings--provided that in each case the declaration has a unique "parameter and result type profile", i.e., that the paramater and result types of each declaration are distinguishable. This means that in an expression, the meaning of an operator such as '=' must be determined by examining the types of the operands and the type of result required by the context. But in a VHDL-flavor PSL assertion, a Boolean expression can be of any of several types, such as Bit, Boolean, or std_ulogic, each of which is compatible with PSL type class "Boolean". As a result, if the user has overloaded an operator such as '=' so that one version returns a bit, while another version (the implicitly declared one) returns a Boolean, then in a PSL context (which allows either a Bit or a Boolean type expression to appear), an expression such as (a=b) becomes ambiguous. This could be avoided by specifying a rule for disambiguating such a situation. The rule could be based on type (e.g., look for a Boolean expression first, otherwise a Bit expression, otherwise a std_logic expression), or it could be based on characteristics of operator declarations (e.g., if there is a conflict between a user-defined operator and an implicitly declared operator, ignore the implicitly declared operator). [EM 3-May-06]103. PSL does not define precisely the scope of a declaration. In the following example: property a (boolean a,b) = {a} |-> {b}; the name 'a' is used both as the name of the property and as the name of a formal parameter of the property. Where does 'a' mean the property, and where does it mean the parameter? The current rules for name resolution in PSL do not answer this question, nor do they even say whether this is legal or illegal. In VHDL, this is legal and is clearly defined: in general, the scope of a name starts at [the end of] its declaration, and extends to the end of the innermost enclosing scope, except where it is hidden. If we were to apply this to the PSL above, the scope of 'a' meaning the formal parameter would begin at [the end of] the declaration of the formal parameter, and extend to the end of the property declaration, so that clearly the 'a' in '{a}' would refer to the formal parameter, not to the property. Similarly, the scope of 'a' meaning the property would begin at [the end of] the property declaration and extend to the end of the innermost enclosing context, e.g., the enclosing vunit - and it would be hidden within the body of the property by the declaration of the formal parameter 'a'. The PSL LRM explains in detail how names in an HDL expression are interpreted (clause 5.2.1). However, it does not appear to explain how a reference to a name declared in PSL is interpreted. In particular, there is no path from nonterminal HDL_or_PSL_Expression to /Formal_Parameter/_Name. The discussion of the lookup process (in the transitive closure of the inherited verification units, etc.) does not clearly distinguish between HDL-declared names and PSL-declared names, but it clearly does not consider nested declarations such as declarations of formal parameters, which have a given meaning only within the scope of an enclosing property or sequence declaration. [EM 3-May-06]104. syntax glitch in nondet, nondet_vector In the IEEE 1850-2005 PSL LRM, a reference to a nonterminal "Value_List" appears in - the syntax production for built-in function 'nondet' (5.2.3, syntax 5-20, p38) - the syntax production for built-in function 'nondet_vector' (5.2.3, syntax 5-20, p38) - the syntax production for built-in function 'nondet' (A.4.8, p127) - the syntax production for built-in function 'nondet_vector' (A.4.8, p127) However, the description of these functions refers to "Value Set", and the syntax used in the examples is consistent with the syntax for production "Value_Set" (defined in 6.2.3, syntax 6-76, p91). It appears that the syntax for nondet() and nondet_vector() should be updated to refer to Value_Set instead of Value_List. There are also several occurrences of "value set" in the description that should be capitalized, to make it clear that this refers to the text object represented by the nonterminal Value_Set. Finally, we should consider moving the definition of Value_Set backward, from page 91, to where it is first referenced, on page 38. [EM 5-May-06]105. Deprecate assume_guarantee, restrict_guarantee. These directives are provided as explicit representations of the assume_guarantee paradigm. However, in practice, nearly all assumptions (or restrictions) will eventually need to be checked in a larger context. This suggests that almost all assumptions (or restrictions) should be expressed with assume_guarantee (or restrict_guarantee). This is inconvenient, in part because these keywords are so long, compared to the much shorter, more readable, and more obvious 'assume' and 'restrict'. Also, although the LRM says that the *_guarantee directives involve "verify[ing] independently" that an assumed property or restricted sequence holds, it does not address how a given tool should know, in a given run, whether to treat such a directive as an assumption/restriction or to verify that the assumption/restriction holds. And in any case, not using the *_guarantee directives does not indicate that there is never going to be a need to verify that an assumed property or restricted sequence holds. It would be better to simplify the language by removing these keywords. The assume/guarantee paradigm could still be represented explicitly via verification units (e.g., a vunit A defining sequences/properties, vmodes B1..Bn inheriting A and assuming/restricting various properties/sequences, and vprops C1..Cm inheriting A and asserting various properties/sequences [but see issue 107]). [EM 17-May-06]106. Allow a report clause on assume, restrict. It is likely that any assumption or restriction will eventually need to be verified. It would be convenient to allow such assumptions or restrictions to include a 'report' clause, both to serve as a user-defined comment explaining the assumption/restriction, and to provide a text string to be reported when the assumption or restriction is later verified. [EM 17-May-06]107. Verifying that a restrict directive holds. It is not clear how one verifies that a restrict directive holds. For a directive "restrict S;", the assertion "assert S;" is insufficient, as is "assert S!;", since the first is weak and therefore might not hold tightly at all over the whole trace, whereas the second is strong but might hold tightly only on a prefix of the whole trace. Can we define this as "assert {S : EOT}", where EOT = end of trace? If so, can we enable the user to write this explicitly? Is there a better way (without EOT) to express this? [EM 17-May-06]108. Verification of (Strong) Fairness directives. These directives are special forms of assumption. Unlike the general forms, these don't have corresponding "*_guarantee" directives--which is another argument for deprecating the "*_guarantee" directives. At the same time, it should be clear how (strong) fairness assumptions are to be verified. Since a fairness directive "fairness P;" is equivalent to "assume always eventually P", it would appear that verifying a fairness directive amounts to verifying the assertion "assert always eventually P". Similarly, it would appear that verifying a strong fairness directive "strong fairness P, Q;" would amount to verifying the assertion "assert (always eventually P) -> (always eventually Q)". The LRM should mention this, perhaps in a note. [EM 17-May-06]109. Strong Fairness directives should be outside the Simple Subset. The Simple Subset requires that the LHS of an implication be a Boolean. This implies that strong fairness directives (which are equivalent to assumptions of properties in which the LHS of an implication is a non-Boolean property) are outside the Simple Subset. This should be noted in the LRM. [EM 17-May-06]110. Named association of actual/formal parameters. It has been suggested that PSL should support named association of actuals and formals, as an alternative to positional association, in sequence and property instances. This could be supported with the syntax appropriate for a given flavor, or it could be supported using a language-neutral syntax. For PSL within VHDL 200x, it would probably be better to allow VHDL-style named association. [EM 17-May-06]111. Restricting to linear time in assume/assert reasoning. An email received from Moshe Vardi: >For linear time, "assume f, assert g" is equivalent to >"assert f->g". The LRM does require assumptions to be linear, but it >does not require assertions to be linear. > >Mixing linear and branching formulas requires carefully defining the >semantics. See "Modular Model Checking" by Kupferman&V. If f is linear >and g is branching, thanM is not the same as M||A_f |= g. > >I'd suggest requiring that only linear time be used in both assumtions >and assertions in the context of assume/assert reasoning. [CE 23-May-06] 112. Flavors and Portability: portability is relevant only for external (i.e.: not embedded) properties; in there, how much it makes sense to use a flavor to check properties on designs written in another language? A little, if not for legacy code, so my proposal would be to prevent usage of flavor out of embedded code or bound vunits. The only allowed flavor for external properties should be GDL. [AF 8-June-06]113. Inheritance and Vunit reuse: I would just recommend to add two new keywords to the language, to allow inheritance of properties either as assertions or assumptions, enabling exploitation of vunits as "natural" property containers. A point I'm currently reviewing is about whether allowing partial inheritance of properties, in case some of them had already been declared as assertions or assumptions in the inherited vunit, or not, allowing only qualified (assume| assert ) inheritance of fully undeclared property sets. [AF 8-June-06] 114. Overriding, Namespaces: Current overriding rules are dangerous for false positive risks, due to the default binding mechanism. I would propose reviewing the scoping rules, by making everything not explicitly declared global to be locally defined, and to require to explicitate overriding. [AF 8-June-06]115. Definition of a PSL abstract machine: whether we remove flavor, or allow flavors cross-application (e.g.: vhdl flavor to deal with verilog descriptions), and actually even if we just restrict our attention to one single flavor, it would be necessary to build an HDL-independent representation of the DUV, in PSL terms; this is currently delegated to the verification tool, but should instead be coded, in my view, by the LRM, so that any possible added flavor has a clear representation to match with, and any possible implementation of a PSL translator has a flavor independent reference for the DUV. One of first steps along the path to this result is the definition of a sampling semantics. [AF 8-June-06]116. Use Models. There are many ways of using PSL. Since PSL is defined separate from the HDL text to which it relates, PSL vunits can potentially be processed before, after, or along with the corresponding HDL text. Each of these use models has different implications for operations such as name resolution, component/instance binding, scope and visibility, etc. The LRM should make some statement about what use model(s) are expected to be supported, and it should make explicit what the use models imply in these other areas. [EM 2-June-06]117. Formal semantics for built-in functions Define formal sematics for built-in functions, especially for ended(), rose(), fell(). [SR 13-June-06]118. Holds tightly on an infinite path. What is the meaning of "holds tightly" on an infinite path. It should be part of the formal semantics. Explain how these semantics are related to the formal semantics of restrict. [EM 13-June-06]119. portability of vunits between flavors. The current LRM says that "any flavor vunit could be used with any HDL, provided that the signals referenced in the HDL are declared in the vunit." Clarify that only non-Bit signals should be declared in the vunit. [EM 13-June-06]120. Type mismatch in overriding declarations. From Eduard Cerny: The LRM does not explain about type mismatches in overriding declarations. For example, is it an error if the signal names match and the types are different. The alternative could be to treat it as a different variable in a local scope. The LRM does not explain overriding of declarations other than signal declarations. When the sequence or property names are the same in the inheriting and inherited context, is it an error? The rules on pp37 seem to contradict what the rules about inheritance say. For example, rule c on pp 37 mentions "single" declaration in the transitive closure. Why is it in parentheses? Meaning? See (here) for more details. [CE 10-July-06]121. Index range syntax. The IEEE 1850 PSL LRM defines 'Index_Range' as follows: Index_Range ::= LEFT_SYM /finite/_Range RIGHT_SYM | '(' HDL_RANGE ')' This is a bit odd, since the first alternative uses LEFT_SYM and RIGHT_SYM, whereas the second alternative uses '(' and ')' directly. The reason seems to be that HDL_RANGE is only defined for VHDL, and in VHDL, the LEFT_SYM and RIGHT_SYM are '(' and ')' respectively. However, this kind of coupling is inappropriate; it would be better for Index_Range to be defined as Index_Range ::= LEFT_SYM Range_Spec RIGHT_SYM Range_Spec ::= /finite/_Range | HDL_RANGE [EM 11-July-06]122. Subroutine calls on a match of a sequence. Add subroutine calls that are triggered when a match of a prefix of a sequence occures. [SR 11-July-06]123. Add the througout operator Add the throughout operator as in SVA. It is an always version of the within operator. [EM 11-July-06]124. Clock/Data race conditions. The PSL LRM needs to clearly state how clock/data race conditions are handled. see (here) for details. [EM 13-July-06]125. Input-sensitive assertions vs. unclocked assertions. PSL unclocked assertions are expected to evaluate at every cycle of the underlying tool. For combinational assertions, this is acceptable, although it is not necessarily efficient. But for unclocked sequential assertions, for example for modeling untimed logic, it doesn't work very well at all. Instead of evaluating at every tool cycle, it is often more useful (or efficient) to evaluate whenever an input changes, much like the semantics of VHDL processes and Verilog always blocks. It might be possible to do this now, using a Verilog event expression as the clock, e.g., always ({a} |=> {b; c})@(a,b,c); However, this approach clearly creates a race condition between clock and data inputs, and may result in the assertion sampling the old values of the inputs rather than the new values. (This would definitely occur if we apply SVA sampling semantics.) We need a mechanism that allows the assertion to evaluate after a change on any input, using the new value of that input - even in a cycle-based environment. see (here) for more details. [EM 13-July-06]126. Weak and strong assume From the verification guild: For model checker, to provide an option for ignoring possible future assumption violations, is not the same as to provide an option to pass the kind of the semantics to be used: - weak semantics (implies ignoring future assumption violations). - strong semantics (filter all behaviors violating assumptions) for the full discussion, see: (here) [CE 15-Aug-06]127. Forall index range in VHDL The forall operator should support both ascending and descending ranges. In VHDL, ranges are often extracted using the 'range attribute, which can be either ascending or descending (and are more often descending). VHDL designers who will use PSL will want to specify replicated assertions as: forall idx in {my_bus'range}: ... where my_bus'range may be either ascending (e.g., 0 to 31) or descending (e.g., 31 downto 0). In general, it is not possible for the user to know whether a given bus is declared with an ascending or a descending range, because VHDL allows ports to be declared as unconstrained, with the formal constraints being inherited from the actual signal associated with the formal. It is possible to always say forall idx in {my_bus'low to my_bus'high}: ... but since PSL syntax allows use of attribute 'range, it should not result in an error if the range is a descending range. This issue applies to the parameterized 'for' operators as well as to 'forall'. Received on Mon Jul 24 15:56:17 2006 [EM 24-JUL-06]128. Recursion in PSL Does the IEEE 1850 PSL LRM explicitly state whether a property or sequence declaration can contain (directly or indirectly) an instantiation of itself? If not, it should. [EM 13-Sep-06]129. The keyword "for" is missing from the keyword table The parameterized SERE/Property forms in IEEE 1850 PSL added 'for' as a keyword. However, we neglected to add 'for' to the keyword table in clause 4.2.2. The table needs to be updated to include 'for', and we should also review it carefully to see if any other keywords need to be added. [EM 5-Oct-06]130. LRM typos 5.2.3.x From Mike Avery (Cadence) Page 43, clause 5.2.3.9 LRM reads - nondet( {1:2,4,15:18} -- returns a value chosen nondeterministically Should read - nondet( {1:2,4,15:18} ) -- returns a value chosen nondeterministically Page 43, clause 5.2.3.10 LRM reads - nondet(8, {1:2,4,15:18}) -- returns an array of length8, with each element chosen Should read - nondet_vector(8, {1:2,4,15:18}) -- returns an array of length 8, with each element chosen [MA 6-Oct-06]131. Structural contradiction vs. logical contradiction Length matching: the logical contradiction false is treated differently than the structural contradiction. It has been known since Accellera Version 1.01 (where it is mentioned in Appendix B) that there is an inconsistency in the way that structural contradictions are treated vs. the way that logical contradictions are treated. During the past year some ideas for the direction of a solution have been explored, and are described in [EFH05]. We recommend that a future version of the formal semantics base a solution to this problem on [EFH05].Benefit: Language consistency. [CE 19-Nov-06]132. The semantics of r[*0] The semantics of r[*0] are different depending on whether or not r[*0] is standalone or is concatenated with another SERE. There is no good reason for this. We recommend that it be changed, and note that the formal semantics of [EFH05] fix this problem as well.Benefit: Language consistency. [CE 19-Nov-06]133. Suppose we would like to say that signal "a" is independent of signal "b". This could be checked by a cone-of-influence reduction. Currently, there is no way to say such meta-properties in PSL. We recommend that inclusion of such language constructs be considered.Benefit: Add expressive power. [CE 19-Nov-06]134. Adding a new "witness" directive. This will instruct a verification tool to produce a trace on which the property holds (as opposed to "assert", which instructs the tool to verify that it holds on all traces). Benefit: Prevent the coding of ostensible "assertions" which are actually intended to fail. [CE 19-Nov-06]135. The BNF is missing the definition of PSL_Identifier. Note: what is actually missing is not the definition, but the italics (PSL _Identifier) that would indicate that PSL_Identifier is equivalent to Identifier.Benefit: Clarification. [CE 19-Nov-06]136. Adding past operators The PSL language only supports temporal operators allowing to speak about the future. We would like to suggest extending PSL to deal also with past temporal operators. See (here) for more details. [CE 19-Nov-06]137. Clock alignment operator In the clocks paper [EFHMV03] where we suggested the current semantics for the @ operator, we pointed to one problem with it: The characterization of until as a least fixed point is not preserved when multiple clocks are involved. In [F06] we showed that this can be fixed by adding weak/strong alignment operators that takes you to the next clock tick, if the current cycle is not a clock tick. Formally, denoting X![0] and X[0] for the strong and weak alignmentoperators, respectively, we have: w |-c- X![0] f <==> \exists j<|w| s.t. w^{0..j} is a clock tick of c and w^{j..} |-c f w |-c- X[0] f <==> if \exists j<|w| s.t. w^{0..j} is a clock tick of c then w^{j..} |-c- f I suspect these operators are not only of theoretical interest, but are also useful when writing properties involving several clocks. [DF 22-Nov-06]138. PROSYD EU project recommendations for PSL changes See (here) for details. [CE 12-Dec-06]139. Add to the formal parameters of PSL a struct parameter. This can ease the specification, for example, in cases where there is a vunit collecting several properties regarding the same set of parameters and each property refers to some subset of this set. [DF 13-Feb-07]140. Add examples explaining the precedence of the various clocks. In particular, add an example of a vunit that contains both a default clock and an explicit clock for an assertion. Explain which clock has higher priority. Currently the reader has to read sections 5.3 and 5.4 in order to figure this out. [SR 13-Feb-07]140. Implicit parentheses around property instances and parameters. The LRM may not make it clear that property instantiation and parameter substitution is done in such a way that the integrity (and meaning) of the instantiated property or the referenced poperty parameter is maintained. In particular the example at the end of 6.3.3.2, property instantiation, shows a property instance and an equivalent property, but the example does not consider what happens when a property is instantiated within another property, not does it show the equivalent result in parentheses. The LRM should give more examples. For more details see here. [EM 15-Feb-07]141. Passing a module as parameter Phrasing of the point-to-point property for one of PROSYD's case studies was done using as parameters the relevant signals of one master and one slave. Each such property usually involved 5-8 parameters. These parameters were later instantiated in the top-level properties. It would have been much less cumbersome if it was possible to pass as a parameter to the property a slave and a master, rather than the relevant signals of each. This is not possible in PSL, since the allowed parameters are one of the following: Boolean, bit, bitvector, numeric, string, sequence, property. An entire module may not be passed as a parameter. We suggest enhancing the set of allowed parameters to include a predefined module. Benefit: Ease of use. [CE, PROSYD 7-Mar-07]142. Analog extensions: PROSYD deliverable D1.3/2 describes an extension of PSL to allow it to be used in real-time and analog properties. We recommend that the committee consider this extension. Benefit: Applicability to analog designs. [CE, PROSYD 7-Mar-07]143. Counting untils. Extend PSL to allow statements such as "p holds until the 3rd occurrence of q". This property occurs for instance in buffer protocols in which the bus must be granted to a given client until the 3rd transfer has completed. This property is hard to express in PSL. For more details see PROSYD recommendations, p.10, item 4. [CE, PROSYD 7-Mar-07]144. Local Binding and scope: Variables should be visible only in the current vunit and in those inheriting from the current one; transitive closure of inheritance should require to always specify the referenced vunit in case of variable name conflict. For more details see PROSYD recommendations, p.11, item 7. [CE, PROSYD 7-Mar-07]145. Clarifications for nondet() 1. p.43 about nondet(): "nondet( {1:2,4,15:18}" - missing closing parenthesis 2. Clarify what mixtures of ranges and distinct values are allowed in nondet(). [SR 11-Mar-07]146. PSL never and weak/strong operands There is inconsistency in the various references to the operand of "never". see here for details. [EM 23-Mar-07]147. Interpretation of 'and', 'or' in the VHDL flavor The LRM needs to make it clear that "predefined" in item a) in clause 5.2.1 refers only to HDL identifiers that have meaning without (implicit or explicit) declaration. The LRM must also clarify when an expression of the form Bool1 op Bool2 (where op = and/or) should be interpreted as an HDL expression, and therefore op is the HDL operator, and when it should be interpreted as a PSL property, and therefore op is the PSL operator. [EM 17-May-07] --------------------- !-- ----------------------------------------------------------------- -->
Last updated on 28 Nov 2005.