Advanced Properties - SVA: The Power of Assertions in SystemVerilog - page 222

Case

Property case is a generalization of if - else for a multiple-valued condition b .
case (b)
b1: p1;
...
bN: pN;
default :p;
endcase
The property case (b)... is true iff either pi evaluates to true for the first i
such that the value of bi matches the value of b ,orno bi matches the value of b
and if the optional default item property p is specified then it evaluates to true. If
the default case item is not specified and no bi matches the value of b , then the
property case is vacuously true.
A case operator can be used, for example, to define a property in which
a sequence delay varies based on some register value. Of course, for practical
purposes a small range of delays is assumed:

Example 10.7. property p( bit [2:0] delay);
case (delay)
0: a;
1: nexttime [1] a;
2: nexttime [2] a;
3: nexttime [3] a;
4: nexttime [4] a;
default : 1'b0; // delay too large
endcase
endproperty :p

t

The same property could be written using a chain of if - else property operators,
but the meaning of such nested operators is less obvious than when using the case
operator. It is left to the reader as an exercise at the end of the chapter to rewrite the
property in Example 10.7 using if - else .
Many of the following operators have been briefly described in Chap. 5 , and
their formal semantics can be found in Chap. 22 . Here, we provide an intuitive
recapitulation of the operators, further clarifying the distinction between the strong
and the weak forms and between the bounded and unbounded forms. The bounded
variants evaluate the operand property over finite, bounded numbers of clock ticks,
while the unbounded ones evaluate over indefinite but finite numbers of clock ticks.

10.3 Suffix Operators: Implication and Followed-By

The following are suffix operators:
￿ Suffix implications |-> and |=> .
￿ Followed-by operators (also named suffix conjunctions) #-# and #=# .