John, first_match(s.triggered) versus first_match(s).triggered Actually, I am contrasting the two. The issue came up as to whether the two are equivalent. They are not. If s.triggered has multiple matches, s.triggered will have have multiple end points. The issue then became, are the end points of s.triggered considered as a sequence? If so, then first_match(s.triggered) would have one match. But, from this discussion, and from observation on the simulator, s.triggered behaves (am not not implying to mean to same as) as a variable of type logic that is true everytime there is a match. I see it as a pulse of one cycle starting from the Observed region and ending at the PostPoned region. That would explain why first_match(s.triggered) == s.triggered Now, if it behaves as a pulse, then always @ s.triggered $display("triggered"); // should tigger twice My simulator triggeres it once! Conclusion ??? There is some ambiguity here. A formal request for clarification is useless ##1 So far I got no info from my previous formal request for clarification from the IEEE. Maybe it takes time ... It's called "the process".. :) Ben On Mon, Oct 26, 2009 at 5:53 AM, Havlicek John-R8AAAU <r8aaau@freescale.com>wrote: > Hi Ben: > > Thanks. > > There are multiple technical issues being discussed here. > > What I tried to say is that a Boolean sequence cannot have multiple matches > in a single attempt. s.triggered is a Boolean sequence (when it stands as a > sequence), and so it too cannot have multiple matches. > > I agree with you that > > s.triggered > > behaves the same as > > first_match(s.triggered) > > whenever both of these stand as sequences. > > I have wondered why you are not contrasting > > s.triggered > > with > > first_match(s).triggered > > ? > > J.H. > ------------------------------ > *From:* ben cohen [mailto:hdlcohen@gmail.com] > *Sent:* Sunday, October 25, 2009 5:02 PM > *To:* Havlicek John-R8AAAU > *Cc:* Eduard Cerny; Bustan, Doron; sv-ac@server.eda.org; Lisa Piper; > Seligman, Erik; Korchemny, Dmitry > *Subject:* Re: [sv-ac] SVA: Clarification: Is result of .triggered a > boolean or a sequence ? > > John and all, > Thanks for the clarifications. The original issue came about because there > was a question on the assertions below: > sequence q_b; @ (posedge clk) $rose(a) ##[1:$] b; endsequence : q_b > sequence q_bFM; @ (posedge clk) first_match ($rose(a) ##[1:$] b); > endsequence : q_bFM > *aP1*: assert property (@ (posedge clk) *first_match*(q_b.*triggered*) > |=> c); > *aP1_FM*: assert property (@ (posedge clk) *first_match*(q_bFM.* > triggered*) |=> c); > As John restated it, *q_b.triggered* has multiple matches, and aP1 has > multiple evaluation attempts of a static concurrent > assertion. The *first_match* does NOT reduce those multiple evaluations, > and is unlike the first_match(some_sequence).. That was the issue. > However, q_bFM has a single match, and thus one evaluation. Again the > first_match does nothing to reduce the evaluations, but there is only one > evaluation because there is only one match. > ** While we're on the subject, I do have another question. > What is the difference between > * always *@some_seq and > * always *@some_seq.*triggerred* > I did some simulation and saw no difference. In my view, the *@some_seq * triggers > at the completion of the sequence, but that completion is an end point. The > counter argument is that *@some_seq.**triggerred *is a pulse that lasts > for one time step,thus there are 2 edges. However, the simulator disproves > that theory. What I also saw in the simulation is that is a sequence with > multiple matches will cause multiple triggering of the always procedure > (regardless of the *@some_seq* or the *@some_seq.**triggerred). * > *Thus, can we say that those two are equivalent? * > As a guideline, I presume that there is no need for the .triggered in that > case. > Thanks to all, > Ben > > . > > > On Sun, Oct 25, 2009 at 12:49 PM, Havlicek John-R8AAAU < > r8aaau@freescale.com> wrote: > >> Hi Ed: >> >> Hmm ... I agree with Doron. >> >> I think that first_match(b) is equivalent to b for any Boolean b. Ben >> made this point. >> >> What Doron disagrees with, and I do too, is the statement that the >> antecedent of >> >> b |=> p >> >> has multiple matches. The antecedent b either matches once or does not >> match -- there is no opportunity for multiple matches here. >> >> Now, Ben did not exactly say that the antecedent has multiple matches -- >> he said that it has multiple threads. I agree that multiple threads are >> associated with the antecedent, but this is just because >> >> assert property (first_match(s.triggered) |=> p); >> >> results in multiple evaluation attempts of the underlying implication. I >> find Ben's phrase "antecedent has multiple threads" confusing, because these >> multiple threads have nothing to do with the antecedent. They are multiple >> evaluation attempts of a static concurrent assertion. >> >> J.H. >> >> ------------------------------ >> *From:* owner-sv-ac@eda.org [mailto:owner-sv-ac@eda.org] *On Behalf Of *Eduard >> Cerny >> >> *Sent:* Sunday, October 25, 2009 8:53 AM >> *To:* Bustan, Doron; ben@systemverilog.us; sv-ac@server.eda.org; Lisa >> Piper; Seligman, Erik; Korchemny, Dmitry >> >> *Subject:* RE: [sv-ac] SVA: Clarification: Is result of .triggered a >> boolean or a sequence ? >> >> Hi Doron, >> >> >> >> I think that Ben is right, you cannot distinguish multiple setting of the >> conceptual (and real) boolean by several threads/attempts. >> >> >> >> ed >> >> >> >> >> >> *From:* owner-sv-ac@eda.org [mailto:owner-sv-ac@eda.org] *On Behalf Of *Bustan, >> Doron >> *Sent:* Sunday, October 25, 2009 4:02 AM >> *To:* ben@systemverilog.us; sv-ac@server.eda.org; Lisa Piper; Seligman, >> Erik; Korchemny, Dmitry >> *Subject:* RE: [sv-ac] SVA: Clarification: Is result of .triggered a >> boolean or a sequence ? >> >> >> >> Hi Ben, >> >> >> >> I disagree. In your example every attempt has one thread (not sure thread >> is defined in the LRM), and all attempts fail. >> >> So, the multiple match of q_b, just means that there are multiple attempts >> where the triggering Boolean is true. >> >> >> >> >> >> >> >> Doron >> ------------------------------ >> >> *From:* owner-sv-ac@server.eda.org [mailto:owner-sv-ac@server.eda.org] *On >> Behalf Of *ben cohen >> *Sent:* Sunday, October 25, 2009 4:21 AM >> *To:* sv-ac@server.eda.org; Lisa Piper; Seligman, Erik; Korchemny, Dmitry >> *Subject:* [sv-ac] SVA: Clarification: Is result of .triggered a boolean >> or a sequence ? >> >> >> >> LRM: *16.9.11 Detecting and using end point of a sequence ...The end >> point of a sequence is reached whenever the ending clock tick of a match of >> the sequence is reached, regardless of the starting clock tick of the match. >> The reaching of the end point can be tested by using the method triggered. >> .... When method triggered is evaluated in an expression, it tests whether >> its operand sequence has reached its end point at that particular point in >> time. The result of triggered does not depend upon the starting point of the >> match of its operand sequence.* >> >> [Ben] Thus, the .*triggered *produces just a boolean that identifies the >> end point of a sequence, regardless of when it started. I read this as also >> stating that if a sequence has a range, it may have multiple threads, and >> each matching thread generates an individual end point. Since the result of >> a *.triggered* is a boolean, and not as a sequence, I claim that the >> result of *first_match*(sequence_instance.*triggered*) is same >> as sequence_instance.*triggered. * >> >> Here is the situation: >> >> * sequence *q_b*; @ (posedge clk) $rose(*a) *##*[1:*$*] b;* >> endsequence *: q_b >> >> P1: *assert property* ( >> >> @ (*posedge *clk) * first_match(*q_b.*triggered*) |=> c); >> >> Assume that "a==1" for ONLY ONE cycle, and false forever thereafter >> (i.e., a has a single $rose. ) >> >> Assume that "b==1" for all cycles. // thus q_b has a successful attempt, >> and has multiple threads. >> >> Assume that "c==0" for all cycles. // property fails for any of the >> threads. >> >> >> >> In this model, sequence q_b has multiple threads for the 1st successful >> attempt. I claim that the antecedent* first_match(q_b.triggered)* has >> multiple threads, and not one thread*. * Thus, the *first_match* does >> nothing because each end point of q_b.*triggered *is a boolean >> expression, and *first_match* of a boolean is same as boolean. >> >> I tested this on one simulator, and it behaved that way. >> >> Ben cohen >> >> >> -- >> This message has been scanned for viruses and >> dangerous content by *MailScanner* <http://www.mailscanner.info/>, and is >> >> believed to be clean. >> >> --------------------------------------------------------------------- >> >> Intel Israel (74) Limited >> >> >> >> This e-mail and any attachments may contain confidential material for >> >> the sole use of the intended recipient(s). Any review or distribution >> >> by others is strictly prohibited. If you are not the intended >> >> recipient, please contact the sender and delete all copies. >> >> >> -- >> 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 Mon Oct 26 08:53:24 2009
This archive was generated by hypermail 2.1.8 : Mon Oct 26 2009 - 08:54:31 PDT