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

is equivalent to

const bit [3:0] r = 4'd5;
We will always assume that rigid variables are uninitialized. Of course, it is
illegal to assign a rigid variable, as it is illegal to assign any constant variable.

Example 23.28. Checker same1 verifies that two large data words contain the same

value:

checker same1( bit [127:0] word1, word2,
event clk = $inferred_clock);
a1: assert property (@clk word1 == word2);
endchecker : same1
This equality check is expensive as the size of the words is big. For some FV tools, 15
it might be more efficient to choose an arbitrary bit and check that its values in both
words coincide. This may be achieved by introducing a rigid variable i that indicates
which bit in the words to compare, as implemented in checker same2 :
checker same2( bit [127:0] word1, word2,
event clk = $inferred_clock);
rand const bit [6:0] i;
a2: assert property (@clk word1[i] == word2[i]);
endchecker : same2
Assertion a2 compares only one bit in two words instead of comparing 128 bits as in
assertion a1 . This comes, however, at a price of introducing a 7-bit rigid variable i .
t

Example 23.29. Checker data_consistency1 verifies that out_data at the end of
a transaction ( end_t asserted) has the same value as in_data at the beginning of
the transaction ( start_t asserted).
checker data_consistency1(start_t, end_t, in_data, out_data,
event clk = $inferred_clock,
untyped rst = $inferred_disable);
default clocking @clk; endclocking
default disable iff rst;
rand const var type (in_data) data;

a1: assert property (start_t && data == in_data ##1 end_t[->1]
|-> out_data == data);
endchecker : data_consistency1
Assume for simplicity that both in_data and out_data are of type bit [1:0] .
Then assertion a1 is equivalent to the set of the four assertions:
a10: assert property (start_t && 2'b00 == in_data ##1 end_t[->1]
|-> out_data == 2'b00);
a11: assert property (start_t && 2'b01 == in_data ##1 end_t[->1]
|-> out_data == 2'b01);

15 It highly depends on the specific tool.