In reply to jh_veryveri:
Yes these properties have similar and in some cases overlapping functionality. They all have the form Antecedent operator Consequent.
Implication is the most common and has the form
sequence_expr_A |-> property_expr_C
This means the property_expr must be true starting from the cycle that sequence_expr has a match. When the sequence_expr is just a 1-cycle boolean expression, you can write this as
if ( boolean_expr ) property_expr
// same as
boolean_expr_A |-> property_expr_C
Most people still chose the implication using using a simple if. The expressiveness comes from using the if with an accompanying else
if ( boolean_expr_A ) property_expr_C1 else property_expr_C2
// same as
boolean_expr_A |-> property_expr_C1
! boolean_expr_A |-> property_expr_C2
property_expr_A implies property_expr_C
The above property overlaps the functionality of implication when the antecedent is just a 1-cycle boolean expression. However when the antecedent is a sequence or property, the consequent gets evaluated concurrently with the antecedent instead of waiting for the antecedent to become true. This implies property operator is for very complicated properties and usually involved nested multi-clock implication properties.