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

When a sequence s is implicitly promoted to a property by using it in
the statement cover property (s) , the interpretation is as cover property
( strong (s)) . It means that if the first match of the sequence is not reached
when the last clock tick occurs, that attempt is not counted as covered. Recall
that the statement assert property (s) interpretation is as assert property
( weak (s)) , meaning that if a match is not reached when clock ticks stop, the result
is a success of the assertion.
An interesting situation occurs if a cover property statement is placed in a
conditional branch of an always procedure, as shown in the following example.

Example 18.12. Cover in an always procedure

always @( posedge clk) begin
if (!en) ... some code...;
else begin
c: cover property (a ##1 b);
... some other code ...

end

t

end

The cover property is sampled using posedge clk , but an evaluation attempt
will only start when control reaches the location of c in the procedure. That
may or may not ever happen, hence the overall effect of the cover within the
procedural code is similar to having written a static cover containing the property
s_eventually ((en && a)##1 b) . The eventuality occurs when the procedure
does execute the corresponding branch.
The next and final section provides two more complex examples.

18.5 Examples

Example 18.13. Recall the specification from Chap. 1 ,Fig. 1.6 :
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 six 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.