Introduction - SVA: The Power of Assertions in SystemVerilog - page 25

1 logic end_reset, operational, enter_deadlock_area, stuck, clk;
2 // ...
3 property forever_n(x, n);
4 nexttime [n] always x;
5 endproperty
6 a1: assert property (@( posedge clk)
7 end_reset |-> forever_n(operational, 100));
8 a2: assert property (@( posedge clk)
9

enter_deadlock_area |-> forever_n(stuck, 5));

Fig. 1.12 Property reuse

request should be granted ( grant = 1 ) in the next cycle, and one cycle later grant
should be deasserted.
We describe sequences in Chaps. 6 and 11 .

Property Reuse

Like expressions and sequences, properties may also be assigned a name to be used
in concurrent assertions, as shown in Fig. 1.12 .
In this example, forever_n is a property specifying that after n clock cycles
(operator nexttime [n] ) x should be true forever (operator always ). This property
is then reused in assertions a1 and a2 . Assertion a1 states that 100 clock cycles after
reset phase was completed ( end_reset asserted) the device should be operational
forever ( operational should always be high). Assertion a2 states that 5 cycles after
entering a deadlock area ( enter_deadlock_area asserted) signal stuck should be
asserted forever.
We describe properties in Chaps. 5 and 10 .

Assertion Libraries

Although the language features for naming an expression, a sequence or a property
are beneficial for reuse in writing individual assertions, they are not sufficient
for building a library of assertions. Commonly, an element from an assertion
library encapsulates one or more related assertions, and some code to support the
expressions used within the assertions, such as an FSM state or a variable value
computed from a function.
A more suitable feature than what we have described so far is a checker .
The checker construct is similar to a module in that it can contain assertions
and modeling code, but its instantiation and parameterization accommodate the
flexibility and usage that are specific to assertions.