RE: [sv-ac] formal types proposal

Hi Lisa,
 
I skimmed this a bit and here's some food for thought on what strikes
me. I think the only 2 *types* to add (detail below) are sequence,
property, and we also need to add clearly (restate) what (built-in)
operations are allowed on these types, and what type-casting is allowed
i.e. between seq/prop. 
 
Const is not a type it is a qualifier (already in language) that goes
before a type (bit etc...), so we should use it as such. Void is highly
inadequate, may be a "self" is more meaningful and again here this is
not a type it is a qualifier. This can possibly be used later for other
things in language. Also I would feel better about backward
compatibility as I stated before if this is available, it makes porting
much easier with this additional tag qualifier.
 
Event also bothers me note that we state that events cannot be operands
of assertions. Moreover it is inadequate -- we've already established we
are passing an event_expression, so again a qualifier is what's needed
here (particularly since sequences fall under this category too and they
have a type), I can't come up with a good name now, some variant of
clocking_expr or event_expr should do the trick, preferably if there is
some "precedent" of sorts in the LRM.
 
Looping back around, seq/prop are not qualifiers but are indeed "types"
with their own operations etc... and the return type is indeed another
seq/prop. In fact one can think of these types as built-in classes,
indeed they are, and again we need to organize the information in LRM
operations/casting etc ... to reflect this.
 
Hope this helps. Take home point, distinction between type and type
qualifiers.
 
Thx.
-Bassam.
 

________________________________

From: owner-sv-ac@eda-stds.org [mailto:owner-sv-ac@eda-stds.org] On
Behalf Of Lisa Piper
Sent: Thursday, June 29, 2006 10:22 AM
To: sv-ac@verilog.org
Subject: [sv-ac] formal types proposal



I am choosing to keep this separate from the 928 proposal until the
basics are agreed to, then I will merge the two.  I think we all agree
on 928 (I did change "type name" back to just "type" as requested but
other than that it is the same).

 

The following would be merged with 928.  The text in blue in A.2.10
would be added to 928.  The text shown below for 17.6.1 and 17.11.1
would become the text for 928. 

 

Lisa

 

ps By the way, I will not have access to email at all next week and will
have limited hours tomorrow.

 

 

PROPOSAL OVERVIEW:

Formal arguments to properties and sequences are currently defined for
some but not all possible types. The objective of this proposal is to
expand the list of types so that everything that is allowed to be passed
as an argument can be passed as a typed argument. 

The standard currently defines only operand types (per 17.4.1).
Arguments that are not covered by the current type definitions include
property, sequence, repeat and delay arguments, and events.  The "void"
type is introduced to allow for using arguments that do not have any
data type restrictions to be mixed freely with those that do. 

Types are proposed as follows:

o       operand types except noninteger types(shortreal, real and
realtime), string, event, chandle, class, associative arrays, dynamic
arrays (refer to 17.4.1)

o       sequence: sequence instances are passed as type sequence

o       property:  property instances are passed as type property

o       event: used to pass clocking event  



*	void: used when there are no data type restrictions, meaning
that any type is acceptible. The implicit type (that of the declaration
of the argument) is used for any semantic checks.  This is equivalent to
listing the argument prior to any typed arguments. 

o       const: used to pass delay and repetition numbers. These must be
a positive integer_type (existing definition of integer_type is shown in
A.2.10 below for convenience) value that can be statically computed at
compilation time.  Consistent with 6.3.2.1, the "$" can be assigned to
formal arguments of integer_types when used where a $ is allowed. (in a
sense this is an integer_type with a const qualifier, however you will
never get a type error regardless of what integer_type is used because
SV will expand or truncate the value accordingly. So adding the specific
integer_type provides no value - might as well just use the keyword
const)

It is specified that if the user specifies a type, that type is enforced
by semantic checks. Furthermore, "const", "void", or no type must be
used for delay and repetition numbers.  (Note: this is not totally
backwards compatible but is the right thing to do for the language.
Existing untyped designs are backwards compatible. Alternatively, for
backwards compatibility, I would state "A user could choose to use other
types for delay and repetition numbers, but the checks would not be as
complete and less information is conveyed to the user. Compilers would
not require const for repetition and delay numbers, though the arguments
would still need to be const."

The following describes the detailed changes that will be required in
the standard.  All changes are RELATIVE to the revisions of Mantis 928
for A.2.10.  Text sections replace the existing text.  

 

============================================================

A.2.10 Assertion declarations

property_actual_arg ::=

sequence_actual_arg 

| property_instance

 

property_formal_type ::= 

            sequence_formal_type

            | property

 

sequence_formal_type ::= 

             data_type_or_implicit

             | void

             | sequence

             | event

             | const [integer_type]

 

sequence_actual_arg ::=

event_expression

 

                              38

event_expression ::=

[ edge_identifier ] expression [ iff expression ]

| sequence_instance [ iff expression ]

| event_expression or event_expression

| event_expression , event_expression

| ( event_expression )

 

integer_type ::= integer_vector_type | integer_atom_type

integer_atom_type ::= byte | shortint | int | longint | integer | time

integer_vector_type ::= bit | logic | reg

 

Details:

17.6.1 Typed formal arguments in sequence declarations

Formal arguments of sequences can optionally be typed. Typed formal
arguments are recommended because they enable compilers to do additional
semantic checks and convey to the user what is expected. To declare a
type for a formal argument of a sequence, it is required to prefix the
argument with a type. A formal argument that is not prefixed by a type
shall be untyped will inherit the type of the argument's declaration for
the purpose of semantic checks.  When a type is specified, that type is
enforced by semantic checks. Furthermore, when a type is
specified,"const" or "void" must be used for delay and repetition
numbers.  

 

Exporting values of local variables through typed formal arguments is
not supported.

 

The supported data types for sequence formal arguments are the types
that are allowed for operands in assertion expressions (see 17.4.1). 

A typed formal argument can be defined to accept anything that is
defined as allowed for the type name shown in Table x below:

 

Table x.  SVA formal argument types

Type 

Actual Argument

integer, bit, reg, ...

(all operand types)

All arguments that are consistent with the specified data types as
defined in 17.4. ( 17.4.1 defines operand types as all data types except
noninteger types(shortreal, real and realtime), string, event, chandle,
class, associative arrays, dynamic arrays.)

const 

Positive integer_type that is statically computed at compile time. Used
for delay and repetition arguments.  Consistent with 6.3.2.1, the "$"
can be assigned to formal arguments of type const. A formal argument to
which $ is assigned shall only be used wherever $ can be specified as a
literal constant.  

event

A clocking event expression

sequence

Sequence Instance (refer to 17.6) 

property*

Property Instance (refer to 17.11) 

void

Used to specify there are no data type restrictions, meaning that any
type is acceptable. The implicit type (that of the declaration of the
argument) is used for any semantic checks.

 

*Only properties may not have a property instance as an argument.

 

The assignment rules for assigning actual argument expressions to formal
arguments, at the time of sequence instantiation, are the same as the
general rules for doing assignment of a typed variable with a typed
expression (see Clause 4).

 

For example, two equivalent ways of passing arguments are shown below.
The first has untyped arguments, and the second has typed arguments
where x and y are of type bit and z is of type byte.:

 

sequence rule6_with_no_type(x, y, z);

##1 x ##[2:10] y ##1 z == 8'hFF;

endsequence

 

sequence rule6_with_type(bit x, y, byte z);

##1 x ##[2:10] y ##1 z == 8'hFF;

endsequence

 

The "const" type would be used to pass delay and repetition values.  For
example, two equivalent ways of passing delay and repetition arguments
are shown below:

 

            sequence delay_arg_example ( const delay1, delay2, min,
max);

            x  ##delay1   y[*min:max]   ##delay2  z;

            endsequence

 

            `define my_delay=2;

            cover property ( delay_arg_example ( `my_delay, `my_delay-1,
3, $) );

 

which is equivalent to:

 

            cover property ( x  ##2  y[*3:$]   ##1  z);

 

Parentheses are implicit for passing complex expressions as arguments.
Const formal arguments that consist of complex expressions must evaluate
to a value of the specified type named at compile time.   

 

The following shows an example of passing clocking events:

 

            sequence event_arg_example ( event  clock )   

            @(clock) x ##1 y;

            endsequence

            

             cover property ( event_arg_example(posedge clk));  

 

is equivalent to:

 

            cover property ( @(posedge clk) x ##1 y));

Similarly, a sequence instance is passed with a type name of "sequence",
and a property instance argument is passed with a type of "property".
There are two ways to achieve implicit typing of argurments.  The first
is to list all arguments first in the list prior to specifying any type.
The second is to use the "void" type.



Another example, in which a local variable is used to sample a formal
argument, shows how to get the effect of "pass by value". Pass by value
is not currently supported as a mode of argument passing.

sequence foo(bit a, bit b);

bit loc_a;

(1'b1, loc_a = a) ##0

(t == loc_a) [*0:$] ##1 b;

endsequence

 

 

17.11.1 Typed formal arguments in property declarations

Formal arguments of properties can optionally be typed. Typed formal
arguments are recommended because they enable compilers to do additional
semantic checks and convey to the user what is expected. To declare a
type for a formal argument of a property, it is required to prefix the
argument with a type. A formal argument that is not prefixed by a type
shall be untyped will inherit the type of the argument's declaration for
the purpose of semantic checks. When a type is specified, that type is
enforced by semantic checks. Furthermore,when types are specified,
"const" or "void" must be used for delay and repetition numbers.  

 

The supported data types for property formal arguments are the types
that are allowed for operands in assertion expressions (see 17.4.1).
those of sequences with the addition of the property type. The
assignment rules for assigning actual arguments to formal arguments, at
the time of property instantiation, are the same as the general rules
for doing assignment of a typed variable with another typed expression
(see Clause 4).

 

For examples of using formal arguments, refer to section 17.6.1.

 

For example, below are two equivalent ways of passing arguments. The
first has untyped arguments, and the second has typed arguments:

 

property rule6_with_no_type(x, y);

##1 x |-> ##[2:10] y;

endproperty

 

property rule6_with_type(bit x, bit y);

##1 x |-> ##[2:10] y;

endproperty