Assertions - Implications

The implication construct (|->) allows a user to monitor sequences based on satisfying some criteria, e.g. attach a precondition to a sequence and evaluate the sequence only if the condition is successful. The left-hand side operand of the implication is called the antecedent sequence expression, while the right-hand side is called the consequent sequence expression.

If there is no match of the antecedent sequence expression, implication succeeds vacuously by returning true. If there is a match, for each successful match of the antecedent sequence expression, the consequent sequence expression is separately evaluated, beginning at the end point of the match.

There are two forms of implication: overlapped using operator |->, and non-overlapped using operator |=>.

For overlapped implication, if there is a match for the antecedent sequence expression, then the first element of the consequent sequence expression is evaluated on the same clock tick.

s1 |-> s2;

In the example above, if the sequence s1 matches, then sequence s2 must also match. If sequence s1 does not match, then the result is true.

For non-overlapped implication, the first element of the consequent sequence expression is evaluated on the next clock tick.

s1 |=> s2;

The expression above is basically equivalent to:

`define true 1
s1 ##1 ‘true |-> s2;

where `true is a boolean expression, used for visual clarity, that always evaluates to true.