Implication Operator

The implication operator does a property check conditionally if the sequential antecedent is matched.

Syntax:

sequence_exp |-> property_exp
sequence_exp |=> property_exp

The LHS operand sequence_exp is called an antecedent

The RHS operand property_exp is called a consequent

Type of Implication

The overlapped implication operator is denoted by the |-> symbol.

The evaluation of the consequent starts immediately on the same clock cycle if the antecedent holds true.

The consequent is not evaluated if the antecedent is not true.

Example:

property prop;
  @(posedge clk) valid |-> (a ##3 b);
endproperty

The non-overlapped implication operator is denoted by the |=> symbol.

The evaluation of the consequent starts in the next clock cycle if the antecedent holds true.

The consequent is not evaluated if the antecedent is not true.

Example:

property prop;
  @(posedge clk) valid |=> (a ##3 b);
endproperty