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

1 checker gen_mutex( output bit out1, out2);
2 default clocking @$global_clock; endclocking
3 rand bit x, y;
4 m1: assume property ($onehot0({x, y}));
5 assign {out1, out1} = {x, y};
6 endchecker : gen_mutex

Fig. 23.3 Synthesizable testbench generating mutually exclusive stimuli

clock and advance the simulation time. Function randomize (Line 16 ) randomizes
values of class member variables x and y taking mutual exclusion constraint c into
account. Lines 17 - 18 assign the generated values of x and y to output ports out1
and out2 of the program.

t

Compare now the implementation of Example 23.30 with the checker-based
implementation shown in Example 23.31 .

Example 23.31. Checker-based implementation of mutually exclusive stimuli.
This implementation is shown in Fig. 23.3 . Here, x and y are free variables
(Line 3 ), and they are randomized by assumption m1 (Line 4 ). What remains is
to copy the values of the free variables to the checker output ports, which is done by
the continuous assignment statement on Line 5 . We have to copy the free variables
to the output ports because the checker ports cannot be free variables. t

We conclude this section with a more meaningful example of a synthesizable
testbench. This testbench implements a packet generator for the 1-bit serial interface
described in Sect. 1.2.1 . The output of the testbench is the input of a DUT that
we need to verify. The packet generator produces packets and transmits them as
transactions bit by bit to the DUT. The verbal specification of the serialization
protocol is as follows.

TX1 The following packet (or transaction) types are supported:

￿Data
￿ Control
￿Void

These types are encoded using the following enumeration:
typedef enum logic [1:0] {
txa_data = 2'b10,
txa_control = 2'b01,
txa_void = 2'b00,
txa_forbid = 2'b11
} txa_t;
txa_forbid indicates the forbidden combination of bits.
TX2 All packets have the same size. Each packet consists of a type field, tag
field and data field. The corresponding SystemVerilog type definitions are as
follows: