// ************************************************************************** //
//                                                                            //
//    eses                   eses                                             //
//   eses                     eses                                            //
//  eses    eseses  esesese    eses   Embedded Systems Group                  //
//  ese    ese  ese ese         ese                                           //
//  ese    eseseses eseseses    ese   Department of Computer Science          //
//  eses   eses          ese   eses                                           //
//   eses   eseses  eseseses  eses    University of Kaiserslautern            //
//    eses                   eses                                             //
//                                                                            //
// ************************************************************************** //
// The module below implements a FIFO that is instructed to enqueue a data    //
// value over input "dataIn" or to dequeue the topmost data value via output  //
// "dataOut". These instructions are given by inputs "put" and "get". However,//
// no value can be dequeued from the empty FIFO, and no value can be enqueued //
// in the full FIFO. For these reasons, enqueue and dequeue operations may not//
// be successful. Whether an enqueue or dequeue operation was successful is   //
// signaled via the outputs "ackIn" and "ackOut" in the next cycle, and the   //
// dequeued element is available at this point of time from output "dataOut". //
// The FIFO is capable of handling enqueue and dequeue operations in parallel,//
// in particular, also in case it is full or empty.                           //
// ************************************************************************** //


macro size = 3;
macro bits = 4;

macro pre(x) = abs((+x-1) % size);  // unary + converts to type int; abs to nat
macro suc(x) = abs((+x+1) % size);  // unary + converts to type int; abs to nat
macro empty(isMty,hd,tl) = isMty & (tl == hd);
macro full(hd,tl)  = (suc(tl) == hd);


module FIFO(event ?put,?get,!ackIn,!ackOut,event bv{bits} ?dataIn,!dataOut) {
    [size]bv{bits} buffer;  // internal store of FIFO elements
    nat{size} hd;           // buffer[hd..pre(tl)] are the elements in the FIFO
    nat{size} tl;           // hd=tl means that the buffer is either full or empty
    bool isEmpty;           // whether FIFO is full or empty (if hd=tl holds)

    isEmpty = true;
    always{
        case
            (put &!get) do
                // enqueue dataIn -> buffer[tl]
                if(isEmpty) { 
                    // isEmpty implies hd==tl
                    next(buffer[tl]) = dataIn;
                    emit next(ackIn);
                    next(isEmpty) = false;
                } else if(suc(tl) != hd) {
                    // FIFO is neither empty nor full
                    next(buffer[suc(tl)]) = dataIn;
                    emit next(ackIn);
                    next(isEmpty) = false;
                    next(tl) = suc(tl);
                }
            (!put & get) do
                // dequeue buffer[hd] -> dataOut
                if(isEmpty)
                    // do nothing when FIFO is empty
                    nothing;
                else if(hd==tl) {
                    // FIFO contains one element, thus becomes empty
                    next(dataOut) = buffer[hd];
                    emit next(ackOut);
                    next(isEmpty) = true;
                } else if(hd!=tl) {
                    next(dataOut) = buffer[hd];
                    emit next(ackOut);
                    next(hd) = suc(hd);
                }
            (put & get) do
                // parallel enqueue and dequeue
                if(isEmpty) {
                    // empty FIFO
                    next(dataOut) = dataIn;
                    emit next(ackIn);
                    emit next(ackOut);
                } else if(hd==tl) {
                    // one-element FIFO
                    next(dataOut) = buffer[hd];
                    next(buffer[tl]) = dataIn;
                    emit next(ackIn);
                    emit next(ackOut);
                } else {
                    next(dataOut) = buffer[hd];
                    next(buffer[suc(tl)]) = dataIn;
                    emit next(ackIn);
                    emit next(ackOut);
                    next(hd) = suc(hd);
                    next(tl) = suc(tl);
                }
        default
            nothing;
    }
}
drivenby {
    pause;
    // try a get in empty state
    put = false;
    get = true;
    pause;
    // put and get in empty state
    dataIn = 0b1110;
    put = true;
    get = true;
    pause;
    // put in empty state
    dataIn = 0b1000;
    put = true;
    get = false;
    pause;
    // put and get in one-element state
    dataIn = 0b1001;
    put = true;
    get = true;
    pause;
    // get in one-element state
    put = false;
    get = true;
    pause;
    // put another element in yet again empty FIFO
    dataIn = 0b0001;
    put = true;
    get = false;
    pause;
    // put second element in FIFO
    dataIn = 0b0010;
    put = true;
    get = false;
    pause;
    // put third element in FIFO
    dataIn = 0b0011;
    put = true;
    get = false;
    pause;
    // try to put element in full FIFO
    dataIn = 0b0100;
    put = true;
    get = false;
    pause;
    // put and get from full FIFO
    dataIn = 0b0100;
    put = true;
    get = true;
    pause;
    // get from full FIFO
    put = false;
    get = true;
    pause;
    // put and get in intermediate stage
    dataIn = 0b1111;
    put = true;
    get = true;
    pause;
}