Checkers - SVA: The Power of Assertions in SystemVerilog - page 205

9.4.1.1 Functions in Checkers

The following restrictions are imposed on functions used on the right-hand side of
checker variable assignments:

￿ The functions should not contain output or ref arguments ( const ref is
allowed).
￿ The functions should be automatic and not preserve any state information in static
variables. The functions must not have side effects.

These restrictions are the same as imposed on function calls in concurrent
assertions.

9.4.2 Sampling in Checkers

As we saw in Sect. 9.1.2 the expressions in the right-hand side of nonblocking
assignments in checkers are sampled. This is necessary to make assertion modeling
in checkers deterministic and consistent with the behavior of concurrent assertions.

Example 9.23. In the following piece of code there would be a race without variable
sampling: if b changes before clk , variable a would contain the past value of b ,
otherwise it would contain the current value of b .
always_ff @( posedge clk)a<=b;
If the value of b is sampled, a would contain the past value of b regardless of the
race between b and clk .

t

The exact rule of expression sampling in always_ff procedures reads as follows:

All expressions in an always_ff procedure are sampled, except for variables
used in the event control.

From this rule it follows that the expressions in non-temporal assertions (imme-
diate, deferred or final) instantiated in this procedure are also sampled. Expressions
in other always procedures always_comb and always_latch are not implicitly
sampled.

Example 9.24. The code below is a slightly modified example borrowed from the
LRM [ 8 ]. In the comments, CV and SV stand for “current value” and “sampled
value” respectively.