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

1 a_no_start: assert property (
2

start |=> !start throughout complete[->1]

3 );
4 a_no_complete: assert property (
5

complete |=> !complete throughout start[->1]

6 );
7 initial
8

a_initial_no_complete: assert property (

!complete throughout start[->1]

9

);

10

Fig. 15.3 Encoding of control part of sequential protocol

3. If start is high, then the value of dataIn at that time must equal the value of
dataOut at the next strictly subsequent cycle in which complete is high.
4. If start is high, then start must be low in the next cycle and remain low until
after the next strictly subsequent cycle in which complete is high.
5. complete may not be high unless start was high in a preceding cycle and
complete was not high in any of the intervening cycles.
The last two English rules specify that the protocol is sequential. Let us say that
a Boolean occurs if it is high. Then these rules say that a second start cannot
occur until after the complete for the first start occurs, and an occurrence of
complete corresponds to the nearest preceding occurrence of start . A transaction
spans the set of cycles from an occurrence of start to its corresponding occurrence
of complete , and two transactions do not overlap.
Note that this specification decomposes into a control part, which ensures the
sequential pairing of occurrences of start and complete , and a data part, which
checks the data correspondence between dataIn and dataOut for each such pair.
The control part of the specification does not involve data or local variables and can
be encoded as shown in Fig. 15.3 .
Assertion a_no_start checks Rule 4 .Rule 5 is checked by a_no_complete
and a_initial_no_complete . The first two assertions are symmetric in start
and complete , while the last is not. Since the last assertion is within an initial
procedure, only one evaluation attempt of a_initial_no_complete is begun at
the first occurrence of the clocking event. That evaluation checks that there is no
occurrence of complete until after the first occurrence of start .
Now let us move to the data part of the specification and begin without using local
variables. Since the latency from an occurrence of start to the next subsequent
occurrence of complete is not fixed, $past will not work. The value of dataIn at an
occurrence of start needs to be stored somewhere, though, since otherwise it is lost
and the comparison with dataOut cannot be made. Since the protocol is sequential,