Subject: [sv-ac] Final Ballot for 3/23
From: John Havlicek (john.havlicek@motorola.com)
Date: Sun Mar 23 2003 - 23:02:52 PST
Steve:
Motorola votes yes on all ballot items.
Best regards,
John Havlicek
> --=====================_224479985==_
> Content-Type: text/plain; charset="us-ascii"; format=flowed
>
> Hello:
>
> I did not receive any review comments on the draft ballot, so the ballot
> now is final.
>
> If you are a voting Accellera member company please submit your vote by
> 12noon Pacific tomorrow 3/24.
>
> Synopsys votes yes on all ballot items.
>
> Regards,
> Steve
> -----------
> >X-Sender: smeier@pophost.synopsys.com
> >X-Mailer: QUALCOMM Windows Eudora Version 5.1
> >Date: Thu, 20 Mar 2003 23:03:28 -0800
> >To: System Verilog Assertion <sv-ac@eda.org>
> >From: Stephen Meier <Stephen.Meier@synopsys.COM>
> >Subject: [sv-ac] Draft of Ballot for 3/23
> >Sender: owner-sv-ac@eda.org
> >
> >
> >Hi:
> >
> >Here is a draft of ballot. Please repond with any comment by noon on
> >Sunday 3/23. I will update and send out by midnight Sunday. Votes are
> >due by 12noon Monday. All times Pacific.
> >
> >Regards,
> >Steve
> >
> >Steve Meier (stephen.meier@synopsys.com) W: 650-584-4476, Cell: 408-393-8246
> >
> >
>
> Steve Meier (stephen.meier@synopsys.com) W: 650-584-4476, Cell: 408-393-8246
>
>
> --=====================_224479985==_
> Content-Type: text/plain; charset="us-ascii"
> Content-Disposition: attachment; filename="svac_ballot_0224032.txt"
>
> 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 <john.havlicek@motorola.com>
> 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 <john.havlicek@motorola.com>
> 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 <john.havlicek@motorola.com>
> 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 <Surrendra.Dudani@synopsys.COM>
> 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
>
> --=====================_224479985==_--
This archive was generated by hypermail 2b28 : Sun Mar 23 2003 - 23:11:50 PST