Hardware Reference
In-Depth Information
15.2. Suppose that the sequential protocol is relaxed to allow an occurrence of
complete to be concurrent with the corresponding occurrence of start .Ifthis
happens, then start may occur again in the subsequent cycle.
1. Modify the precise English description of the protocol to account for this
relaxation.
2. Modify the encodings given in Figs. 15.3 , 15.4 , and 15.5 to align them with this
relaxation.
15.3. Show that for any positive value of MAX_OUTSTANDING that does not overflow
$clog2 , the declaration of outstanding in Fig. 15.6 has enough bits to store
the number MAX_OUTSTANDING . Show that if MAX_OUTSTANDING is not a power
of two, then this declaration has more than enough bits to store the number
MAX_OUTSTANDING . Find a declaration that always allocates the minimum number
of bits required to store the number MAX_OUTSTANDING .
15.4. Will the behavior of p_fifo_data_check in Fig. 15.9 change if the ##1 in
Line 5 is changed to ##0 ? If so, does the new behavior correctly advance to the cycle
at which the data comparison of Line 8 needs to be performed? What happens if the
##1 in Line 6 is changed to ##0 ?
15.5. The encoding of p_fifo_data_check in Fig. 15.9 uses the decrementing
local variable counter numAhead . Give an alternative encoding that uses an incre-
menting local variable counter. [Hint: Use three local variables, one to capture
dataIn , another to capture outstanding , and the other to serve as the incrementing
counter.]
15.6. Assume that storage for the queue declared in Line 1 of Fig. 15.8 is
allocated at compile time. (This is likely an accurate assumption for a formal
verification tool, although it might not be accurate for a simulation tool.) Compare
the storage requirements for the encodings of a_fifo_data_check with local
variables (Fig. 15.9 ) and without local variables (Fig. 15.8 ). Consider the storage
requirements for the local variables if outstanding remains small compared to
MAX_OUTSTANDING and if outstanding becomes close to MAX_OUTSTANDING .
15.7. What will happen if the assertion a_fifo_all_checks of Fig. 15.15 is
written as a module item instead of within an initial procedure?
15.8. Show how to recode p_fifo_all_checks from Fig. 15.15 to eliminate the
local variable outstanding .
15.9. Suppose that the product of the number of tag values times the number of bits
needed to store a data value in the tag protocol is too large to allocate storage for the
data associated with every tag. Enhance the encoding shown in Fig. 15.14 to store
also the data for each active transaction. Show how to encode the tag protocol data
check without using local variables.
15.10. Write a property using only local variables that checks that once complete
occurs for a given tag, another complete may not occur for that tag until after start
occurs for that tag.
Search WWH ::




Custom Search