A property defines a behavior of the design. A property can be used for verification as an assumption, a checker, or a coverage specification.
Sequences are often used to construct properties. usage of sequences in properties brakes down the complexity. Sequence can be reused across various properties.
A property can be declared in any of the following:
A clocking block
A compilation-unit scope
Implication (if ..else)
overlapping implication (|->)
Non overlapping implication(||->)
EXAMPLE: property rule6_with_type(bit x, bit y);
##1 x |-> ##[2:10] y;
//antecedent |-> consequent
The left-hand operand sequence_expr is called the antecedent, while the right-hand operand property_expr is called the consequent.
if antecedent is false, then consequent is not cared and property is considered as vacuous success.
if antecedent is True and if consequent is false then property is considered as false.
if antecedent is True and if consequent is true then property is considered as true.
Consequent expression is evaluated on the same clock of antecedent.
EXAMPLE: a |-> b
Non Overlapping Implication
Consequent expression is evaluated on the next clock of antecedent