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;
(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
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;
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;

(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;
In this case, if reset_expr is true, the property expression (sequence_example) is valid.

Prev: Property Layer | Next: Implication Operator


Verification Management
Join Verification Management Group

Shop Amazon - Contract Cell Phones & Service Plans

Book of the Month