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

The system consists of a transmitter and a receiver connected by a point-to-point duplex
channel. The transmitter sends to the receiver packets and gets an acknowledgment from
the receiver upon the packet receipt. The packet contains a header and a body. The header
consists of 8 bits, and the two most significant bits contain information about the transaction
type: data (10), control (01), or void (00). The remaining 6 bits of the header contain the
transaction tag in case of a data transaction, and are 0 in case of a control transaction. For
void packets the tag field may contain any value. The packet body consists of three bytes;
these bytes contain raw data for data transactions and commands for control transactions
...
Upon receipt of a data or a control packet the receiver sends back to the transmitter an
acknowledgment signal. The acknowledgment consists of 7 bits: the most significant bit is
set to 1, and the remaining 6 bits contain the tag of the received packet. If a void packet is
received, its contents are ignored and no acknowledgment is sent . . .
The transmitter is not allowed to send a new packet before an acknowledgment is received.
If timeout is reached, the transmitter sends the same packet again. If after three retries it
does not get an acknowledgment, it asserts the error signal and requires a manual reset.
Specifications written in natural languages are ambiguous, and cannot be
processed by tools. If we rewrite the properties from this specification in SVA as
shown in Fig. 1.6 , tools are then able to verify model compliance to its specification.
We do not give the complete specification here (for example, we do not specify how
timeout is set, and how a packet is resent), but only a fragment to illustrate the
concept.
We briefly describe the SVA code in Fig. 1.6 , derived from the specification, to
get an intuitive idea of how assertions can be extracted from a specification and
used for ensuring model compliance. Lines 1 - 7 define new types. Line 1 defines an
enumeration type giving names to specific integral values. Types tag_t and data_t
define new names for logic arrays of corresponding bounds. Lines 6 and 7 assign
names to the combined pieces of data.
Lines 8 - 38 define the specification as a checker .A checker is a special
verification unit containing assertions and their related code. By default, assertions
tx_packet_legal , rx_packet_legal , and no_ack use the clock declared in
Line 17 . We discuss the default clocking statement in Sect. 12.2.2 . Similarly,
Line 18 describes a default reset for all concurrent assertions in this checker. When
rst is asserted, no concurrent assertion is checked. This is carried out to disable
assertion checking during the reset sequence. Handling clocks and resets is a very
important topic, but we postpone the discussion on the related SVA features until
Chaps. 12 and 13 .
Lines 20 , 22 , and 24 define aliases for different conditions used in the assertions.
Sequence no_ack_thrice defined in Lines 32 - 34 models the relation-
ship between right_ack and timeout from the specification: “The transmitter
is not allowed to send a new packet before an acknowledgment is received. If
timeout is reached, the transmitter sends the same packet again. If after three retries
it does not get an acknowledgment, it asserts the error signal and requires a manual
reset.” Thus, the whole sequence
(!right_ack[+] ##1 timeout)[ * 3]