SVA Properties II : Types

Sequence Properties

Properties which contain sequence definitions are called sequence properties.Sequence properties are of three types.

weak(sequence_expr)

If there is no finite prefix that witnesses inability to match the sequence_expr, `weak(sequence_expr)` evaluates to true. The following example shows a weak sequential property p1.

property p1; weak(b ##1 c); endproperty

weak_assert : assert property (@(posedge clk) a |-> p1);

An evaluation attempt of weak_assert assertion returns true in the following condition.

• Either a is false at the tick of posedge clk where the evaluation attempt starts OR
• ( b is true at the tick of posedge clk where the evaluation attempt starts AND
• if exists subsequent tick of posedge clk then c is true after 1 tick)

strong(sequence_expr)

If there is a nonempty match of the sequence_expr, `strong(sequence_expr)` evaluates to true. Strong(sequence_expr) requires only one match of a sequence expression to hold. So evaluation will be a `true` only if property strong(first_match(sequence_expr)) evaluates to true.

property p1; strong(b ##1 c); endproperty

strong_assert : assert property (@(posedge clk) a |-> p1);

An evaluation attempt of `strong_assert` assertion returns true in the following condition.

• a is true at the tick of posedge clk where the evaluation attempt starts AND
• b is true at the tick of posedge clk where the evaluation attempt starts AND
• In subsequent tick of posedge clk, c is true (after 1 tick).

sequence_expr

This means, property has sequence expression without strong or weak operators.If the strong or weak operator is omitted, then the evaluation of the sequence_expr depends on the verification directives used.- For assert or assume : sequence_expr is evaluated as weak(sequence_expr)

• For Cover or restrict : sequence_expr is evaluated as strong(sequence_expr)

Negation property

Negation property has the form "not property_expr"

assert_negprop : assert property (@clk not a ##1 b);

For each evaluation attempt of the property, there is an evaluation attempt of property_expr. Due to "not" operation along with the property_expr, evaluation of the property returns the opposite of the evaluation of the property_expr.

The "not" operator switches the strength as well. For example, in the above assertion, as strength is not mentioned and assert verification directive is used, it is considered as weak. This means that if clk stops ticking and 'a' holds at the last tick of clk then a ##1 b will hold, but assert_negprop fail.

It is better to use such cases in the following way.

assert_negprop : assert property (@clk not strong(a ##1 b));

Dis junction property

The property evaluates to true only if at least one of property_expr1 and property_expr2 evaluates to true. property_expr or property_expr

property myprop1; seq1 |=> out1 endproperty

property myprop2; seq1 |=> out1 endproperty

property myprop3; myprop1 or myprop2 endproperty

Conjunction property

The property evaluates to true only if both property_expr1 and property_expr2 evaluate to true. property_expr and property_expr

property myprop1; seq1 |=> out1 endproperty

property myprop2; seq1 |=> out1 endproperty

property myprop3; myprop1 and myprop2 endproperty

If-else property

A property is an if–else if it has either the following form:

if ( expression_or_dist ) property_expr

The above property evaluates to true if either expression_or_dist evaluates to false or property_expr evaluates to true.

if ( expression_or_dist ) property_expr else property_expr

The above propery evaluates to true if expression_or_dist evaluates to true and property_expr1 evaluates to true or expression_or_dist evaluates to false and property_expr2 evaluates to true.

property myprop1; if(in1 ^ in2) seq1 |=> (out1 == in3 and in2) else seq1 |=> (out1 == in2) endproperty

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