```// ************************************************************************** //
//                                                                            //
//    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 Omega-Permutation network [Lawr75] which is  //
// a typical dynamic interconnection network. 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 Omega 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 = 3;                    // log(N), i.e., the number of columns
macro N = exp(2,K);             // number of inputs = twice the number of rows
macro rotl(x) = x{0}@x{K-1:1};  // inverse of perfect shuffle
macro route(from,to) = nat2bv(from,K) xor nat2bv(to,K);

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

module OmegaNetwork([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  b;    // whether the line requests a connection

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

// routing through the network
for(col=0..K-1){
for(i=0..N/2-1)
// determine outputs of switch in column col in row i
let(i0 = 2*i)
let(i1 = 2*i+1)
let(j0 = bv2nat(rotl(nat2bv(i0,K))))
let(j1 = bv2nat(rotl(nat2bv(i1,K))))
let(cross0 = r[j0][col]{K-1-col})
let(cross1 = r[j1][col]{K-1-col}) {
// connections
z[i0][col+1] = (cross0 ? z[j1][col] : z[j0][col] );
z[i1][col+1] = (cross0 ? z[j0][col] : z[j1][col] );
r[i0][col+1] = (cross0 ? r[j1][col] : r[j0][col] );
r[i1][col+1] = (cross0 ? r[j0][col] : r[j1][col] );
b[i0][col+1] = (cross0 ? b[j1][col] : b[j0][col] );
b[i1][col+1] = (cross0 ? b[j0][col] : b[j1][col] );
// report a potential conflict
if(b[j0][col] & b[j1][col] & cross0 != cross1)
emit(conflict);
}
}

// 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]) = i;
data(x[i]) = i;
req(x[i]) = true;
}
}
drivenby allcrossed {
for(i=0..N-1) {
target(x[i]) = N-1-i;
data(x[i]) = i;
req(x[i]) = true;

}
}
drivenby oddeven {
for(i=0..N/2-1) {
target(x[2*i]) = 2*i+1;
data(x[2*i]) = 2*i;
req(x[2*i]) = true;
target(x[2*i+1]) = 2*i;
data(x[2*i+1]) = 2*i+1;
req(x[2*i+1]) = true;
}
}
drivenby confl {
target(x[4]) = 6;
data(x[4]) = 11;
req(x[4]) = true;
target(x[2]) = 7;
data(x[2]) = 10;
req(x[2]) = true;
}

```