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

typedef bit [5:0] tag_t;
typedef bit [23:0] data_t;
typedef struct packed {
txa_t txa;
tag_t tag;
data_t data;
} packet_t;
TX3 The serialized data is sent to tx_data input pin of the DUT. The validity of
the data bit is indicated by the assertion of tx_valid DUT input pin. There
are two versions of the serialization protocol: normal and quiet . In the quiet
mode it is required that tx_data be set to zero when tx_valid is deasserted.
TX4 Each packet is transmitted bit by bit, from LSB to MSB, one bit per clock
cycle.
TX5 During reset an active transaction, if any, is aborted.
TX6 Packets are transmitted sequentially. Transmission of a different packet is
allowed only when the current packet has been fully transmitted, or when its
transmission has been aborted because of a reset.
TX7 Each packet my be retransmitted according to the internal logic of the
transmitter.
TX8 There are no timing constraints imposed on the transmission of two consecu-
tive packets or on the retransmission of the same packet. Back-to-back packet
transmission is allowed.

Checker tx implementing this testbench is shown in Figs. 23.4 and 23.5 .
Fig 23.4 shows the checker interface and several internal declarations. Input checker

1 checker tx(QUIET = 1'b0,
2

event clk = $inferred_clock,

untyped rst = $inferred_disable,

3

output bit tx_valid, tx_data

4

5 );
6

default clocking @clk; endclocking

default disable iff rst;

7

8
9

let legal_txa(txa) = txa != txa_forbid;

10
11

rand bit valid;

rand bit data;

12

rand bit packet_start;

13

rand bit new_packet;

14

rand packet_t packet;

15

16
17 assign tx_valid = valid;
18 assign tx_data = data;
19 ...
20 endchecker :tx

Fig. 23.4 Packet generation for 1-bit serial interface. Checker skeleton