Properties which contain sequence definitions are called sequence properties.Sequence properties are of three types.
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)
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).
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.
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
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
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
Hi , I am bit confused in the definition of strong and weak assertions . Does SVA really supports weak and strong signals ? In your example , you have put weak(b ##1 c) in both the places . So the actual assertion a |-> p1 , if a does not occur, formal tool will throw a vacuous pass . In that case what is the use for weak(b ##1 c) ?
Yes. SVA supports weak and strong signals. Please refer IEEE System Verilog Hardware Specification (1800-2012) Chapter 16.12.1 for more details.
But I am not sure if all formal tools support this.
If your formal tool has weak & strong implementation, below assertion passes even if “a” does not occur. This is the use case of weak. If you want assertion to be passed only with “a”, change it to strong.
weak(b ##1 c);
weak_assert : assert property (@(posedge clk) a |-> p1);
If you don’t specify weak and just sequence expression, all formal tools wont give you vacuous pass. Assert & assume directive should act as weak in some of the formal tools like jasper. This will be caught in cover directive, which will act as strong.
property p1; b ##1 c; endproperty
Hope this helps.
weak() is used in example of strong(). It seems to be copy paste error.