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 Line: 17
# ** Info: done memory load
#    Time: 300 ns  Scope: seq_trigger2.a1 File: seq_trigger2.sv Line: 10
# ** Info: done memory load with triggered
#    Time: 800 ns  Scope: seq_trigger2.a1b File: seq_trigger2.sv Line: 17
# ** Info: done memory load
#    Time: 800 ns  Scope: seq_trigger2.a1 File: 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>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]
> *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> 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.