Checkers in Formal Verification - SVA: The Power of Assertions in SystemVerilog - page 508

23.2 Checker Modeling with Free Variables

Free variables may participate in regular checker modeling, though some limitations
apply. In this section we discuss the semantics of free variables in the context of
checker modeling and the specifics of their usage.

23.2.1 Free Variable Initialization

Free variables may be initialized with a declaration assignment. Initialization
constrains only the initial value of a free variable; its values at other times are not
affected by the initialization.

Example 23.7. Consider the following checker:

checker check1;
rand bit rst = 1'b1;
bit a = 1'b0;
bit b = 1'b0;

default clocking @$global_clock; endclocking
default disable iff rst;

always_ff @$global_clock
a <= 1'b1;

a1: assert property (a);
a2: assert property (b);
endchecker : check1
The first tick of the global clock happens at time 0, and both assertions a1 and a2 are
disabled since the value of rst at time 0 is 1 . At the next tick of the global clock, a1
either is disabled or passes because the value of a has been set to 1 . On the contrary,
the assertion a2 fails because b is always 0 (it is not a free variable, so it keeps its
value until it is again assigned), while rst is constrained only in global clock tick 0.
For example, the trace rst D 1 ; 0 ;::: violates assertion a2 .
Now, let us modify our checker to be controlled by some general clock:
checker check2( event clk);
rand bit rst = 1'b1;
bit a = 1'b0;
bit b = 1'b0;

default clocking @clk; endclocking
default disable iff rst;

always_ff @clk a <= 1'b1;

a1: assert property (a);
a2: assert property (b);
endchecker : check2