John, Thanks for the clarification. The complexity can grow pretty fast! If the ORing subsequences have a range, as shown below, and that sequence is an antecedent, we now have multiple matches with the same starting but multiple ending points, and with different outgoing valuations of the local variables. sequence q1(local output int v); // assume that a==b==c==1, d==2 ( ((a, v=1) ##[1:10] b==v) or // v==1 for this thread ((c, v=2) ##1 d==v) ) // v==2 for this thread endsequence : q1 If I apply the first_match operator, would that give one match of the possible sequences with the same starting point, but different endpoints caused by the range delay. But would I still have different outgoing valuations of the local variables? I think tha the answer would be yes. first_match(q1) |=> x==v; // 2 values of v or one?? What if the 2 threads of some q_sequence end at the same cycle, but with different values of the local variables, then first_match(q_sequence) |=> x==v; Thanks again, Ben On Sun, Mar 1, 2009 at 2:09 PM, Havlicek John-R8AAAU < john.havlicek@freescale.com> wrote: > Hi Ben: > > Your answer "2 values of v are flowed out" is correct. It does not matter > whether the "or" subevaluations end their matches at the same timepoint. > > In the case that q1(v_p) is an antecedent, the two values result in > multiplicity of matching. > > Without local variables, evaluation of an antecedent from a given starting > point can still have multiple matches, but we really only care about at most > one such for any pair of starting > and ending points for the match. > > Once we add local variables into the mix, we must also differentiate > multiple matches with the same starting and ending point but with > different outgoing valuations of the local variables. > > J.H. > > ------------------------------ > *From:* owner-sv-ac@eda.org [mailto:owner-sv-ac@eda.org] *On Behalf Of *ben > cohen > *Sent:* Sunday, March 01, 2009 3:22 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" > > 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* <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 14:43:59 2009
This archive was generated by hypermail 2.1.8 : Sun Mar 01 2009 - 14:44:47 PST