SystemVerilog Assertion

Next: Recursive Property | Next: The 'assume' statement

In Part 4, we saw how a property describes the behavior of a logic. We also mentioned that a property by itself does not participate in any way in a simulation or verification process. In order for a property to be meaningful to a verification tool, you must use associate it with, what is known as, a sense. In this concluding part about SystemVerilog assertion, we will look into how to associate a sense to a property.

Associating a Sense with a Property

A property describes a logic behavior. But how do you use this behavior in a simulation? In order to use this property in simulation, you must associate a sense with the property. A sense describes how a property is supposed to be used. Is the behavior that a property describes is assumed to be true, or does the behavior need to be checked during simulation? Do we want to measure the coverage of the behavior described by a property or do we simply want to wait for the various events within the behavior to take place? All of these define a sense for a property. A property can be associated with only one sense at a time.

To associate a sense on each of the above occasions, SystemVerilog assertion uses a separate keyword. Here are the keywords that define a sense for an assertion.

1. assert: The keyword assert indicates that a property acts a checker. The verification environment should check if the behavior occurs.
2. assume: The assume keyword indicates that the property behavior is anticipated or assumed and should be treated so by the verification tool.
3. cover: If a property is associated with the keyword cover, it indicates that the property evaluation will be monitored for coverage.

When a property is associated with a sense keyword, the entire concurrent assertion can be specified inside any of the following places:

• an always block
• an initial block
• a module
• a program
• an interface

 
   assert property (p1);

   always 
      assert property (p1);

The 'assert' Statement

When a propoerty is associated with an assert statement, verification tools treats the property as a checker. When the property has a match, a block of code commonly called 'pass block' is executed. Optionally, a similar 'fail block' of code can be specified that executes upon failure of the property. The following example shows this. The property for this example is taken from our earlier discussion.

 
   property top_prop;
      seq0 |-> prop0;
   endproperty 

   assert_top_prop: 
   assert property (top_prop) begin 
      int pass_count;

      $display ("Pass: top_prop");
      pass_count = pass_count + 1'b1;
   end

1. An assert statement is a named block and optionally can be assigned a name (such as, assert_top_prop in the current example).
2. If there is no 'else' part given in an assert statement, an implied $error statement is assumed.
3. A pass block or fail block can not contain other assert, assume or cover statements.

Prev: Recursive Property | Next: The 'assume' statement