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

1 bit complete_justified;
2 always @( posedge clk)
3 complete_justified = 1'b0;
4 task t_justify_complete;
5 @( negedge clk)
6 complete_justified = 1'b1;
7 endtask : complete_justified
8 property p_start_and_data_checks;
9

tagType tag;

dataType data;

10

(start, tag = tagIn, data = dataIn)

11

|=>

12

(

13

!(start && tagIn == tag)

14

throughout

15

(complete && tagOut == tag)[->1]

16

17 )
18 ##0 (1'b1, t_justify_complete)
19 ##0 dataOut == data;
20 endproperty
21 a_start_and_data_checks: assert property (
22

p_start_and_data_checks

23 );
24 a_complete_check: assert property (
25

complete |=> complete_justified

26 );

Fig. 15.16 Encoding of all tag protocol checks using local variables and a single-bit static variable

￿ Once start occurs for a given tag, another start may not occur for that tag until
after complete occurs for that tag.
￿ Once complete occurs for a given tag, another complete may not occur for that
tag until after start occurs for that tag.
These statements can be encoded in a straightforward way using local variables:
the first is represented in Lines 11 through 17 of Fig. 15.16 ; for the second, see
Exercise 15.10 . The asymmetry is that initially there can be a start on any tag, but
there cannot be a complete on a tag until after an occurrence of start on that tag.
Accounting for the tags for which no start has occurred is the challenging part,
and doing so explicitly is essentially encoding a data structure to represent all the
tags in a particular state, similar to the data structures discussed in Sect. 15.4 .
The novelty of the present encoding is that it entirely avoids explicit
representation of such a data structure. Instead, it makes use of the fact that
there is one evaluation thread of property p_start_and_data_checks tracking
each active tag. When a complete occurs, we need to determine whether or
not there is such a thread tracking the tag value in tagOut . SystemVerilog
provides no way to query such information from a set of threads of evaluation.
Instead, p_start_and_data_checks is encoded so that the relevant thread,