Subject: Re: [sv-ac] Missed point about first_match (sequence_expr)
From: John Havlicek (john.havlicek@motorola.com)
Date: Thu Apr 10 2003 - 12:40:10 PDT
Hi Adam:
> Good afternoon;
>
> I missed asking this question.
>
> On page 189, it states, "The result of property evaluation is either true or false. ...
> This is accomplished by implicitly transforming sequence_expr to
> first_match(sequence_expr). As soon as a match is determined the result is considered
> to be true and no other matches are required.
> However for implication, then the semantics of implication determine whether the
> property is true or false.
>
>
> So assert property (sequence)
>
> will only result in a single pass or fail.
>
> For an implication, it is thus possible for a property to pass and fail multiple times?
> Is this how this should be read?
No. If I assert
assert property (sequence1 |-> sequence2)
at clock tick t, then this assertion as whole passes iff every match of
sequence1 starting at t is followed in the overlapping way by some match of
sequence2. The assertion as a whole fails iff there is some match
of sequence1 starting at t that is not followed in the overlapping way
by any match of sequence2.
It would be interesting for property coverage to know about all the matches
of sequence1 starting at t and whether each such match is or is not followed
by a match of sequence2. But this information should not be considered as
multiple passes and fails of the assertion. It is the totality of this information
that determines whether the overall assertion passes or fails.
Best regards,
John H.
>
> This seems inconsistent to me. At least, we should explain this when implication is
> used, so that we are clear.
>
> Any other comments on this?
>
>
> Adam
>
>
>
This archive was generated by hypermail 2b28 : Thu Apr 10 2003 - 12:41:39 PDT