Checkers - SVA: The Power of Assertions in SystemVerilog - page 180

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

complete |-> dataOut == last_dataIn);

Fig. 9.2 Encoding of sequential protocol data check

The fact that there can be no complete before the first occurrence of start
is captured by assertion a_initial_no_complete . Would there be no reset, this
assertion should have been placed within an initial procedure. However, if the
reset ever becomes active, it will kill the only attempt of the assertion, and the
assertion might be never checked. Also, it is natural to interpret the specification
in a way that the entire checking starts anew after each reset. Therefore in our
implementation we check that there may be no complete before start each time
the reset goes low. Unfortunately, our solution has two problems:
1. It does not cover the case when reset is initially inactive.
2. It does not take into account the fact that the disable condition is not sampled in
SVA.

Exercises 9.1 - 9.3 discuss the solution for these problems.
Now let us move to the data part of the specification. The value of dataIn at an
occurrence of start needs to be stored somewhere, since otherwise it is lost and
the comparison with dataOut cannot be made. Since the protocol is sequential, one
auxiliary storage variable can be used to hold the value of dataIn from the nearest
preceding occurrence of start . The bookkeeping of dataIn and dataOut is done
by auxiliary code. Such auxiliary code required for assertions is called assertion
modeling code. For now, we implement the assertion modeling code in a module.
Its implementation is shown in Fig. 9.2 (Lines 1 - 4 ). Line 1 contains declaration
of the auxiliary storage variable last_dataIn whose type should be the type of
dataIn .
Since this code is not part of the design RTL, we have no idea what changes first:
clk or start . To follow the concurrent assertion semantics we must capture the
sampled value of start . This is reflected by the explicit call to the sampled value
function $sampled in Line 3 . For the same reason we explicitly sample dataIn
when capturing its value in Line 4 . This situation is typical when the assertion
modeling is done in modules or interfaces. Assertion a_seq_data_check in Line 5
checks that at the occurrence of complete the value of dataOut coincides with the
captured valued of dataIn .
It remains to define the module declaration. There are two questions to be
addressed:

￿ What is the type of dataIn and dataOut ?
￿ How to define a clock?