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

Hello Ben,

just consider that each thread is an independent entity and it carries with it its "context", the value of the local variable.

So, regarding your example, please see belaow.

Best...
ed


From: ben cohen [mailto:hdlcohen@gmail.com]
Sent: Sunday, March 01, 2009 4:17 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"

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?
[Ed:] There are two threads that match, one having v equal to 1, and the other v equal to 2.  Both match.  If the sequence is used as a property, then either one is the first match -> success of the property.
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
[Ed:] No it will not make a diff in the interpretation. The first thread finishes with v equal to 1, and the other one finishes with v equal to 100 this is because the in 2nd thread v is reassigned a new value. Look at it as in procedural language programming with fork and join, with a new variable being created if there is a choice. In procedural code evaluation of nondeterministic choice, it is in fact a concurrent evaluation of the two threads, one (or both) that match are considered....
hanks again,
Ben
On Sun, Mar 1, 2009 at 11:14 AM, Eduard Cerny <Eduard.Cerny@synopsys.com<mailto: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) or  // 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) or  // 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<mailto:hdlcohen@gmail.com>]
Sent: Sunday, March 01, 2009 1:32 PM
To: Eduard Cerny
Cc: sv-ac@eda.org<mailto: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) or  // 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) or   // 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<mailto: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> [mailto: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<mailto: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.