Tej,
I think sections 6.1.3, 6.1.4 and 6.2.4 should not be removed but rather
that the changes be made in these sections. This way it is clearer for
example that
a named property instantiation is also an FL_PROPERTY.
Related to this, you write:
Formal types Actual Expression type
sequence Sequence expression (refer to 6.1.2)
property FL property expression (refer to 6.2.1)
It is not clear here that a named sequence (property) instantiation can be
used as the actual parameter when the formal parameter is a sequence
(property).
Regards,
Sitvanit
Sitvanit Ruah
Formal Verification and Testing Technologies Group
IBM Haifa Research Laboratory
Tel: 972-3-640-1697 email: sitvanit@il.ibm.com
|---------+---------------------------------->
| | "Singh, Tej" |
| | <tej_singh@mentorg.com>|
| | Sent by: |
| | owner-ieee-1850-extensi|
| | ons@eda.org |
| | |
| | |
| | 03/01/2005 20:28 |
|---------+---------------------------------->
>-----------------------------------------------------------------------------------------------------------|
| |
| To: <ieee-1850-extensions@eda.org> |
| cc: |
| Subject: Group D Issues : Formal Proposal |
>-----------------------------------------------------------------------------------------------------------|
Hi All,
Please consider the following formal proposal to take care of issue group D
in http://www.eda.org/ieee-1850/Issues/Issues.html.
In my informal proposal (
http://www.eda.org/ieee-1850/ieee-1850-extensions/hm/0085.html), I had
outlined three possible solutions.
In the last meeting, it was decided that it should be a mix of proposal 1
and proposal 3.
Outline
a) Add the following four formal types in addition to existing
boolean | sequence | property
bit
bitvector
numeric
string
b) const is no longer a type but a type qualifier. const is optional and
can be used to qualify any Boolean type. If there is no type with const,
numeric is assumed.
c) In addition to PSL formal types, which are language neutral and exist in
all flavors, formals can be of HDL_VARIABLE_TYPE. Such types have to
qualified with the hdltype keyword so that there is no clash between PSL
types and flavor types (e.g. between PSL bit and VHDL bit).
Note - This proposal is backward compatible to LRM 1.1
Proposal
Remove sections 6.1.3, 6.1.4 and 6.2.4
Create a new section
6.3 Named Declarations
A given temporal expression may be applicable in more than one part of the
design. In such a case, it is convenient to be able to define the
expression once and refer to the single definition wherever the expression
applies. Declaration and instantiation of named declaration provide this
capability.
Create box
--------------------------------------------------------------------------------------------------------------------------
PSL_Declaration ::=
Sequence_declaration
| Endpoint_declaration
| Property_declaration
Sequence_declaration ::=
sequence PSL_Identifier [ ( Formal_Parameter_List ) ] DEF_SYM Sequence
;
Endpoint_declaration ::=
endpoint PSL_Identifier [ ( Formal_Parameter_List ) ] DEF_SYM Sequence
;
Property_declaration ::=
property PSL_Identifier [ ( Formal_Parameter_List ) ] DEF_SYM Property
;
Formal_Parameter_List ::=
Formal_Parameter {; Formal_Parameter }
Formal Parameter ::=
Param_Type PSL_Identifier {, PSL_Identifier}
Param_Type ::=
const
| [ const ] Boolean_Type
| sequence
| property
Boolean_Type ::=
HDL_Type
| PSL_Boolean_Type
PSL_Boolean_Type ::= boolean | bit | bitvector | numeric | string
HDL_Type ::=
hdltype HDL_VARIABLE_TYPE
-----------------------------------------------------------------------------------------------------------------
Informal Semantics
The PSL_Identifier following the keyword sequence/endpoint/property in the
PSL_Declaration is the name of the declaration. The PSL_Identifiers given
in the formal parameter list are the names of the formal parameters of the
named declaration.
Restriction
The name of the declaration shall not be same as any other declaration in
the same verification unit.
NOTE--There is no requirement to use formal parameters in a declaration.
The declaration expression may refer directly to signals in the design as
well as to formal parameters.
6.3.1 Formals
A named declaration can optionally specify a list of formal parameters that
may be referenced in the declaration expression. A declaration
instantiation creates an instance of the named declaration and provides
actual expressions for formal parameters.
Formals of Boolean_type can be optionally qualified with const. The actual
expression that maps to a const formal shall be statically computable. If a
const formal has no type, the formal shall be of numeric type.
6.3.1.1 PSL Formal types
PSL defines formal types that are language flavor neutral. Refer to the
table below for PSL defined types and the actual expression types that map
to those formals .
Formal types Actual Expression type
boolean Boolean expression (refer to 5.1.2)
bit Bit expression (refer to 5.1.1)
bitvector BitVector expression (refer to 5.1.3)
numeric Numeric expression (refer to 5.1.4)
string String expression (refer to 5.1.5)
sequence Sequence expression (refer to 6.1.2)
property FL property expression (refer to 6.2.1)
Many-to-one mapping from PSL types to HDL types can result in type
ambiguity issues in strictly typed languages like VHDL.
Example
sequence s (boolean b0, b1) is {b0 = b1};
In VHDL flavor, both bit and std_ulogic map to boolean type, but it is an
error to pass expressions of type bit and std_ulogic to formals b0 and b1
respectively in this example if the '=' operator is not defined for
operands of type bit and std_ulogic.
6.3.1.2 HDL Formal Types
In addition to language neutral types, PSL allows formal types that are HDL
flavor specific. If an HDL type can be used in a formal parameter
declaration of a subroutine defined in the HDL flavor, it can be used as a
formal type in a PSL named declaration. This includes user defined types.
The actual to formal mapping rules are the same as for subroutines in that
flavor.
HDL formal types have to be qualified with the hdltype keyword.
Example
VHDL flavor
sequence color_is_red (hdltype COLOR_ENUM c) is {c = "RED"};
sequence slope_is_1 (hdltype COORDINATE_RECORD c) is {(c.x / c.y) = 1};
System Verilog flavor
sequence color_is_red (hdltype COLOR c) = {c == RED};
sequence slope_is_1 {hdltype COORDINATE_STRUCT c) = {(c.x / c.y) == 1};
6.3.2 PSL Declarations
6.3.2.1 Sequence Declaration
A sequence declaration defines a sequence and gives it a name.
Restrictions
Formal parameters of a sequence declaration cannot be of type property.
Example
Move the example in 6.1.3.1 over here
6.3.2.2 Endpoint declaration
An endpoint declaration defines an endpoint for a given sequence and gives
the endpoint a name. An endpoint is a special kind of Boolean-valued
variable that indicates when an associated sequence completes.
Restrictions
Formal parameters of an endpoint declaration cannot be of type property.
Example
Move example from 6.1.4.1 here
6.3.2.3 Property Declaration
A property declaration defines a property and gives it a name.
Example
Move example for 6.2.4.1 here
6.3.3 Named Declaration Instantiation
An instantiation of a PSL declaration creates an instance of the named
declaration and provides actual expressions for formal parameters. The
mapping of actual expression to formal is by position.
Restrictions
For each formal parameter of the declaration, the instantiation shall
provide a corresponding actual expression. For a const formal parameter,
the actual expression shall be a statically computable expression. The
expression type of the actual parameter shall map to the respective formal
type as per Section 6.3.1. Further, the expression obtained after replacing
all formals with the actual expression in the declaration expression shall
be a legal expression in the language flavor.
6.3.3.1 Sequence Instantiation
A sequence instantiation, shown in box XX, creates an instance of a named
sequence.
In box
---------------------------------------------------------------------
Sequence ::=
Sequence_Instance
Sequence_Instance ::=
sequence_Name [ ( Actual_Parameter_List ) ]
Actual_Parameter_List ::=
Actual_Parameter { , Actual Parameter }
--------------------------------------------------------------------------
Informal Semantics
Move informal semantics from 6.1.3.2 here
Example
Move example from 6.1.3.2 here
6.3.3.2 Endpoint Instantiation
An endpoint instantiation,shown in box XX, creates an instance of a named
endpoint.
In box
---------------------------------------------------------------------------
Boolean ::=
boolean_HDL_or_psl_Expression
boolean_HDL_or_psl_Expression ::=
endpoint_Name [ ( Actual_Parameter_List ) ]
-----------------------------------------------------------------
Informal semantics
Move informal semantics from 6.1.4.2 here
Example
Move example from 6.1.4.2 here
6.3.3.3 Property Instantiation
A property instantiation, shown in box XX, creates an instance of a named
property.
In box
-----------------------------------------------------------------------------------------
FL_Property ::=
property_Name [ ( Actual_parameter_list ) ]
-----------------------------------------------------------------------------------
Informal semantics
Move informal semantics from 6.2.4.2 here
Example
Move example from 6.2.4.2 here
################################################################################
Changes to Appendix A
A.3.2 Flavor macros
Add the following rule
Flavor Macro HDL_VARIABLE_TYPE =
System Verilog : data_type
/ Verilog : task_port_type | reg [signed] [range]
/ VHDL : subtype_indication
/ GDL :
A.4.2 PSL Declaration
Replace Param_Type with
Param_Type ::=
const
| [ const ] Boolean_Type
| sequence
| property
Boolean_Type ::=
HDL_Type
| PSL_Boolean_Type
PSL_Boolean_Type ::= boolean | bit | bitvector | numeric | string
HDL_Type ::=
hdltype HDL_VARIABLE_TYPE
Replace Actual_Parameter with
Actual_Parameter ::=
HDL_EXPR | Property | Sequence
Received on Tue Jan 4 05:44:34 2005
This archive was generated by hypermail 2.1.8 : Tue Jan 04 2005 - 05:44:41 PST