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.

                            Copy code
                        
propertyexpr ::= 
...
| sequenceexpr |-> propertyexpr
| sequenceexpr |=> propertyexpr

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

Overlapped Implication

                            Copy code
                        
property nandprop;
     nandsigo |-> !(nandai && nandbi);
endproperty;

assertnand: assert property(nandprop);

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

                            Copy code
                        
property dprop;
     $changed(dout) |=> (dout == $past(din));
endproperty;

assertdprop: assert property(dprop);

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