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

    3 comments on “SVA Properties II : Types

    1. Ayanava

      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) ?

      Reply
      1. Sini Balakrishnan Post author

        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.

        property p1;
        weak(b ##1 c);
        endproperty
        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.

        Reply

    Leave a Reply

    Your email address will not be published. Required fields are marked *