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

1 dataType data[tagType];
2 always @( posedge clk)
3

if ($sampled(start)) begin

a_no_tag_reuse: assert final (

4

!data.exists($sampled(tagIn))

5

);

6

data[$sampled(tagIn)] <= $sampled(dataIn);

7

end

8

else if ($sampled(complete)) begin

9

a_comp_tag_ok: assert final (data.exists($sampled(tagOut))
);

10

a_data_check: assert final (

11

$sampled(dataOut) == data[$sampled(tagOut)]

12

);

13

data.delete($sampled(tagOut));

14

end

15

Fig. 15.11 Encoding of tag protocol control and data check

1 property p_tag_data_check;
2 tagType tag;
3 dataType data;
4 (start, tag = tagIn, data = dataIn)
5 ##1 (complete && tagOut == tag)[->1]
6 |-> dataOut == data;
7 endproperty
8 a_tag_data_check: assert property (p_tag_data_check);

Fig. 15.12 Encoding of tag protocol data check using local variables

Without using local variables, a similar associative array can be used to store
the data values for the active tags. This array keeps track of which tags are active
and their associated data, so the active array is no longer needed in this approach.
Another final assertion can perform the data check specified in Rule 7 . Such an
encoding is shown in Fig. 15.11 .
The data check can be encoded using local variables in a style similar to that
of the FIFO data check with local variables, as shown in Fig. 15.12 .At start ,the
property captures the values of both tagIn and dataIn in the local variables tag
and data . The property then advances to the nearest occurrence of complete at
which tagOut equals the value stored in tag , and at that point compares dataOut
to the value stored in data . This encoding still relies on the final assertions in
Fig. 15.10 to perform the control checks.
Associative arrays are convenient for encoding the checks of the tag protocol, but
because of their dynamic and unbounded nature, they will typically not be supported
in formal verification tools. To provide an encoding for formal verification, the
auxiliary variables should be declared in a way that is explicitly bounded. If the
number of tag values is not too large, then the active associative array can be