SystemVerilog Assertion

Part 5: Property Layer

Prev: Associating sense | Next: The 'expect' statement

The 'assume' Statement

A property associated with an assume statement implies that the property holds during verification. However, an assume statement means different actions for a formal tool and a simulation.

For a formal or dynamic simulation environment, the statement is simply assumed to be true and rest of the statements that need to be verified are constrained accordingly.

For a event or cycle base simulation, the property associated with an assume statement is also checked to see if it holds and if it does, then the rest of the properties associated with this assumed statement are checked. If the property associated with the assume statement is found not to be true, the simulation fails. No action is taken if it passes.

The following example shows how to use an assume statement. Here, We use the same properties as before, but this time, we assume that seq0 does not match when active high synchronous reset is asserted.

 
   assume_property_reset_seq0: 
   assume property (reset_seq0);

   property reset_seq0;
      @(posedge clk) reset |-> not seq0;    
   endproperty

   property top_prop;
      seq0 |-> prop0;
   endproperty 

   ...

Note that we could write the above statement as below without changing the sense.

   assume_property_reset_seq0: 
   assume property @(posedge clk) 
      reset |-> not seq0;    

   property top_prop;
      seq0 |-> prop0;
   endproperty 

   ...

The 'cover' Statement

A cover statement measures the coverage of the various components (expressions, sequences, or other properties) of a property. The following example shows how to do this:

   cover_property_top_prop: 
   cover property (top_prop) 
      $display ("top_prop is a hit");

   property top_prop;
      seq0 |-> prop0;
   endproperty 

   ...
In this case, the cover statement cover_property_top_prop will print "cover_property_top_prop" whenever the property top_prop succeeds. In addition, the results of a coverage statement include:
  1. Number of times the property is attempted (but may not have succeeded.
  2. Number of times the property has succeeded.
  3. Simlarly, number of times the property has failed.
  4. Number of times the property had a vacuous success.
The last item needs more detailed look. In our previous example, if seq0 is never true, will the property top_prop be considered as a pass or fail? Since, seq0 never succeeded, prop0 will never be checked and hence top_prop will not fail. This is called a vacuous success and a cover statement should report the number of such a success.

Prev: Associating sense | Next: The 'expect' statement

Share/Save/Bookmark



Verification Management
Join Verification Management Group


Book of the Month


From Our Press