IBM®
Skip to main content
    Israel [change]    Terms of use
 
 
 
    Home    Products    Services & solutions    Support & downloads    My account    
IBM Research

RuleBase Parallel Edition

Formal Verification


Generalized Buffer (PSL/Sugar version)

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:
  1. 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)).
  2. When GenBuf can service the sender, it reads the data from the data bus and asserts BtoS_ACK(i).
  3. 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.
  4. 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:
  1. 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).
  2. In the cycle following the assertion of BtoR_REQ(j), the receiver asserts RtoB_ACK(j).
  3. 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).
  4. 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




 
 





    About IBMPrivacyContact