[$ieee-1850] IEEE 1850 PSL - Issues Subcommittee Meeting - 12 Oct 04 - Minutes

IEEE 1850 PSL - Issues Subcommittee Meeting - 12 Oct 04

Acting chair: Erich Marschner

Attendees: Erich, Tej, Avigail, Dana, Johan, Johan, Adriana, Bassam, Andrew

We reviewed and discussed the prioritizations and dispositions of each of the issues, including a few additional issues (total now is 44 issues). Based on average prioritization scores received from 13 respondants, and upon discussion leading to consensus among the meeting attendees, we classified them as follows:

 - Rejected: we should not pursue these at all.
 - LRM: these are simple enough to pass to the LRM subcommittee immediately
 - Extensions: these are complex enough to require discussion in the Extensions subcommittee
 - Out of Scope: these are considered out of scope w.r.t. the IEEE 1850 effort

The results were as follows:

Rejected - 14, 16, 18, 22, 24, 28, 29, 32, 35.
LRM - 1, 2, 3, 4, 6, 13, 27, 36, 37
Extensions - 5, 7, 8, 9, 10, 11, 12, 15, 17, 19, 20, 23, 26, 30, 31, 33, 38, 39, 40, 41, 42, 43, 44
Out of Scope - 34

In addition, issues 21 and 25 were left unresolved - one person voted to not do these, but others felt they had at least medium priority. After some discussion, we left them unresolved and went on to other issues. Given that we couldn't agree to reject these, and they clearly are not LRM issues, I've decided to consider them Extensions.

Issues 36-44 were not listed in the original Issues list. These issues are listed below. An updated Issues list will be posted to the web, containing all issues received to date. (Harry Foster is maintaining the web site. The update will be posted when he returns from traveling.)

Additional Issues
=============

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

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).

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 07 Oct 04]

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 08 Oct 04]

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]

44. Need to define a SystemC flavor of PSL, to allow PSL to be used in system-level models. [EM 11Oct04]

===================================================================
Received on Tue Oct 19 07:34:35 2004