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

1 typedef bit [0:$clog2(MAX_ACTIVE)] indexType;
2 typedef struct {
3 bit valid;
4 tagType activeTag;
5 } extendedTagType;
6 extendedTagType tags[0:MAX_ACTIVE] = '{ default : '{1'b0, '0}};
7
8 function automatic indexType freeIndex;
9 for (indexType i=0; i < MAX_ACTIVE; i++)
10 if (!tags.valid[i]) return i;
11 return MAX_ACTIVE; // no free index
12 endfunction : freeIndex
13
14 function automatic indexType tagIndex (tagType tag);
15 for (indexType i=0; i < MAX_ACTIVE; i++)
16 if (tags.valid[i] && tags.activeTag[i] == tag)
17 return i;
18 return MAX_ACTIVE; // tag not found
19 endfunction : tagIndex
20
21 always @( posedge clk)
22

if ($sampled(start))

tags[freeIndex] <= '{1'b1, $sampled(tagIn)};

23

else if ($sampled(complete))

24

tags.valid[tagIndex($sampled(tagOut))] <= 1'b0;

25

26
27 a_no_tag_reuse: assert property (
28

start

|-> tagIndex(tagIn) == MAX_ACTIVE // tagIn not found

29

30 );
31 a_comp_tag_ok: assert property (
32

complete

|-> tagIndex(tagOut) < MAX_ACTIVE // tagOut found

33

34 );

Fig. 15.14 Encoding of tag protocol control check with bound on number of active transactions

of the array without explicitly enumerating values or iterating over indices. 4 We
allocate MAX_ACTIVE+1 , and not just MAX_ACTIVE , array elements and reserve the
top element as a sink in case our assumed bound on the number of active transactions
is violated.
The auxiliary function freeIndex returns the smallest index that is not currently
storing a tag, if there is one. Otherwise, it returns MAX_ACTIVE . The auxiliary
function tagIndex returns the smallest index of the entry that is currently storing

4 The initialization could be skipped because the valid members are of data of type bit ,which
is initialized by default to 1'b0 . The explicit initialization clarifies the intention. The initial values
of the activeTag members are not important. Note also that only the first MAX_ACTIVE entries
of the array need be initialized.