DRAFT, 15-SEP-2003 SVA 3.1A PROPOSAL: ACCESSING AND SAMPLING LOCAL VARIABLES ---------------------------------------------------------- DISCUSSION: SVA 3.1 already provides for access of local variables sampled within a defined sequence in the instantiating context of an instance of the sequence. The mechanism is to define the local variables in the instantiating context and pass them into the instance as actual arguments. Provided the local variables flow out of the definition of the instantiated sequence, they can be accessed later in the instantiating context. SVA 3.1 forbids passing arguments to a sequence to which "ended" or "matched" is applied, requiring instead that the desired instance with actual arguments be embedded within an auxiliary defined sequence that has no arguments. This effectively prevents sampled values of local variables from being passed into the instance. This restriction is sensible because the temporal relationship of the sampling point of such local variables to the beginning of a match of the sequence to which "ended" or "matched" is applied is unkown. However, the restriction is more severe than necessary and has the effect of preventing local variables from passing out of applications of "ended" or "matched". This proposal relaxes the restriction on passing local variables to sequence instances to which "ended" or "matched" is applied. This allows local variable values sampled within such instances to be accessed in the intantiating context by the same mechanism as that for ordinary sequence instances. The following restriction is imposed, though, in order to avoid passing sampled values of local variables into a sequence instance to which "ended" or "matched" is applied: RESTRICTION: If "ended" or "matched" is applied to any instance of a defined sequence S and if S has a local variable v as formal argument, then v must not be referenced within the definition of S before it is sampled within S. In particular, if "v = exp" is a sampling of v in the definition of S and if v has not been previously sampled or initialized in S, then v cannot be in the support of "exp". The effect is that the values of local variables sampled outside do not flow into such a sequence. In a single cycle, there can be mutliple matches of a sequence instance to which "ended" is applied and these matches can have different valuations of the local variables. The multiple matches are treated semantically the same way as matching both disjuncts of an "or". In other words, the thread evaluating the instance to which "ended" will fork to account for such distinct local variable valuations. Such forking occurs analogously when a multi-clocked sequence evaluates a sequence instance to which "matched" is applied. In this case, the multiple matches that result in forking need not be simultaneous, but they all must occur before the clock event that leads the subsequence that follows the evaluation. This proposal also makes coding of the sampling of local variables simpler by allowing sampling to occur after any sequence expression, not just booleans. This extension is an abbreviation for a capability that already exists in the language, as (sequence_expr, v = e) is semantically equivalent to sequence_expr ##0 (1'b1, v = e) Thus, as an alternative to (!a[*0:$] ##1 (a, v = e) ##1 first_match(##[0:$]b) |=> c one can code (first_match(##[0:$]a), v = e) ##1 first_match(##[0:$]b) |=> c This proposal does not provide for access of local variables in the action block. The capability needed to generated error messages with local variables seems better solved by moving the activation of the messages into the assertion definitions rather than trying to solve the problem of accomodating multiple threads with distinct local variable valuations in a single execution of the action block. PROPOSED CHANGES TO THE BNF: ---------------------------- 1. p. 155, box 17-5. Change sequence_expr ::= ... | expression { , function_blocking_assignment } [boolean_abbrev] | (expression { , function_blocking_assignment } ) [boolean_abbrev] | sequence_instance [ sequence_abbrev ] | (sequence_expr) [ sequence_abbrev ] to sequence_expr ::= ... | expression | sequence_expr { , function_blocking_assignment } [boolean_abbrev] | (sequence_expr { , function_blocking_assignment } ) [boolean_abbrev] | sequence_instance [ sequence_abbrev ] | (sequence_expr) [ sequence_abbrev ] 2. p. 172, box 17-13. Change sequence_expr ::= ... | (expression { , function_blocking_assignment } ) [boolean_abbrev] | expression { , function_blocking_assignment } [boolean_abbrev] to sequence_expr ::= ... | sequence_expr { , function_blocking_assignment } [boolean_abbrev] | (sequence_expr { , function_blocking_assignment } ) [boolean_abbrev] 3. p. 281, in the production for sequence_expr. Change | expression { , function_blocking_assignment } [boolean_abbrev] | (expression { , function_blocking_assignment } ) [boolean_abbrev] to | expression | sequence_expr { , function_blocking_assignment } [boolean_abbrev] | (sequence_expr { , function_blocking_assignment } ) [boolean_abbrev] PROPOSED CHANGES TO LRM TEXT: ----------------------------- 1. 17.7.10, p. 168. Change ended can be used directly ... to ended can be used on an instance of a defined sequence with arguments. For example, sequence e2(a,b,c); @(posedge sysclk) $rose(a) ##1 b ##1 c; endsequence sequence rule2; @(posedge sysclk) reset ##1 inst ##1 e2(ready,proc1,proc2).ended ##1 branch_back; endsequence If ended is applied to an instance of a defined sequence with formal arguments, then for any formal argument that is a local variable (17.8), the local variable must be sampled in the definition of the sequence before it can be referenced. 2. 17.8, p. 172, before "Local variables can be written on repeaded sequences and accomplish accumulation of values". Add Local variables can be sampled at the end of any sequence expression. For example, sequence two_cycle_stability; [7:0] x; ($first_match(##[0:$]req), x = attribute) ##1 (a && (attribute == x)); endsequence 3. 17.8, p. 173, before "There are special considerations on using local variables in parallel branches ...". Add Also, if a local variable is a formal argument of a sequence to which "ended" is applied, then in the definition of the sequence the local variable must be sampled before it can be referenced. 4. 17.11, p. 179. Delete Like ended, matched can be used directly on sequences that do not have formal arguments. 5. 17.11, p. 179, end of subsection. Add, If a local variable is a formal argument of a sequence to which "matched" is applied, then in the definition of the sequence the local variable must be sampled before it can be referenced. 6. [TBD. Add some intuitive discussion of getting local variables out of an instance to which "matched" is applied and give an example.] PROPOSED CHANGES TO THE FORMAL SEMANTICS: ----------------------------------------- 1. G.2.3.5, p. 346. Change * (b, v = e) \equiv (b ##0 (1, v = e)) to * (R, v = e) \equiv (R ##0 (1, v = e)) 2. G.2.3.5, p. 346. Change * (b, v_1 = e_1,..., v_k = e_k) \equiv ( (b, v_1 = e_1) ##0 (1, v_2 = e_2,..., v_k = e_k) ) to * (R, v_1 = e_1,..., v_k = e_k) \equiv ( (R, v_1 = e_1) ##0 (1, v_2 = e_2,..., v_k = e_k) ) 3. G.4.1, p. 351. Change T denotes a clocked or unclocked sequence to T(V) denotes an instance of a clocked or unclocked sequence that is passed the local variables V as actual arguments 4. G.4.1, p. 351. Change * w^j |= T.ended iff there exist 0 <= i <= j and L such that w^{i,j},{},{} |== T to * w^j,L_0,L_1 |== T(V).ended iff there exist 0 <= i <= j and L such that both w^{i,j},{},L |== T(V) and L_1 = L_0 |_{dom(L_0) - (dom(L) \cap V)} \cup L|_V 5. G.4.1, p. 351. Change * w^j |= @(c) (T.matched) iff there exists 0 <= i < j such that w^i |= T.ended and w^{i+1,j},{},{} |== (!c[*0:$] ##1 c). to * w^j,L_0,L_1 |= @(c) (T(V).matched) iff there exists 0 <= i < j such that w^i,L_0,L_1 |= T(V).ended and w^{i+1,j},{},{} |== (!c[*0:$] ##1 c).