An Apology for Local Variables - SVA: The Power of Assertions in SystemVerilog - page 342

1 bit active[0:MAX_TAG];
2 initial
3 active <= '0;
4 always @( posedge clk)
5 if ($sampled(start))
6 active[$sampled(tagIn)] <= 1'b1;
7 else if ($sampled(complete))
8 active[$sampled(tagOut)] <= 1'b0;
9 a_no_tag_reuse: assert property (start |-> !active[tagIn]);
10 a_comp_tag_ok: assert property (complete |-> active[tagIn]);

Fig. 15.13 Encoding of tag protocol control check without associative arrays

recoded as a bounded array. For simplicity, suppose that the tag values range from
0 to MAX_TAG . Then the array of active bits can be encoded as shown in Fig. 15.13 .
There we use concurrent assertions to illustrate a coding style suitable for formal
verification. 3 The code of this figure, together with that of the data check using
local variables shown in Fig. 15.12 , gives a complete encoding of the tag protocol
checks suitable for formal tools.
If the number of tag values times the number of bits needed to store a data value
is also not too large, then a similar bounded array of elements of type dataType can
be used to store the data of the active transactions, replacing the associative array of
Fig. 15.11 .
In practice, it may be that the number of tag values or the product of the number
of tag values times the number of bits needed to store a data value will be too large
for static allocation and formal verification. If the number of active transactions can
be bounded by a number significantly smaller than the number of tags, then smaller
arrays that store the tag and data values for each active transaction can be encoded.
Such arrays are essentially RTL implementations of bounded associative arrays.
Suppose that the positive integer parameter MAX_ACTIVE is an upper bound for
the number of simultaneously active transactions. Figure 15.14 shows an encoding
of the tag protocol control checks assuming this bound. Line 1 defines indexType ,
which can store values from 0 through MAX_ACTIVE (cf. Exercise 15.3 ). An array
tags indexed from 0 to MAX_ACTIVE is used to store the tags of the active
transactions. Each element of the array has a validity bit ( valid ) and a tag data field
( activeTag ). If the validity bit is 1'b1 , then the tag data field stores the value of an
active tag. If the validity bit is 1'b0 , then the tag data field is not meaningful and that
position in the array is considered free. The data for an element are organized in a
structure (Line 2 ) with type name extendedTagType (Line 5 ). In Line 6 the array of
structures is declared with a declaration assignment initializing its elements to zero.
The expression '{ default : '{1'b0, '0}} is an assignment pattern that says that
each element in the array is initialized to value '{1'b0, '0} , which in turn specifies
that the valid member of the structure gets value 1'b0 and the activeTag member
of the structure gets value '0 . The assignment pattern accomplishes initialization