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

15.1 Fixed Latency Data Pipeline

To get started, suppose that there is a fixed latency data pipeline whose data checking
requirement is specified by the following English:

1. start is a signal of type logic . dataIn and dataOut are signals of type
dataType .
2. LATENCY is a positive integer parameter.
3. Whenever start is high, dataIn is valid.
4. The value of dataIn when start is high must equal the value of dataOut
LATENCY cycles later.
The specification can be encoded without using local variables as shown in
Fig. 15.1 .
By using $past(dataIn,LATENCY) , one should expect performance in simula-
tion and formal verification to be similar to that of encoding a cascade of LATENCY
delay variables of type dataType .If LATENCY equals three, then the cascade of delay
variables is

dataType dataIn_D1, dataIn_D2, dataIn_D3;
always @( posedge clk) begin
dataIn_D1 <= $sampled(dataIn);
dataIn_D2 <= dataIn_D1;
dataIn_D3 <= dataIn_D2;

end
and the reference to $past(dataIn,LATENCY) is like a reference to dataIn_D3
(see also the discussion of $past in Sect. 7.2.1.2 ).
Using a local variable, the pipeline data check can be encoded as shown in
Fig. 15.2 . The local variable data of type dataType is declared on Line 2 within

a_pipeline_data_check: assert property (
start
|->
##LATENCY dataOut == $past(dataIn, LATENCY)

);

Fig. 15.1 Encoding of pipeline data check without local variables

1 property p_pipeline_data_check;
2 dataType data;
3 (start, data = dataIn)
4 |->
5 ##LATENCY dataOut == data;
6 endproperty
7 a_pipeline_data_check: assert property (p_pipeline_data_check);

Fig. 15.2 Encoding of pipeline data check with a local variable