macro pre(x) = abs((+x-1) % size);
macro suc(x) = abs((+x+1) % size);
macro numBits = 4;
macro size = 4;


module FIFO(event ?put,!ackPut,
            event ?get,!ackGet,
            event bv{numBits} ?dataIn,
            event bv{numBits} !dataOut) {
  // local variables to implement the buffer
  [size]bv{numBits} buf;
  nat{size} hd;
  nat{size} tl;
  bool isEmpty;

  isEmpty = true;
  always{
    case
      (put & !get) do
        // enqueue dataIn -> buf[tl]
        if(isEmpty) { 
          // FIFO is empty
          next(buf[tl]) = dataIn;
          emit next(ackPut);
          next(isEmpty) = false;
        } else if(hd==tl) {
          // FIFO is full
          nothing;
        } else {
          // FIFO is neither empty nor full
          next(buf[tl]) = dataIn;
          emit next(ackPut);
          next(isEmpty) = false;
          next(tl) = suc(tl);
        }
      (!put & get) do
        // dequeue buf[hd] -> dataOut
        if(isEmpty) {
          // FIFO is empty
          nothing;
        } else if(hd==tl) {
          // FIFO is full
          next(dataOut) = buf[hd];
          emit next(ackGet);
          next(isEmpty) = true;
        } else {
          // FIFO is neither empty nor full
          next(dataOut) = buf[hd];
          emit next(ackGet);
          next(hd) = suc(hd);
        }
      (put & get) do
        // parallel enqueue and dequeue
        if(isEmpty) {
          // FIFO is empty
          next(dataOut) = dataIn;
          emit next(ackPut);
          emit next(ackGet);
        } else if(hd==tl) {
          // FIFO is full
          next(dataOut) = buf[hd];
          next(buf[tl]) = dataIn;
          emit next(ackPut);
          emit next(ackGet);
        } else {
          // FIFO is neither empty nor full
          next(dataOut) = buf[hd];
          next(buf[tl]) = dataIn;
          emit next(ackPut);
          emit next(ackGet);
          next(hd) = suc(hd);
          next(tl) = suc(tl);
        }
    default
      nothing;
  }
}