All: I have updated the proposal for 1668 in response to comments from Ed Cerny and Jiang Long. I incorporated Ed's suggestion to replace $fell(a) by !a in one of the examples. I have tried to address Ed's quation regarding empty match and all of Jiang's concerns. Of the latter, the toughest one was to account for the local variable declaration assignments in Annex E. If v = e is the declaration assignment, then for a sequence S we want to prepend (*) (1, v=e) ##0 S This is fine unless S admits empty match, and then things get complicated. I have been thinking about this for a while and have been unable to come up with a good formal description that allows S to admit an empty match. My best attempt was (S intersect 1[*0]) // S matches empty, no declaration assignment or ((1, v=e) ##0 S) // non-empty match of S fused with declaration assignment but this does not give the right result from the recursive flow definitions. If you know how to solve this problem, now is the time to speak up. Lacking an acceptable solution, I decided to be more conservative and forbid instances of S that admit empty match if S has a local variable declaration assignment. Then (*) works as a formal rewrite rule without "secretly" throwing away empty matches. This also leaves open the possibility of relaxing the restriction if we find an acceptable solution. For properties, the situation is not as tricky because local variables do not flow out of them. If P is satisfied by the empty word, then we can use (1, v=e) |-> (P) to account for the declaration assignment. Otherwise, we use the dual, overlapping "followed by", which we currently have to write as not ((1, v=e) |-> not(P)) Best regards, John H. -- This message has been scanned for viruses and dangerous content by MailScanner, and is believed to be clean.
Proposal for Mantis 1668: Local Variable Initializers
The goal of this proposal is to allow an initialization assignment to be written as part of the declaration of a local variable in either a sequence or a property declaration. The intended semantics is that declaration assignments be performed in order at the beginning of each evaluation attempt of an instance of the named sequence or property.
In order to simplify the semantics, declaration assignments are not allowed in a named sequence that has an instance that admits an empty match. This allows a declaration assignment v = e in a named sequence to be accounted for formally by prepending (1,v = e) ##0. The situation with declaration assignments in named properties is simpler because local variables do not flow out. Either (1,v = e) |-> or its dual (using overlapping “followed by”) can be used, according as the instance of the property is or is not satisfied by the empty word. For both sequences and properties, instances need to be considered because preprocessing, parameter substitution, and argument substitution could all affect whether the empty word matches or satisfies.
In the proposed Syntax 17-13, the subroutine_call option for sequence_match_item is replaced by an ellipsis because that feature is not discussed in this section.
This proposal clarifies, in alignment with Mantis 1704, that
a local variable assignment cannot be attached to a sequence that admits an
empty match.
The description of the declaration assignments involves expansion of the initial description of local variables. Parts of the text of 17.8 have been rewritten and expanded to improve clarity. For example, there was before no clear description of when a local variable can be referenced and the relationship between a local variable’s “not flowing” and its “becoming unassigned”.
17.8, p. 259: REPLACE
The dynamic creation of a variable and its assignment is achieved by using the local variable declaration in a sequence or property declaration and making an assignment in the sequence.
[
sequence_expr ::=
...
| ( expression_or_dist {, sequence_match_item } ) [ boolean_abbrev ]
| ( sequence_expr {, sequence_match_item} ) [ sequence_abbrev ]
...
sequence_match_item ::=
operator_assignment
| inc_or_dec_expression
| subroutine_call
]
Syntax 17-12 -- Variable assignment syntax (excerpt from Annex A)
The type of variable is explicitly specified. The variable can be assigned at the end point of any syntactic subsequence by placing the subsequence, comma separated from the sampling assignment, in parentheses. For example, if in
a ##1
b[->1] ##1 c[*2]
it is desired to assign x = e at the match of b[->1], the sequence can be rewritten as
a
##1 (b[->1], x = e) ##1 c[*2]
The local variable can be reassigned later in the sequence, as in
a
##1 (b[->1], x = e) ##1 (c[*2], x = x + 1)
For every attempt, a new copy of the variable is created for the sequence. The variable value can be tested like any other SystemVerilog variable.
Hierarchical references to a local variable are not allowed.
WITH
The dynamic creation of a local variable is achieved by using an assertion variable declaration within the declaration of a named sequence or property (see 17.11).
[
assertion_variable_declaration ::=
var_data_type list_of_variable_decl_assignments ;
]
Syntax 17-12 -- Assertion variable declaration syntax (excerpt from Annex A)
The data type of an assertion variable declaration shall be specified explicitly. The data type is followed by a comma-separated list of one or more identifiers with optional declaration assignments. If present, a declaration assignment is used to place an initial value in the corresponding local variable. The initial value is defined by an expression, which need not be constant. If an instance of a named sequence has at least one local variable with a declaration assignment, then the body sequence expression of that instance must not admit an empty match.
At the beginning of each evaluation attempt of an instance of a named sequence or property, a new copy of each of its local variables is created and, if present, the corresponding declaration assignment is performed. Declaration assignments are performed in the order that they appear in the sequence or property declaration. Non-local variables appearing in the expression of a declaration assignment to a local variable are evaluated using the Preponed values from the time slot in which the evaluation attempt begins. The expression of a declaration assignment to a local variable can refer to a previously declared local variable. In this case the previously declared local variable must itself have a declaration assignment, and the initial value assigned to the previously declared local variable is used in the evaluation of the expression assigned to the current local variable. Local variables do not have default initial values. A local variable without a declaration assignment is unassigned at the beginning of the evaluation attempt.
For example, at the beginning of an evaluation attempt of an instance of
sequence s;
logic u, v = a, w = v || b;
...
endsequence
the assignment of a to v is performed first and the assignment of v || b to w is performed second. The local variable u is unassigned at the beginning of the evaluation attempt.
Local variables can be assigned and re-assigned within the body of the sequence or property in which they are declared.
[
sequence_expr ::=
...
| ( expression_or_dist {, sequence_match_item } ) [ boolean_abbrev ]
| ( sequence_expr {, sequence_match_item} ) [ sequence_abbrev ]
...
sequence_match_item ::=
operator_assignment
| inc_or_dec_expression
…
| subroutine_call
]
Syntax 17-13 -- Variable assignment syntax (excerpt from Annex A)
[Note to
editor: all subsequent syntax box
numbers in Section 17 must be adjusted.]
One or more local variables can be assigned at the end point of a syntactic subsequence by placing the subsequence, comma separated from the list of local variable assignments, in parentheses. At the end of any non-empty match of the subsequence, the local variable assignments are performed in the order that they appear in the list. For example, if in
a
##1 b[->1] ##1 c[*2]
it is desired to assign x = e and then y = x && f at the match of b[->1], the sequence can be rewritten as
a
##1 (b[->1], x = e, y = x && f) ##1 c[*2]
A local variable can be reassigned later in the sequence, as in
a ##1 (b[->1], x = e, y = x &&
f) ##1 (c[*2], x &= g)
The subsequence to which a local variable assignment is attached must not admit an empty match. For example, the sequence
a ##1 (b[*0:1], x = e) ##1 c[*2] // illegal
is illegal because the subsequence b[*0:1] can match the empty word. The sequence
(a ##1 b[*0:1], x = e) ##1 c[*2] // legal
is legal because the concatenated subsequence a ##1 b[*0:1] cannot match the empty word.
A local variable can be referenced within the sequence or property in which it is declared. The structure of the sequence or property must guarantee that the local variable has been assigned a value prior to the point at which the reference is made. The prior assignment can be a declaration assignment or an assignment attached to a subsequence. There is an implicit reference associated with the use of an inc_or_dec_operator or an assignment operator other than “=”. Therefore, a local variable must have been assigned a value prior to being updated with an inc_or_dec_operator or with an assignment operator other than “=”.
Under certain circumstances, a local variable that is assigned can later become unassigned. If a local variable does not flow out of a subsequence (see below), then the local variable is unassigned at the end of that subsequence, regardless of whether it was assigned a value prior to that point. The local variable cannot be referenced after the point from which it does not flow until after it has again been assigned a value. See Annex E for precise conditions defining local variable flow.
Hierarchical references to a local variable are not allowed.
REMARK: Jiang Long asked about the sampling point for local variable initialization, so I added the following sentence: “Non-local variables appearing in the expression of a declaration assignment to a local variable are evaluated using the Preponed values from the time slot in which the evaluation attempt begins.” I also added the language clarifying how a reference to a previously declared local variable is evaluated within the expression of a declaration assignment.
Section 17.8, p.
260. REPLACE
Local variables can be written on repeated sequences and accomplish accumulation of values.
sequence rep_v;
int
x;
`true,x
= 0 ##0
(!a [*0:$] ##1 a, x = x+data)[*4] ##1 b
##1 c && (data_out == x);
endsequence
WITH
Local variable assignments can be attached to the operand sequence of a repetition and accomplish accumulation of values.
sequence rep_v;
int
x = 0;
(a[->1], x += data)[*4] ##1 b ##1 c && (data_out == x);
endsequence
An accumulating local variable can be used to count the number of times a condition is repeated, as in the following example:
sequence count_a_cycles;
int
x;
($rose(a), x = 1)
##1 (a, x++)[*0:$] ##1 !a && (x <= MAX);
endsequence
RATIONALE: The original rep_v example showed how to work around lack of local variable declaration assignments and is awkward with the feature added. Also, the idiom !a[*0:$] ##1 a is more compactly written as a[->1]. The second example shows a useful idiom and illustrates the use of an inc_or_dec_expression to update a local variable. In the second example, $fell(a) has been changed to !a as suggested by Ed Cerny.
Section 17.8, p.
260. REPLACE
The local variables declared in one sequence are not visible in the sequence where it gets instantiated.
WITH
The local variables declared within a sequence or property are not visible in the context where the sequence or property is instantiated.
RATIONALE: The beginning of the proposal discusses local variables for both sequences and properties.
Section 17.8, p. 262. CHANGE
A local
variable may have been assigned a value before the start of the evaluation of
the composite sequence. Such a local
variable is said to flow in to each of the operand sequences.
TO
A local
variable may have been assigned a value before the start of the evaluation of
the composite sequence, either from an initial
declaration assignment or from an assignment attached to a preceding
subsequence. Such a local
variable is said to flow in to each of the operand sequences.
RATIONALE: To clarify that a declaration assignment
counts as an assignment “before the start of evaluation of the composite
sequence”, as suggested by Jiang Long.
Section 17.8, p. 262. CHANGE
If these conditions are satisfied, then the local variable is said to flow out of the composite sequence. An intuitive description of the conditions for local variable flow follows:
TO
If these conditions are satisfied, then the local variable is said to flow out of the composite sequence. Otherwise, the local variable is unassigned at the end of the composite sequence. An intuitive description of the conditions for local variable flow follows:
RATIONALE: To complete the correlation of the concepts of “not flowing” and “becoming unassigned”.
Syntax 17-4, p.
240. CHANGE
assertion_variable_declaration ::=
var_data_type list_of_variable_identifiers ;
TO
assertion_variable_declaration ::=
var_data_type
list_of_variable_identifiers
list_of_variable_decl_assignments ;
Syntax 17-14, p. 265. CHANGE
assertion_variable_declaration ::=
var_data_type list_of_variable_identifiers ;
TO
assertion_variable_declaration ::=
var_data_type
list_of_variable_identifiers
list_of_variable_decl_assignments ;
A.2.10, p. 526. CHANGE
assertion_variable_declaration ::=
var_data_type list_of_variable_identifiers ;
TO
assertion_variable_declaration ::=
var_data_type
list_of_variable_identifiers
list_of_variable_decl_assignments ;
Annex E, p. 563. CHANGE
2)
The abstract syntax eliminates
instantiation of sequences and properties. The semantics of an assertion with
an instance of a sequence or nonrecursive property is
the same as the semantics of a related assertion obtained by replacing the
sequence or nonrecursive property instance with an
explicitly written sequence or property. The explicit sequence or property is
obtained from the body of the associated declaration by substituting actual
arguments for formal arguments. A separate subclause
defines the semantics of instances of recursive properties in terms of the semantics
of instances of nonrecursive properties.
TO
1) The
abstract syntax eliminates local variable declarations. The semantics of local variables
is written with implicit types. The accounting for local variable declaration assignments is
discussed in the next item.
2) The abstract
syntax eliminates instantiation of sequences and properties. The semantics of
an assertion with an instance of a sequence or nonrecursive
property is the same as the semantics of a related assertion obtained by
replacing the sequence or nonrecursive property
instance with an explicitly written sequence or property. The explicit sequence
or property is obtained from the body of the associated declaration by
substituting actual arguments for formal arguments. Local variable declaration
assignments are accounted for as follows.
Let v1 = e1,…,vk
=
ek be the ordered list of declaration
assignments.
·
If the declaration assignments
are in a named sequence with body sequence expression S, then S is replaced by(1, v1
=
e1,…, vk
=
ek) ##0
(S)before
the substitution of actual arguments.
According to 17.8, the instance of S
itself must not admit an empty match.
·
If the declaration assignments
are in a named property with body property expression P and the instance of P
is satisfied by the empty word, then P
is replaced by (1, v1
=
e1,…, vk
=
ek) |-> (P) before the
substitution of actual arguments.
·
If the declaration assignments
are in a named property with body property expression P and the instance of P
is not satisfied by the empty word, then P
is replaced by not((1, v1
=
e1,…, vk
=
ek) |-> not(P)) before the
substitution of actual arguments.
A separate subclause defines the
semantics of instances of recursive properties in terms of the semantics of
instances of nonrecursive properties.
RATIONALE: Jiang Long pointed out that we should probably account for the semantics of local variable declaration assignments in Annex E. The semantics is simplified by excluding the possibility of empty match on an instance of a named sequence with declaration assignments. If the overlapping “followed by” operator is added to the language, then the second property rewrite rule can be simplified to use this operator.
This archive was generated by hypermail 2.1.8 : Mon Feb 19 2007 - 11:07:21 PST