Introduction - SVA: The Power of Assertions in SystemVerilog - page 11

1 typedef enum logic [1:0] {
2 txa_data = 2'b10, txa_control = 2'b01,
3 txa_void = 2'b00, txa_forbid = 2'b11 } txa_t;
4 typedef logic [5:0] tag_t;
5 typedef logic [23:0] data_t;
6 typedef struct packed { txa_t txa; tag_t tag; data_t data; }
packet_t;
7 typedef struct packed { logic ack_received; tag_t tag; } ack_t;
8 checker spec (
9 packet_t tx_packet, // Packet to be transmitted
10 packet_t rx_packet, // Last received packet
11 logic sent, // Packet sent
12 ack_t ack, // Acknowledge
13 logic timeout, // Timeout active
14 logic err, // Error signal
15 event clk, // System clock
16 logic rst); // Reset
17 default clocking @clk; endclocking
18 default disable iff rst;
19 // Legal transaction type
20 let legal_txa(txa) = txa != txa_forbid;
21 // Non-void packet sent
22 let packet_sent = sent && tx_packet.txa != txa_void;
23 // Right acknowledgment received
24 let right_ack = ack.ack_received && ack.tag == tx_packet.tag;
25 // Transmitted packet is always legal
26 tx_packet_legal: assert property (legal_txa(tx_packet.txa))
27 else $error("Transmitted packet is malformed");
28 // Received packet is always legal
29 rx_packet_legal: assert property (legal_txa(rx_packet.txa))
30 else $error("Received packet is malformed");
31 // No acknowledgment thrice
32 sequence no_ack_thrice;
33 (!right_ack[+] ##1 timeout)[ * 3];
34 endsequence
35 // Despair - raise error flag
36 no_ack: assert property (packet_sent ##1 no_ack_thrice |->
37 always err) else $error("Err indication does not persist");
38 endchecker : spec

Fig. 1.6 System specification

detects a situation when signal timeout is activated three times while awaiting
acknowledgment. 5

We discuss sequences in Chap. 6 .

5 This specification does not provide details about how the timeout condition is formed. Of
course, a complete specification should provide them.