Checkers in Formal Verification - SVA: The Power of Assertions in SystemVerilog - page 519

23.2.3 Example: Building Abstract Models with Checkers

Checkers with free variables can be used to build nondeterministic models for FV.

Example 23.18. Consider a pipeline consisting of n stages. Each stage has its own
enabler signal en[i] , where i is the number of the stage. This signal en[i] is
asserted when the i -th stage is ready to process the new data. When the data is
ready at the pipeline input, the data_ready flag is asserted. We want to write a
checker verifying that the pipeline latency (the number of clock ticks required to
pass through the pipeline) does not exceed max_latency .
The RTL implementing this model may be very complex, but the exact data and
exact operations performed in the pipeline are not important for our purpose. We can
build an abstract model as a checker that will only take into account the progress of
the data in the pipeline. This checker is shown in Fig. 23.1 .
At the beginning of the checker, there are definitions of the checker variables
and several let -definitions provided for convenience. ub(x) (Line 7 ) defines an
upper bound of a vector that can store the value x . The lower bound of the vector
is understood to be 0 . For example, if x=5 then 3 bits are needed to store x .The
upper bound of this vector will be 2 assuming that its lower bound is 0 .
The variable stage (Line 14 ) contains the number of the active stage, the first
active stage having number 1 .The stage can also assume two dummy values:
stage 0 , meaning that the data has not been sent to the pipeline yet, and stage
nstages (Line 8 ), which exceeds the number of actual stages by one, signaling
that data has been fully processed by the pipeline.
The variable latency (Line 15 ) keeps the current latency of the data. It is
limited by max_latency + 1 ( big_latency ,Line 10 )—in our implementation, if
the latency reaches this value, it is not incremented anymore, as the exact value of
the latency is not important, only the fact that the latency has exceeded the maximum
allowed value.
The main point in this checker is to understand when the transaction starts.
There may be many simultaneous transactions in the system, different data may be
simultaneously processed by different stages of the pipeline, and therefore, checking
the condition data_ready alone is not sufficient for counting the stage and latency.
The checker needs to be able to track any of these transactions, but by taking
advantage of nondeterminism it does not have to allocate and manage resources
to track them all at once. It only needs resources to track one!
The key here is to introduce free variable start (Line 13 ) and to start counting
the first time that both start and data_ready are simultaneously true. The role of
start is to choose nondeterministically which among all the possible transactions
the checker will track. Since start is free to take any value in each clock tick, we
effectively consider all combinations of possible attempts, and among them also all
possible single attempts. For convenience, we introduce variable go (Line 18 )for
the simultaneous occurrence of data_ready and start .
For example, assume that data_ready is high at clock ticks 10 and 20. The
following scenarios are possible: