Ben, I think that using s.triggered in event control using @ is a bad idea to start with. The problem is that the triggered is supposed to hold true till the end of a time step. But by then, the simulator may not be able to process the event on the falling edge of triggered, hence you get one trigger. The behavior is not defined, as far as I can tell. The same thing applies to some event e.triggered. s.triggered and e.triggered should be used with wait statements, not @. Best regards, ed From: ben cohen [mailto:hdlcohen@gmail.com] Sent: Sunday, October 25, 2009 7:00 PM To: Eduard Cerny Cc: Havlicek John-R8AAAU; 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 ? Ed, Given the model below, would you say that a simulator is in error if the reported action blocks are as follows because we see one trigger and not 2 triggers? If I had 2 triggers, then I would see the info "done memory load with triggered" twice. But I don't !!! Sim results: ** Info: done memory load with triggered # Time: 300 ns Scope: seq_trigger2.a1b File: seq_trigger2.sv<http://seq_trigger2.sv> Line: 17 # ** Info: done memory load # Time: 300 ns Scope: seq_trigger2.a1 File: seq_trigger2.sv<http://seq_trigger2.sv> Line: 10 # ** Info: done memory load with triggered # Time: 800 ns Scope: seq_trigger2.a1b File: seq_trigger2.sv<http://seq_trigger2.sv> Line: 17 # ** Info: done memory load # Time: 800 ns Scope: seq_trigger2.a1 File: seq_trigger2.sv<http://seq_trigger2.sv> Line: 10 //Code module seq_trigger2; logic clk =1, load_mem=0, done=0, ready=0, ready2=0; sequence qDoneSetup; @ (posedge clk) first_match($rose(load_mem) ##[0:5] done); endsequence : qDoneSetup cp_qDoneSetup: cover property (qDoneSetup); always @ qDoneSetup begin : a1 // The trigger point using the end point of the sequence $info( "done memory load" ); ready <= 1'b1; @ (posedge clk) ready <= 1'b0; end : a1 always @ qDoneSetup.triggered begin : a1b // The trigger point using the end point of the sequence $info( "done memory load with triggered" ); ready2 <= 1'b1; @ (posedge clk) ready2 <= 1'b0; end : a1b initial forever #50 clk = !clk; always @ (posedge clk) begin repeat (100) @ (posedge clk); $display("end of simulation"); $stop; end always @ (posedge clk) assert (randomize(load_mem, done)); endmodule : seq_trigger2 On Sun, Oct 25, 2009 at 3:50 PM, Eduard Cerny <Eduard.Cerny@synopsys.com<mailto:Eduard.Cerny@synopsys.com>> wrote: 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<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<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 ? 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 Mon Oct 26 06:58:46 2009
This archive was generated by hypermail 2.1.8 : Mon Oct 26 2009 - 06:59:56 PDT