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