SystemVerilog Assertion

Prev: Property Types | Next: Recursive Property

Implication Operators

As we mentioned earlier, an implication refers to a situation in which in order for a behavior to occur, a preceding sequence must have occured. This preceding sequence in this case is known as antecedent. The suceeding behavior is known as consequent. Thus, in other words, an antecedent sequence implies a consequent property expression. This is shown by the following notation:

   antecedent |-> consequent;

The property top_prop is an example that demonstrates this. In this example, seq0 is a sequence that as an antecedent implies the consequent property expression prop0. The sequence seq0 matches when signal sig_a appears two clocks before sig_b. The property prop0 consists of another sequence seq1 that matches when signal sig_d follows sig_d after 5 clock ticks.

   property top_prop;
      seq0 |-> prop0;
   endproperty 

   property prop0;
      seq1;
   endproperty 

   sequence seq0;
      sig_a ##2 sig_b;
   endsequence 

   sequence seq1;
      sig_c ##5 sig_d;
   endsequence 

Equivalently, top_prop can also be written as:

   property top_prop;
      (sig_a ##2 sig_b) |-> (sig_c ##5 sig_d);
   endproperty 

A closer look into an implication type property definition reveals several of its characteristics.

1. An antecedent sequence (such as seq0 in the above example) in general may match zero, one or more than one time.
2. If there is no match for the antecedent sequence, that is, if seq0 never occurs, even then the property top_prop evaluates to be true. This is known as Vacuous Success.
3. The end point of matching an antecedent sequence is the start point of evaluation of the consequent property expression.
4. An antecedent may match even when the consequent is being evaluated for a previous match. Each match of the antecedent will result in separate thread of evaluation for the consequent. As an example, let us assume that seq0 has a match. This results in a match of prop0. Let us further assume that sig_c is asserted and the only other requirement for a match of prop0 (or of seq1) is an assertion of sig_d after 5 clock ticks. When two of these five clock ticks are over, seq0 has another match. In this case, a separate thread for evaluation of top_prop will be created for this second match of seq0. The whole property evaluates to be true if and only if all such threads return a true value between a given start and end point pair.

The Implication Operator '|=>'

For the implication operator |=> the consequent property expression is evaluated one clock tick after the antecedent sequence ends. This means a property expression

   antecedent |=> consequent; 

   antecedent ##1 `true |-> consequent; 

More Examples of Implication

Here are some more examples of implication operators for various types of property expressions.

Clocking Event

An antecedent sequence and a consequent property expression both may have a clocking event associated with them.

   property clk_implication_example;
      @(posedge src_clk) seq0 |=> @(posedge dst_clk) prop0;
   endproperty 

Other Types of Property Expressions

An implication can be used along with any other type of property expression. For instance, an 'if...else' type property expression can nest implication.

   property top_prop;
      if (sig_back2back) 
         seq0 |-> prop0;
      else 
         seq0 |=> prop0;
   endproperty

Prev: Property Types | Next: Recursive Property