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:
- Number of times the property is attempted (but may not
have succeeded.
- Number of times the property has succeeded.
- Simlarly, number of times the property has failed.
- 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
|
