Group F - First Draft LRM Changes

The following is a first draft of changes to address Group F.

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 cases, if an HDL expression appears in the location at which the PSL grammar requires an expression of a specific type class, then the type and values of the HDL expression will be interpreted as specified in the following." The interpretations described herein do not apply to an HDL expression that appears immediately within an HDL context, e.g., as a subexpression within another HDL expression."
Received on Sat Jan 8 20:01:37 2005