Mechanics of Local Variables - SVA: The Power of Assertions in SystemVerilog - page 378

sequence s_cnt_occurrences( bit a, local output int num_a);

1

(1'b1, num_a = a)

2

##1 (a[->1], num_a++)[ * ]

3

##1 !a[ * ];

4

endsequence

5

property p_num_dataValid_check;

6

transType l_ttype;

7

int num_dataValid;

8

(start, l_ttype = ttype)

9

##1

10

(

11

s_cnt_occurrences(.a(dataValid), .num_a(num_dataValid))

12

intersect

13

complete[->1]

14

)

15

|->

16

num_dataValid_OK(l_ttype, num_dataValid);

17

endproperty

18

a_num_dataValid_check: assert property (p_num_dataValid_check);

19

Fig. 16.18 Checking the number of occurrences of dataValid using local variable output

If these conditions are satisfied, then at the endpoint of any match of the sequence
instance, the values of the argument local variables of direction output or inout are
cast-converted and assigned to the corresponding receiver local variables. If there
are multiple matches of the sequence instance, then each match results in an ensuing
thread of evaluation in the instantiation context with its own copies of the receiver
local variables, and for each such match the receiver local variables are assigned the
values of the corresponding argument local variables for that match. Rule 2 ensures
that the result of these assignments is independent of the order in which they are
performed. Rules 3 and 4 ensure that each receiver local variable is assigned upon
match of the instance of the sequence.
As an example, suppose that we need to count the number of occurrences of
dataValid that are strictly after start and not later than complete , perhaps so
that a validity check can be performed based on this number and the value of
ttype that appeared with start . The code in Fig. 16.18 shows how this can be
done using a sequence, s_cnt_occurrences , with an argument local variable of
direction output . 11 s_cnt_occurrences monitors the argument a of type bit
and accumulates the number of occurrences of a in the output argument local
variable num_a . The sequence begins in Line 2 by assigning the value of a to
num_a , which accounts for an occurrence of a in the first cycle of match of the
sequence. The sequence continues in Line 3 with repetition of going to the next
occurrence of a and incrementing num_a . This accounts for subsequent occurrences

by substituting actual arguments for formal arguments, as described in the rewriting algorithms of
Annex F.4 of the LRM [ 8 ].
11 For formal verification, the int type of num_a and num_dataValid should be replaced with
the type of smallest bitwidth needed for the counters.