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.
property_expr ::= ... | sequence_expr |-> property_expr | sequence_expr |=> property_expr
There are two types of implication called overlapped and non-overlapped.
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:
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