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