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

From: ben cohen <hdlcohen_at_.....>
Date: Sun Mar 01 2009 - 11:06:37 PST
Page 350: "In the case of or, a local variable flows out of the composite
sequence if, and only if, it flows out of each of the operand sequences. If
the local variable is not assigned before the start of the
composite sequence and it is assigned in only one of the operand sequences,
then it does not flow out of the composite sequence."
In examples below, the local variable flows out of the composite because it
flows out of each of the operand sequences.

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.
 This, in my q1 and q2 examples, each thread of the or continues separately.
So in q1, one thread has v==1, and the other has v==2.
Apologies for posting this new question.
Ben

On Sun, Mar 1, 2009 at 10:31 AM, ben cohen <hdlcohen@gmail.com> wrote:

> 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>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.
Received on Sun Mar 1 11:07:29 2009

This archive was generated by hypermail 2.1.8 : Sun Mar 01 2009 - 11:08:11 PST