SystemVerilog Assertion
Part 4: Property Layer
Prev: Property Layer |
Next: Implication Operator
More Property Types
Property Type 5: A Conjunction
A conjunction is equivalent of a logical and operation, and
very aptly, is expressed by an and operator.
property conjunction_example;
sequence_example and inversion_example;
endproperty
(Similar to our last example, in this particular case, the
property conjuction_example will never be true.)
Property Type 6: An 'if...else'
An 'if...else' property expression is a conditional statement
that describes two possible behaviors based on the value of an
expression.
property ifelse_example;
if (expr == 2'b10)
// expr defined elsewhere
inversion_example;
else
sequence_example;
endproperty
The 'else' part is optional and can be omitted.
Property Type 7: An Implication
An implication property describes a behavior that occurs when
a preceeding behavior takes place. The implication operators
'|->' and '|=>' are used for describing such a property.
In the next example, the sequence s0 implies the occurance
of property sequence_example.
property implication_example;
s0 |-> sequence_example;
endproperty
Implications are perhaps the most important as well as most
commonly used form of property expression. This is why we will
devote an entire section on how to use implication operator.
But first, some more information on the operators that we just
learnt.
More on Property Operators and Expressions
Property Operators
Figure 7 shows the property operators from highest to lowest
precedence and associativity.
| Operator
| Associativity
|
| not
| not applicable (unary function)
|
| and
| left
|
| or
| left
|
| if...else
| right
|
| |-> |=>
| right
Figure 7. Property Operators
|
Property Expression Qualifiers
The property expression has two optional qualifiers. They are
(a) clocking event and (b) disable iff.
(a) The clocking event describes when a property expression should
take place. An example of this is shown below.
property clocking_example;
@(posedge clk) sequence_example;
endproperty
(b) A 'disable iff' command is similar to a reset statement - the
property expression is valid only if the reset situation is
lifted. Here is an example of this command.
property disable_iff_example;
disable iff (reset_expr) sequence_example;
endproperty
In this case, if reset_expr is true, the property
expression (sequence_example) is valid.
Prev: Property Layer |
Next: Implication Operator
|
