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

a12: assert property (start_t && 2'b10 == in_data ##1 end_t[->1]
|-> out_data == 2'b10);
a13: assert property (start_t && 2'b11 == in_data ##1 end_t[->1]
|-> out_data == 2'b11);
Thus, specifying rigid variable data is equivalent to checking the data correspon-
dence for all possible in_data values. 16
We can rewrite assertion a1 using local variables instead of rigid variables:
checker data_consistency2(start_t, end_t, in_data, out_data,
event clk = $inferred_clock,
untyped rst = $inferred_disable);
default clocking @clk; endclocking
default disable iff rst;

property data_consistent;
var type (in_data) data;
(start_t, data = in_data) ##1 end_t[->1]
|-> out_data == data;
endproperty : data_consistent

a2: assert property (data_consistent);
endchecker : data_consistency2
Using rigid variables in checker data_consistency1 is even syntactically similar
to local variables, only instead of assigning to a local variable, there is a comparison
with a rigid variable. In this sense, local and rigid variables are interchangeable
when in the beginning of the transaction they store a value of some data and then
check this value later during the transaction.

t

23.4.2 Rigid Variable Support in Simulation

In simulation, rigid variables are randomly initialized, and then their values remain
unchanged. If there are assumptions imposed on rigid variables, a simulator does not
have any obligation to take these assumptions into account when assigning initial
random values to rigid variables. Therefore, there is no guarantee to fulfill even
straightforward assumptions imposed on rigid variables.
The simulation of rigid variables does not fully reflect their nature. Instead
of checking an assertion for all possible values of rigid variables, only one
random value is checked. For instance, if in simulation of checker same2 from
Example 23.28 , variable i was initialized with 47, only equality of the 47-th bit
in two words would be checked.

16 In PSL, the construct similar to rigid variables is even called forall .