SV-AC Ballot for 03/23/03, Vote due by 03/24/03 12noon Pacific Written by: Stephen Meier This is major vote - 1 vote per Accellera member company with attendance record Ballot ====== 5a Sem5 Expand local variable support [] Yes []No 5b Sem5 Provide explicit passing of local variable in/out of named seq [] Yes []No 15 Sem6 Multiple clock support [] Yes []No 17 Sem8 Add optional negation of rhs of sequence implication [] Yes []No 20 Sem9 Add matched operator (only applicable if Item15 approved) [] Yes []No Ballot Notes: ============= Items require a simple majority of all cast votes to be approved. All items are major vote = 1 vote per Accellera member company with valid attendance record. Item 5a: Expand Local Variable support ======= A yes vote approves the expanded support based on following proposal. Date: Thu, 20 Mar 2003 09:46:32 -0600 (CST) To: sv-ac@eda.org Subject: [sv-ac] local variable proposal From: John Havlicek Reply-To: john.havlicek@motorola.com Sender: owner-sv-ac@eda.org All: Below is a revision of the "forward flow" local variable proposal. Here are the changes: 1. New rule for "&&" and "intersect" as suggested by Erich Marschner. This rule now allows a local variable that exists before the fork and is sampled in exactly one branch of the "&&" or "intersect" to pass on with its latest sampled value. 2. Rewrote the rules for "||", "&&", "intersect" to try to make them clearer. 3. Changed "and" to "&&", "or" to "||" in a few places. This proposal does not address the issues discussed with Jay Lawrence about local variables flowing into and out of instances of named sequences. As you have seen in my previous mail, I was being naive in saying that the rules below should apply after elaboration of named sequence instances. Such a convention will make the namespaces of defined sequences difficult to manage. Best regards, John Havlicek ================================================================= DISCUSSION: The local (i.e., dynamic) variables described in LRM 0.80 are severely restricted by the strict scoping rules. Since nesting of implications has been eliminated, it is no longer possible to attach local variables to the desired sampling point withing the lhs of an implication. There has never been a mechanism for publishing local variables outside of a named subsequence or an instance thereof. This proposal attempts to overcome these limitations of local variables without separating the declaration of a local variable from the sampling point. The basic idea is to use a "forward flow" semantics for local variables. Intuitively, once a local variable is sampled, it can be referenced at that or any later point of a sequence or implication. The definition and sampling of a local variable can be attached to the beginning or to the end of a sequence element. Thus, one can write a sequence like (a; !a (int x = data_in); !b*[0:inf]; b && (data_out == x)) or an implication like (a; !a (int x = data_in)) => (!b*[0:inf]; b && (data_out == x)) and understand that the value sampled into x is available "further to the right" in the sequence or implication. Furthermore, one can write local variables on repeated sequences and accomplish accumulation of values, as in (int x = 0) ((!a*[0:inf]; a (int x = x+data))*[4]; b; c && (data_out == x)) The challenge that comes with the forward flow semantics is to define which local variables are visible after an "||", "&&", or "intersect". The motivating principle in this proposal is that local variables which are guaranteed to exist after such an operation without collision can flow on, while other local variables will be lost. PROPOSAL: This feature allows one to declare local variables and use them anywhere subsequent in the property or sequence without using the strict scoping of 0.80 LRM. SYNTAX: BNF sequence_element ::= "sequence_element as currently defined" | `('var_decl`)' sequence_element | sequence_element `('var_decl`)' SEMANTICS: 1) The declaration and assignment point of the local variables is the same. For example, sequence s1 = (a ; b (int x = data); (c==x)); 2) There is no explicit scoping of variables related to subsequences. Once declared, the variable is available until the end of the sequence or property. For example, property p1 = ((a ; b (int x = data); c) => (d==x)); 3) The local variable may be used as initializer for another local variable declared later in the sequence. For example, property p2 = ((a ; b (int x = data); c) => (1; d (int x1 = x + data1); e==x1)); 4) If a local variable is redeclared with the same name later in the sequence, then the later version of the variable shadows the previous declaration. Any reference after the redeclaraion in the sequence to the variable will be accessing the later declaration. Also, rhs of the initialization of a variable may reference a local variable with the same name, in which case, the previous version of the variable will be used to initialize the declaration. For example, property p3 = ((a ; b (int x = data); c) => (1; d (int x = x + data1); e==x)); 5) There are special considerations on declaring and using local variables in parallel branches ("||", "&&" and "intersect"). i) Variables declared on parallel threads cannot be accessed in sibling threads. For example, sequence s4 = ((a ; (int x = data) b; c) || (d; (e==x))); // this is illegal ii) In the case of "||", it is the intersection of the variables (names) that passes on past the "||". More precisely, a local variable passes on past the "||" iff either a. The local variable exists at the start of the "||". or b. The local variable is sampled in both branches of the "||". Note that both a. and b. can hold. All succeeding threads out of "||" branches continue as separate threads, carrying with them their own latest samplings of the local variables. These threads do not have to have consistent valuations for the local variables. For example, sequence s5 = ( ( (a ; (int x = data, int y = data1) b; c) || (d; (int x = data) (e==x)) ) ; (y==data2) ); // illegal since y is not in the intersection sequence s6 = ( ( (a ; (int x = data, int y = data1) b; c) || (d; (int x = data) (e==x)) ) ; (x==data2) ); // legal since x is in the intersection iii) In the case of "&&" and "intersect", the symmetric difference of the local variables that are sampled in the two joining threads passes on past the join. More precisely, a local variable passes on past the join iff either a. The local variable exists at the start of the "&&" or "intersect" and is sampled in neither branch. or b. The local variable is sampled in exactly one of the branches. The value passed on is the latest sampled value. The two joining threads are merged into one thread at the join. sequence s7 = ( ( (a ; (int x = data, int y = data1) b; c) && (d; (int x = data) (e==x)) ) ; (x==data2) ); // illegal since x common to both threads sequence s8 = ( ( (a ; (int x = data, int y = data1) b; c) && (d; (int x = data) (e==x)) ) ; (y==data2) ); // legal since y is in the difference iv) The intersection and difference of the sets of names should be computed statically at compile time. Item 5b: Explicit passing of local variable in/out of named sequences ======= A yes vote approves the explicit passing of local variables based on following proposal. DISCUSSION: Some care needs to be taken in the way local variables flow into and out of instances of named sequences in order to make management of names reasonable for users. There are two problems with using the forward flow semantics after instances of sequences are expanded in a macro fashion: 1. Local variables in the instantiating context may overshadow references in the definition of the instantiated sequence that were intended to bind otherwise (e.g., to design signals of the same name). [Undesirable inward flow.] 2. Local variables in the definition of a named sequence may overshadow references in the instantiating context that were intended to bind otherwise. [Undesirable outward flow.] Both problems are illustrated in the following example: sequence s(v) = (a; (b==v) (int x=e) ; 1; c==x); sequence t = (u (int b=w, int x=z); s(x); y==x+b); If the instance of s in t is expanded as a macro, then we get (u (int b=w, int x=z); (a; (b==x) (int x=e) ; 1; c==x); y==x+b); As a result, the reference to b in "b==x" now means the local variable that was sampled in "int b=w", not whatever b meant in the context of the definition of s. This is an example of undesirable inward flow. Also, the reference to x in "y==x+b" now means the local variable that was sampled in "int x=e", rather than the one sampled in "int x=z". This is an example of undesirable outward flow. The following proposal is intended to eliminate undesirable inward and outward flow, while still allowing both as controlled by the user through argument passing. This proposal does not describe the specific syntax for achieving the argument passing, as it is out-of-scope of SV-AC. PROPOSAL: 1. A sequence definition will distinguish input and output formal arguments. 2. Local variables sampled in the instantiating context will flow into an instance of a sequence only if passed in as actual arguments to input formal arguments of the sequence. A local variable passed as an actual argument to an input formal argument must be declared and sampled in the instantiating context before the instance of the sequence. 3. Local variables sampled in the definition of the instantiated sequence will flow out of an instance of the sequence only if they are output formal arguments of the sequence definition. The values passed out will be bound to the actual arguments as local variables in the instantiating context. This proposal does not say how the actual arguments must be declared. a. One possibility is that the actual argument constitutes a local variable declaration and sampling at completion of the named sequence instance. b. Another possibility is that the actual argument must be declared and sampled before the instance of the sequence. 4. References to names in a sequence definition that are not formal arguments will be bound according to scoping rules at the sequence definition, not according to scoping rules at instances of the sequence. Item 15: Multiple clock support ======= A yes vote would approve enhancements to provide multiple clock support based on following proposal. Syntax is only for demonstration purposes. If approved syntax will be determined by the DWG group. Date: Wed, 5 Mar 2003 15:11:37 -0600 (CST) To: sv-ac@eda.org Subject: [sv-ac] multi-clock proposal From: John Havlicek Reply-To: john.havlicek@motorola.com Sender: owner-sv-ac@eda.org All: Below is a multi-clock proposal for SVA from the semantics subcommittee. Best regards, John Havlicek ========================================== 1) Introduce a higher layer of sequences, multiply-clocked sequences, which are formed by attaching a clock operator (i.e., event_control) to a sequence. 2) The ordinary sequence operators cannot be applied to multiply-clocked sequences. 3) Mulitply-clocked sequences can be combined by a non-overlapping concatenation operator, represented below by the placeholder "@@". 4) Multiply-clocked sequences can be combined by the non-overlapping version of "=>", represented below by the placeholder "|=>". So the modified BNF will look something like sequence_expr ::= sequence_instance | '(' sequence_expr ')' | boolean_expr | range sequence_expr | sequence_expr { ';' range sequence_expr } | sequence_expr '*' range | boolean_expr '*=' range | sequence_expr 'within' sequence_expr | boolean_expr 'throughout' sequence_expr | sequence_expr and sequence_expr | sequence_expr or sequence_expr | sequence_expr intersect sequence_expr | first_match '(' sequence_expr ')' | '(' var_decl {,var_decl}; sequence_expr ')' range ::= '[' constant_range_expression ']' | '[' constant_range_expression ':' constant_range_expression ']' | '['constant_range_expression ':' inf ']' clocked_sequence_expr ::= [event_control] sequence_expr mult_clk_seq ::= clocked_sequence_expr { '@@' clocked_sequence_expr } prop_expr ::= mult_clk_seq | implication | '(' prop_expr ')' implication ::= sequence_expr => sequence_expr | mult_clk_seq |=> mult_clk_seq Item 17: Add feature to allow negation of rhs of implication operator ======= Yes on this proposal would extend sequential implication operator feature with optional negation of rhs sequence. Date: Thu, 6 Mar 2003 11:10:27 -0600 (CST) To: sv-ac@eda.org Subject: [sv-ac] negate rhs of implication From: John Havlicek Reply-To: john.havlicek@motorola.com Sender: owner-sv-ac@eda.org All: As the freeze is on, here is another issue I would like to raise. The (unclocked) semantics for implication is as follows: w |= r => s iff for every j >= 0 such that w^{0,j} |== r, there exists k >= j such that w^{j,k} |== s. If we negate this, we get w |= not(r => s) iff there exists j >= 0 such that w^{0,j} |== r and for all k >= j, not(w^{j,k} |== s). It has been argued that this semantics is not as useful as for every j >= 0 such that w^{0,j} |== r, for every k >= j, not(w^{j,k} |== s), which corresponds to the syntax w |= r => (not s). Therefore, I would like to raise as issue for consideration that we allow negation of the rhs of an implication. Notice that if negation of rhs is allowed, then there is typically no need to write something like "not(r => (not s))", since w |= not(r => (not s)) iff there exists j >= 0 such that w^{0,j} |== r and there exists k >= j such that w^{k,j} |== s which is usually equivalent to w |= r ;[0] s Best regards, John Havlicek Item 20: Addition of matched operator ======= Yes on this proposal would add support of matched operator iff the multiclock proposal passes. The matched operator is a feature to detect endpoint of a sequence from another clock domain. The behavior is to latch the occurence of endpoint of sequence until next occurence of the sampling clock. From: Surrendra Dudani Subject: [sv-ac] "matched" operator: a new issue Sender: owner-sv-ac@eda.org Hi All, I would like to raise a new issue. Hopefully, it will be considered before the tomorrow's deadline. I am proposing to add a new operator "matched". Like "ended" operator for a single clock domain, "matched" detects the endpoint of a sequence from one clock domain in another. Also, like, "ended" it is a boolean, so it can be conveniently combined with other boolean operators, and assigned to a variable. This functionality is useful when the beginning of a sequence is of no consequence. Having explicit "matched" operator, and the multi-clock proposal from John would provide a very powerful and easy-to-use capability. Surrendra End of Ballot