Group F - First Draft LRM Changes, slightly amended

The following is the first draft of changes to address Group F, with a minor correction regarding when interpretations are applied (to deal with the back-conversions from PSL type class values to HDL data types when PSL expressions, built-in functions, and endpoints are used in an HDL context).

1. Clarify how values of PSL type classes Boolean and Numeric are mapped back to HDL-specific types in cases in which PSL constructs (endpoints and built-in functions) can appear in an HDL expression.

Summary:
 - In VHDL:
    - Boolean => VHDL 'STD.Standard.Boolean'
    - Numeric => VHDL 'STD.Standard.Integer'
- In Verilog:
    - Boolean => a single bit value
    - Numeric => an array of bits of the length required to represent the (unsigned) value
- in SystemVerilog:
    - Boolean => type 'logic'
    - Numeric => type 'int'
- in SystemC (assuming that we add this flavor):
    - Boolean => built-in data type 'bool'
    - Numeric => built-in data type 'unsigned int'

Details:

- in 5.1.2, Boolean expressions, the following paragraph already appears:

  "The return value from a PSL expression or built-in function that returns a Boolean value is of the appropriate type for the context. For Verilog, the return value is of the built-in logic type; for SystemVerilog, the return value is of the built-in type logic, for VHDL, the return value is of type /STD.Standard.Boolean/."

This needs to be extended to cover endpoints also, so the first part should be changed to

  "The return value from an endpoint, a PSL expression, or built-in function that returns a Boolean value ..."

If we adopt a SystemC flavor, this will have to be extended to say also

  "...; for SystemC, the return value is of built-in type bool."

- in 5.1.4, Numeric expressions, the following paragraph already appears:

  "The return value from a PSL built-in function that returns a Numeric value is of the appropriate type for the context. For Verilog, the return value is a vector of the built-in logic type; for SystemVerilog, the return value is of the built-in type int; for VHDL, the return value is of type STD.Standard.Integer."

If we adopt a SystemC flavor, this will have to be extended to say also

  "...; for SystemC, the return value is of built-in type unsigned int."

2. Clarify the return type of prev().

I don't think any change is necessary here. The LRM already says that prev(s) returns a previous value of s, and clearly any value of s would be of the type of s.

3. Add VHDL 'H' and 'L' to the definitions of True and False, respectively.

Details:

- in Definition 3.1.20 False, change the third sentence, which starts
  
   "In the VHDL flavor, he values STD.Standard.Boolean’(False) and STD.Standard.Bit’(‘0’),
    as well as the values IEEE.std_logic_1164.std_logic’(‘0’), ...

  to read

   "In the VHDL flavor, the values STD.Standard.Boolean’(False) and STD.Standard.Bit’(‘0’),
    as well as the values IEEE.std_logic_1164.std_logic’(‘0’), IEEE.std_logic_1164.std_logic’(‘L’), ...

*** Note also the typo in the fifth word of the original text, corrected above - 'he' should be 'the' ***

- in Definition 3.1.51 True, change the third sentence, which starts

    "In the VHDL flavor, the values |STD.Standard.Boolean'(True)|, |STD.Standard.Bit'('1')|,
     and |IEEE.std_logic_1164.std_logic'('1')| are all interpreted ..."

  to read

    "In the VHDL flavor, the values |STD.Standard.Boolean'(True)|, |STD.Standard.Bit'('1')|,
     |IEEE.std_logic_1164.std_logic'('1')|, and |IEEE.std_logic_1164.std_logic'('H')| are all interpreted ..."

*** Also, make the definitions of True and False consistent w.r.t. the use of Courier font for HDL type names - the names are in Courier in the definition of True, but in the regular font in the definition of False. ***

4. Clarify that interpretation of an HDL expression as an expression of a particular PSL type class occurs only when necessary, i.e., at the point where the Temporal Layer requires an expression of a given type class.

- in clause 5.1, Expression type classes, split the first (only) paragraph before and after the box, and extend it to read as follows:

  "Five classes of expression are distinguished in PSL: Bit, Boolean, BitVector, Numeric, and String expressions. Each of these correspond to a set of specific data types in the underlying HDL context, and an interpretation of the values of those data types."

  "Some PSL built-in functions take operands that may be of any HDL data type or PSL type class. In such cases, there is no interpretation of type or values involved."

[Box defining AnyType ::= HDL_or_PSL_Expression ]

  "Other PSL built-in functions and expressions, and PSL temporal layer constructs, require operands that belong to specific type classes. In such a case, if an HDL expression appears in a location at which the PSL grammar requires an expression of a specific PSL type class, then the value of the HDL expression will be interpreted as a value of a corresponding PSL type class, as described below."

  "PSL expressions, built-in functions, and endpoints can be used in an HDL context, either in the modeling layer or in an HDL expression. In such a case, the value of the PSL type class returned by the PSL expression, built-in function, or endpoint is converted back to a specific HDL data type, as described below."

  "If an HDL expression appears immediately within an HDL context, e.g., as a subexpression within another HDL expression, then neither the interpretation of HDL expression values as values of a PSL type class, nor the conversion of values of a PSL type class back to values of an HDL data type, apply to such a case."
Received on Sat Jan 8 20:38:45 2005