```// ************************************************************************** //
//                                                                            //
//    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 butterfly        //
// 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 btfly(x) = (sizeOf(x)<=2 ? reverse(x) : x{0}@x{-2:1}@x{-1});   // (inverse) butterfly
macro rotl(x) = x{-2:0}@x{-1};
macro rotr(x) = x{0}@x{-1:1};
macro route(from,to) = reverse(nat2bv(from,K) xor rotr(nat2bv(to,K)));

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

module BanyanButterfly([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(btfly(nat2bv(i0,col+1))))) // source of i0
let(s1 = (col<=0 ? i1 : bv2nat(btfly(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(rotl(nat2bv(i,K)));
data(x[i]) = i;
req(x[i]) = true;
}
}
drivenby allcrossed {
for(i=0..N-1) {
target(x[i]) = bv2nat(not(rotl(nat2bv(i,K))));
data(x[i]) = i;
req(x[i]) = true;

}
}

```