|
Specifications
Next, we introduce the design to be verified:
GenBuf is a design block that queues words (32 bits) of data sent by
four senders to two receivers. The queue is a depth 4 FIFO. The senders are
equivalent, as are the receivers. The interface for each sender
consists of a request input (denoted StoB_REQ(i) for the ith sender),
an acknowledge output (denoted BtoS_ACK(i)), and one point-to-point data bus (denoted DI(i*32..(i+1)*32-1)). (Note that each sender has its own bus, although we are defining a joint single dimension array).
The interface for each receiver consists of a request output (denoted
BtoR_REQ(i)), an acknowledge input (denoted RtoB_ACK(i)), and one
output data bus (denoted DO(0..31)), that is shared by both
receivers. The following is a block diagram of the design and its
interface. Dashed boxes represent the environment.
The interface between GenBuf and the senders is a 4-phase handshaking protocol described below:
-
When a sender, say sender i, has data to send, it initiates a transfer
by asserting StoB_REQ(i) (Server to Buffer REQuest).
One cycle later, the sender puts the data on its data bus
(i.e. DI(i*32..(i+1)*32-1)).
-
When GenBuf can service the sender, it reads the data from the data
bus and asserts BtoS_ACK(i).
-
In the cycle following the assertion of BtoS_ACK(i), the sender should
deassert the signal StoB_REQ(i). From this point onwards, the data on the data
bus is considered invalid.
-
The end of the transaction is marked by GenBuf deasserting
BtoS_ACK(i). A new transaction may begin a cycle after the deassertion
of BtoS_ACK(i). (Note: GenBuf may hold BtoS_ACK(i) asserted
for several cycles before eventually deasserting it.)
An example timeline of a GenBuf-to-sender handshake
The interface between GenBuf and the receivers is another 4-phase handshaking protocol described below:
-
When GenBuf has data to send, it chooses one of the receivers, (denoted the
jth receiver). GenBuf then initiates a transfer by asserting
BtoR_REQ(j).
-
In the cycle following the assertion of BtoR_REQ(j), the receiver asserts
RtoB_ACK(j).
-
In the cycle following the assertion of RtoB_ACK(j),
GenBuf puts the data on the data bus (i.e. DO(0..31)) and
deasserts BtoR_REQ(j). Note: The cycle in which the data on the
bus is valid is the same cycle when GenBuf deasserts BtoR_REQ(j).
-
To conclude the transaction, the receiver should deassert
RtoB_ACK(j) a cycle after the deassertion of BtoR_REQ(j).
GenBuf does not initiate another transaction until a
cycle after RtoB_ACK(j) is deasserted.
An example timeline of a GenBuf-to-receiver handshake
The following are guaranteed:
- GenBuf maintains FIFO order
- Senders are never starved
- Receivers are requested by a round-robin scheme
- GenBuf never requests both receivers at the same time
| |
|
