// ************************************************************************** //
//                                                                            //
//    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;
}