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

23.5 Checkers as Generators

Checkers may be used as input stimuli generators for a DUT, i.e., as a synthesizable
testbench. The major advantage of such a testbench is its natural support both in
simulation and in FV. Writing synthesizable testbenches saves the effort spent on
creation of two different environments. A synthesizable testbench is useful even
when created only for FV because it provides an excellent tool for debugging the
FV model correctness in simulation.
Let us start with a simple example in which two inputs of a DUT are restricted to
be mutually exclusive. For simplicity we assume that these inputs are of type bit .
Example 23.30. Conventional implementation of mutually exclusive stimuli.
Using conventional SystemVerilog testbench constructs — programs, classes,
randomization and constraints, — this testbench may be implemented as shown
in Fig. 23.2 . The program implementing this testbench declares class Mutex
(Lines 2 - 7 ) to represent a data structure for two random bits. These bits are defined
on Line 3 .Here rand qualifier specifies only randomness; it is not to be confused
with the checker specification of free variables. These random bits are constrained
using the SystemVerilog constraint construct (Lines 4 - 6 ). This constraint has
name c , and its body contains a condition for the mutual exclusion of x and y
(Line 5 ).
The stimuli are generated in the initial procedure of the program
(Lines 11 - 20 ). Line 9 instantiates class Mutex and names the created object vals .
The value generation is done in the loop (Lines 13 - 19 ). Lines 14 - 15 generate the

1 program gen_mutex( output bit out1, out2, clk);
2

class Mutex;

rand bit x, y;

3

constraint c{

4

$onehot0({x, y});

5

}

6

endclass : Mutex

7

8
9

Mutex vals = new ;

10
11 initial begin
12 clk = 1'b1;
13 for ( int i = 0; i < 100; i ++) begin
14 #5 clk = !clk;
15 #5 clk = !clk;
16 vals.randomize();
17 out1 = vals.x;
18 out2 = vals.y;
19 end
20 end
21 endprogram : gen_mutex