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.