Coverage - SVA: The Power of Assertions in SystemVerilog - page 417

1 typedef enum {
2 info = 2'b10, control = 2'b01, void = 2'b00, forbid = 2'b11
3 } kind_t;
4 typedef logic [5:0] tag_t;
5 typedef logic [23:0] data_t;
6 typedef struct {
7 kind_t kind; tag_t tag; data_t data;
8 } packet_t;
9 typedef struct { logic ack_received; tag_t tag; } ack_t;
10
11 checker spec (
12

packet_t tx_packet, // Packet to be transmitted

rx_packet, // Last received packet

13

logic sent, // Packet sent

14

ack_t ack, // Acknowledge

15

logic timeout, // Timeout active

16

logic err, // Error signal

17

event clk, // System clock

18

logic rst // Reset

19

20 );
21 default clocking @clk; endclocking
22 default disable iff rst;
23
24 ...same as before...
25
26 // coverage of different packet types
27 let packet_sent_type(packet_t packet, kind_t kind) =
28 sent && packet.kind == kind;
29 cov_kinds_tx_info: cover property (
30 packet_sent_type(tx_packet, info));
31 cov_kinds_tx_void: cover property (
32 packet_sent_type(tx_packet, void));
33 cov_kinds_tx_control: cover property (
34

packet_sent_type(tx_packet, control));

35
36 // coverage of packet types transmission and acknowledgment.
37 property tx_rx_ack(kind_t kind);
38 tag_t tag;
39 (sent && tx_packet.kind == kind, tag = tx_packet.tag)
40 #=# s_eventually (ack.ack_received && ack.tag == tag);
41 endproperty
42
43 cov_sent_ack_info: cover property (tx_rx_ack(info));
44 cov_sent_ack_void: cover property (tx_rx_ack(void));
45 cov_sent_ack_control: cover property (tx_rx_ack(control));
46
47 endchecker : spec

Fig. 18.1 System specification with coverage