Hi Ben, I think that always @some_seq and always @some_seq.triggerred are not equivalent because always @some_seq.triggerred should trigger 2x when it is reset to 0 at the end of the time step. My 5 cents... ed From: ben cohen [mailto:hdlcohen@gmail.com] Sent: Sunday, October 25, 2009 6: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<mailto: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> [mailto: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<mailto:ben@systemverilog.us>; sv-ac@server.eda.org<mailto: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> [mailto: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<mailto:ben@systemverilog.us>; sv-ac@server.eda.org<mailto: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> [mailto: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<mailto: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 Sun Oct 25 15:57:29 2009
This archive was generated by hypermail 2.1.8 : Sun Oct 25 2009 - 15:58:25 PDT