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

Line 6 does two jobs. The first is to prevent the repetition of Line 5 from stopping
early. This is done by enforcing the Boolean condition numAhead == 0 .Ifthe
evaluation tries to proceed from Line 5 to Line 6 when numAhead > 0 , then the
Boolean numAhead == 0 will be false and the evaluation must revert to Line 5 to
attempt another repetition of the skipping sequence. The second job of Line 6 is
to advance to the next occurrence of complete by matching complete[->1] .This
occurrence is the one that corresponds to the occurrence of start in Line 4 and at
which the data check should be performed.
As an intuitive summary, the matching of Lines 5 and 6 accomplishes the
following:

￿ While numAhead is positive, advance to the next occurrence of complete and
decrement numAhead .
￿ When numAhead becomes zero, advance to the next occurrence of complete and
stop.

Managing a local variable counter such as numAhead within a repetition as shown
in this example may seem daunting at first. After fully understanding a few such
patterns, the reader will acquire the skill and confidence to put them into practice.
Exercise 15.6 explores the storage requirements of the encodings of the FIFO
protocol data check with and without local variables.

15.4 Tag Protocol

In this section, we switch from an in-order protocol to an out-of-order protocol in
which two occurrences of complete do not have to be in the same order as the
corresponding occurrences start . Additional data are needed to determine which
occurrence of complete corresponds to a given occurrence of start . This protocol
uses a tag to do the matching. The signal tagIn is valid with an occurrence of start
and determines the tag of the transaction. The tag is active for that transaction while
the transaction is outstanding. The signal tagOut is valid with an occurrence of
complete , and matching of the values of tagIn and tagOut is used to define the
correspondence. While a tag is active for a transaction, it must not be reused by
another transaction. Here are the English rules:

1. start and complete are signals of type logic . dataIn and dataOut are signals
of type dataType . tagIn and tagOut are signals of type tagType .
2. Whenever start is high, dataIn and tagIn are valid. Whenever complete is
high, dataOut and tagOut are valid.
3. In each cycle, each tag value is either active or inactive, according to the
following rules:

￿ Every tag value begins inactive.
￿ If there is no occurrence of start or complete in a cycle, then no tag value
changes state in the next cycle.