// ************************************************************************** //
//                                                                            //
//    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                                             //
//                                                                            //
// ************************************************************************** //
// This Quartz file implements a Banyan network based on the perfect shuffle  //
// permutation. Banyan networks for N=exp(2,K) inputs consist of log(N)=K     //
// columns that consist of N/2 switches. The columns are organized as a binary//
// tree, i.e., the columns enumerated with 0,…,K-1 from left to right consist //
// of blocks where column i has exp(2,K-1-i) blocks of size exp(2,i+1).       //
// The N inputs are triples (x,r,t) consisting of the message x (here a nat   //
// value), a request r, and the target address t that has to be connected with//
// the corresponding input.                                                   //
// The Banyan network can implement 2^{Nlog(N)/2)} = N^{N/2} different        //
// permutations which is a number less than N!. Hence, not every connection of//
// the N input to the N outputs can be established. The module below reports  //
// on output "conflict" if the desired connections are in conflict. Otherwise,//
// for all i y[target(x[i])] equals to data(x[i]) as given in the assertion.  // 
// ************************************************************************** //

macro K = 4;                    // log(N), i.e., the number of columns
macro N = exp(2,K);             // number of inputs, i.e. twice the number of rows
macro rotl(x) = x{0}@x{-1:1};   // inverse perfect shuffle
macro route(from,to) = reverse(nat2bv(from,K)) xor nat2bv(to,K);

macro data(x) = x.0;
macro target(x) = x.1;
macro req(x) = x.2;


module BanyanPerfectShuffle([N](nat * nat{N} * bool) ?x,[N]nat y,event conflict) {
    [N][K+1]nat   z;    // data to be transmitted
    [N][K+1]bv{K} r;    // desired routing information
    [N][K+1]bool  s;    // whether the line requests a connection

    // copy inputs to the leftmost column of the network
    // routing configuration is obtained by bitwise xor of reverse target and
    // the original source indices given as binary numbers
    for(i=0..N-1) {
        z[i][0] = data(x[i]);
        r[i][0] = route(i,target(x[i]));
        s[i][0] = req(x[i]);
    }

    // routing through the network
    for(col=0..K-1) {                       // for all columns    
        for(b=0..exp(2,K-1-col)-1) {        // number of blocks in column col
            for(i=0..exp(2,col)-1)          // for all switches in block b of col
                let(bsize = exp(2,col+1))   // size of a block
                let(boff  = b*bsize)        // offset of the block
                // determine outputs of switch i in block b of column col
                let(i0 = 2*i)           // block index of input 0
                let(i1 = 2*i+1)         // block index of input 1
                let(s0 = (col==0 ? i0 : bv2nat(rotl(nat2bv(i0,col+1))))) // source of i0
                let(s1 = (col==0 ? i1 : bv2nat(rotl(nat2bv(i1,col+1))))) // source of i1
                let(j0 = boff + s0)     // absolute source index of i0
                let(j1 = boff + s1)     // absolute source index of i1
                let(cross0 = r[j0][col]{K-1-col})
                let(cross1 = r[j1][col]{K-1-col}) {
                // report a potential conflict
                if(s[j0][col] & s[j1][col] & cross0 != cross1)
                    emit(conflict);
                // connections
                z[boff+i0][col+1] = (cross0 ? z[j1][col] : z[j0][col] );
                z[boff+i1][col+1] = (cross0 ? z[j0][col] : z[j1][col] );
                r[boff+i0][col+1] = (cross0 ? r[j1][col] : r[j0][col] );
                r[boff+i1][col+1] = (cross0 ? r[j0][col] : r[j1][col] );
                s[boff+i0][col+1] = (cross0 ? s[j1][col] : s[j0][col] );
                s[boff+i1][col+1] = (cross0 ? s[j0][col] : s[j1][col] );
            }
        }
    }

    // receiving the final outputs
    for(i=0..N-1){
        y[i] = z[i][K];
        assert(!conflict -> y[target(x[i])] == data(x[i]));
    }

}
drivenby allstraight {
    for(i=0..N-1) {
        target(x[i]) = bv2nat(reverse(nat2bv(i,K)));
        data(x[i]) = i;
        req(x[i]) = true;
    }
}
drivenby allcrossed {
    for(i=0..N-1) {
        target(x[i]) = bv2nat(not(reverse(nat2bv(i,K))));
        data(x[i]) = i;
        req(x[i]) = true;

    }
}