Re: [sv-ac] P1800-2009 Page 350 "threads do not have to have consistent valuations for the local variables"

Ed, So far so good, thanks, but now a more complex case:  Consider the
following example:
 sequence q1(local output int v);  // assume that a==b==c==1, d==2
 ( ((a, v=1) ##1 b==v) or  // v==1 for this thread
   ((c, v=2) ##1 d==v) )    // v==2 for this thread
endsequence : q1
What is the value of the outflow for v?
Would it make a difference if one thread is longer and has a reassignment
for v? e.g.
sequence q2(local output int v);  // assume that a==b==c==1, d==2
 ( ((a, v=1) ##1 b==v) or  // v==1 for this thread
   ((c, v=2) ##1 d==v ##1 (1'b1, v=100) )    // v==2 for this thread
endsequence : q2
hanks again,
Ben
On Sun, Mar 1, 2009 at 11:14 AM, Eduard Cerny <Eduard.Cerny@synopsys.com>wrote:

>  Hi Ben,
>
>
>
> both threads continue as if you opened up the expression into a tree. In
> other words,
>
> sequence q1;  // assume that a==b==c==1, d==2
>
>    int v;
>
>    ( ((a, v=1) ##1 b==v) *o*r  // v==1 for this thread
>
>      ((c, v=2) ##1 d==v) )    // v==2 for this thread
>
>       ##1 e==v; *// v == 1?,  v==2? What is the value of v here? *
>
> endsequence : q1
>
>
>
>
>
> Is the same as
>
>
>
> sequence q1;  // assume that a==b==c==1, d==2
>
>    int v;
>
>    ( ((a, v=1) ##1 b==v##1 e==v) *o*r  // v==1 for this thread
>
>      ((c, v=2) ##1 d==v ##1 e==v))    // v==2 for this thread
>
>       ; *// v == 1?,  v==2? What is the value of v here?  BOTH, each
> thread a different one*
>
> endsequence : q1
>
>
>
> So each branch can have a match, like when you have no local variables. In
> your 2nd example, there is only one thread that reaches a match, and v is
> 1.
>
>
>
> This is also why in intersection you cannot have the same variable in both
> branches because after the intersection there is only one thread (unlike
> with or).
>
>
>
> Does that help?
>
>
>
> Best…
>
> ed
>
>
>
>
>
> *From:* ben cohen [mailto:hdlcohen@gmail.com]
> *Sent:* Sunday, March 01, 2009 1:32 PM
> *To:* Eduard Cerny
> *Cc:* sv-ac@eda.org
> *Subject:* Re: [sv-ac] P1800-2009 Page 350 "threads do not have to have
> consistent valuations for the local variables"
>
>
>
> Thanks Ed,
>
> Thanks for the reply. Since each thread have their copies of the local
> variables, what is the value of the single local variable when the *or* threads
> terminate? For example, given the following 2 sequences.
>
> sequence q1;  // assume that a==b==c==1, d==2
>
>    int v;
>
>    ( ((a, v=1) ##1 b==v) *o*r  // v==1 for this thread
>
>      ((c, v=2) ##1 d==v) )    // v==2 for this thread
>
>       ##1 e==v; *// v == 1?,  v==2? What is the value of v here? *
>
> endsequence : q1
>
> In q1, each thread of the "or" sequence start and end at the same cycle.
>
>
>
> sequence q12;  assume that a==b==c==1, d==10
>
>    int v;
>
>    ( ((a, v=1) ##1 b==v) *o*r   // v==1 for this thread
>
>      ((c, v=2) ##10 d==v) )    // v==2 for this thread
>
>       ##1 e==v; *// v == 1?,  v==2? What is the value of v here? *
>
> endsequence : q2
>
> In q2, each thread of the "or" sequence start at the same cycle, but end at
> different cycles.  The "or" becomes trrue at cycle 2, ans q2 terminates at
> cycle 3.
>
> Comments?
>
> Thanks,
>
> Ben
>
>
>
>
>
> On Sun, Mar 1, 2009 at 8:14 AM, Eduard Cerny <Eduard.Cerny@synopsys.com>
> wrote:
>
> Hi Ben,
>
>
>
> the two threads have separate copies of the variable x. Each thread then
> continues with their copy of x to evaluate x==data2.
>
> Best regards,
>
> ed
>
>
>
>
>
> *From:* owner-sv-ac@eda.org [mailto:owner-sv-ac@eda.org] *On Behalf Of *ben
> cohen
> *Sent:* Sunday, March 01, 2009 10:31 AM
> *To:* sv-ac@eda.org
> *Subject:* [sv-ac] P1800-2009 Page 350 "threads do not have to have
> consistent valuations for the local variables"
>
>
>
> Below is LRM statements with highlighted points of concern or
> clarification:
>
> LRM states that *These threads do not have to have consistent valuations
> for the local variables*.
>
> But, example does show a consistent valuation for "x".   According to those
> rules, the following example would pass the LRM requirements, but I think
> that it should not:
>
> sequence s6_MODIFIED_SLIGHTLY;
>
> int x,y;
>
> ((a *##1 (b, x = data*, y = data1) ##3 *c && x==10* )  // Thread1:
>
> *or* (d *##2 (`true, x = data) ##3* (e==x))) ##1 (x==data2);  // Thread2:
>
>
> // legal because x is in the intersection
>
> endsequence
>
> Assume a==d==b==1
>
> @ cycle 2, *##1 (b, x = data) *causes x=data @ cycle2 for thread 1
> (x==dataT1@cy2 // data thread1 @ cycle2)
>
> @ cycle 3, *##2 (`true, x = data) *causes x=data @ cycle3. (x==dataT2@cy3)
> This is different than what thread1 expects later on.
>
> Thus, Thread 1 now has a different value of x , the one written at cycle 2,
>
>
> @ cycle 5 (*c && x==10), *we're expecting x to be 10, the value thought to
> have been captured at cycle 2 (i.e., dataT1@cy2),
>
> but x was re-evaluated at cycle 3 with the value dataT2@cy3.
>
> Thus, the rule "*These threads do not have to have consistent valuations
> for the local variables*."
>
> does not stand.  In your LRM example, x is updated in both threads at cycle
> 2 with the same data if a==b==d==1.
>
> So here it works.  The only way I see the statement "*These threads do not
> have to have consistent valuations for the local variables"*.  to be true
> is if there are 2 versions of the local variable x, one for each thread.  I
> don't believe that this is the intent.
>
> Comments?
>
> Thanks for clarifying this.
>
>
>
> ------------------------------------------------LRM
> ------------------------
>
> c) Each thread for an operand of an or that matches its operand sequence
> continues as a separate
>
> thread, carrying with it its own latest assignments to the local variables
> that flow out of the composite
>
> sequence. *These threads do not have to have consistent valuations for the
> local variables*. For
>
> example:
>
> sequence s5;
>
> int x,y;
>
> ((a ##1 (b, x = data, y = data1) ##1 c)
>
> or (d ##1 (`true, x = data) ##0 (e==x))) ##1 (y==data2);
>
> // illegal because y is not in the intersection
>
> endsequence
>
> sequence s6;
>
> int x,y;
>
> ((a *##1 (b, x = data*, y = data1) ##1 c)
>
> *or* (d *##1 (`true, x = data) *##0 (e==x))) ##1 (x==data2);
>
> // legal because x is in the intersection
>
> endsequence
>
>
> --
> This message has been scanned for viruses and
> dangerous content by *MailScanner* <http://www.mailscanner.info/>, and is
> believed to be clean.
>
>
>

-- 
This message has been scanned for viruses and
dangerous content by MailScanner, and is
believed to be clean.