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

Example 9.21. The following code is illegal as the checker variable a is referenced
by its hierarchical name mycheck.a in the assignment of b .
checker check(...);
bit a;
...
endchecker : check

module m_illegal(...);
...
check mycheck(...);
...
wire b;
assign b = mycheck.a;
endmodule :m
In other words, it is forbidden to assign or use checker variables from the outside
of the checker (see Sect. 9.2.2 ).

t

Example 9.22. We can generalize the checker stable_for_two_ticks from
Example 9.19 to check the signal stability for n clock ticks. For this purpose,
we introduce a counter ctr , and we allow sig to change only when ctr is 0. The
system function $clog2 returns the number of bits necessary to store the value of n .
checker stable_for_n_ticks(sig, n,
event clk = $inferred_clock,
untyped rst = $inferred_disable);

default clocking @clk; endclocking
default disable iff rst;
bit [$clog2(n)-1:0] ctr = '0;

always_ff @clk begin
if (rst) ctr <= 1;
else if (ctr == n - 1) ctr <= 0;
else ctr <= ctr + 1;
end

a1: assert property ($changed(sig) |-> ctr == 0);
endchecker : stable_for_n_ticks

Discussion: We could declare ctr as int unsigned , and this solution would work
perfectly well in simulation. For efficiency of formal verification it is important to
declare all variables with the smallest possible size. This is why we use the system
function $clog2 to designate the smallest variable size. t

To make checkers efficient in FV, checker variables should be of the smallest
size sufficient to store the desired values.