I expect the answer to be that 2 values of v are flowed out, but that would be OK if in a property I have :property P; int v_p; q1(v_p) ##1 x==v_p; endproperty : P But what happens if the sequence q1 is an antecedent? e.g., property P; int v_p; q1(v_p) |=> x==v_p; // 2 thread? 2 antecedents and consequents? endproperty : P Ben On Sun, Mar 1, 2009 at 1:17 PM, ben cohen <hdlcohen@gmail.com> wrote: > 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.Received on Sun Mar 1 13:23:13 2009
This archive was generated by hypermail 2.1.8 : Sun Mar 01 2009 - 13:23:49 PST