SVA Properties III : Implication

The implication construct (|->) allows a us to monitor sequences based on satisfying some criteria, i.e. for a sequence to occur, a preceding sequence must have occurred. The implication consists of left-hand-side called antecedent, an implication operator and right-hand-side called consequence. The implication is a construct located between antecedent and consequence and if there is a successful match of antecedent, the consequence will be evaluated. The implication will return TRUE if the evaluation of the consequent succeeds and returns TRUE.If there is no match of the antecedent, the evaluation of the implication succeeds vacuously and returns TRUE. The implication can be used only inside property and not inside sequence.

Implication syntax.

property_expr ::= 
...
| sequence_expr |-> property_expr
| sequence_expr |=> property_expr

There are two types of implication called overlapped and non-overlapped.

Overlapped Implication

property nand_prop;
     nand_sig_o |-> !(nand_a_i && nand_b_i);
endproperty;

assert_nand: assert property(nand_prop);

In the overlapped (|->) implication, from a given start point antecedent will be evaluated. If there is:

No match: The evaluation of the implication from that start point succeeds and returns true. [Vacuous success]

Match : The consequent is separately evaluated. The end point of the match of the antecedent is the start point of the evaluation of the consequent.

Non-overlapped Implication

property d_prop;
     $changed(dout) |=> (dout == $past(din));
endproperty;

assert_d_prop: assert property(d_prop);

More about properties can be found in other sections of “SVA Properties” series