[$ieee-1850] IEEE 1850 PSL - Some Additional Issues

36. Need to clarify whether ‘replication’ associated with forall actually involves creation of multiple copies of the assertion. [BC 5Oct04]

37. 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. 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. 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. 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. 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. 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. 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]
Received on Tue Oct 12 09:13:45 2004