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

1 dataType last_dataIn;
2 always @( posedge clk)
3 if ($sampled(start))
4 last_dataIn <= $sampled(dataIn);
5 a_seq_data_check: assert property (
6

start ##1 complete[->1]

|-> dataOut == last_dataIn

7

8 );

Fig. 15.4 Encoding of sequential protocol data check without local variables

1 property p_seq_data_check;
2 dataType data;
3 (start, data = dataIn) ##1 complete[->1]
4 |-> dataOut == data;
5 endproperty
6 a_seq_data_check: assert property (p_seq_data_check);

Fig. 15.5 Encoding of sequential protocol data check with a local variable

one auxiliary storage variable can be used to hold the value of dataIn from the
nearest preceding occurrence of start . Figure 15.4 shows such an encoding. 1
Using local variables, we can follow the same data capture idiom from the
pipeline data check. The encoding is shown in Fig. 15.5 . Note the similarity between
Lines 6 and 7 from Fig. 15.4 and Lines 3 and 4 from Fig. 15.5 . 2 The encoding with
local variables avoids the auxiliary modeling code to define how last_dataIn is
updated, and it makes clear the timing of the data capture because the local variable
assignment data = dataIn is attached to the Boolean start .

15.3 FIFO Protocol

Next, let us generalize the sequential protocol to a FIFO (i.e., in-order) protocol by
allowing multiple occurrences of start prior to the next occurrence of complete
and multiple occurrences of complete before the next occurrence of start .The
occurrences of start and complete pair up by order, so that for each n 1,the

1 The use of $sampled specifies that sampled values of start and dataIn are used in
the always procedure, maintaining consistency with the implicit use of sampled values in
a_seq_data_check . See the detailed discussion in Sect. 9.1.1 .
2 The antecedent written in Line 6 of Fig. 15.4 is more verbose than the one in Line 22 of Fig. 9.4 .
This has been done to help highlight the similarities of the code in Figs. 15.4 and 15.5 .