// ************************************************************************** // // // // 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 cyclic program is due to Rivest [Rive77,Ried04]. The module has N // // inputs x[i], and 2*N outputs y[i], and requires 2*N operations to define // // these outputs. Rivest proves in [Rive77] that at least 3*N-2 operations are// // required for any acyclic implementation. The circuit is however only // // constructive for odd N. // // ************************************************************************** // macro N = 6; module Rivest(event [N]bool ?x, event [2*N]bool y) { loop{ y[0] = x[0] & y[2*N-1]; y[1] = x[1 % N] | y[0]; for(i=0..N-2) { y[2*i+2] = x[(2*i+2) % N] & y[2*i+1]; y[2*i+3] = x[(2*i+3) % N] | y[2*i+2]; } pause; } } drivenby { bv{N} w; for(i=0..exp(2,N)-1) { pause; w = nat2bv(i,N); for(j=0..N-1) x[j] = w{j}; } }