// ************************************************************************** //
//                                                                            //
//    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 is an unrolling of Rivest with N=4 together with an acyclic version.  //
// Note, however, that the circuit does not work for even N, so that the one  //
// below lacks of causality.                                                  //
// ************************************************************************** //

module Rivest04(event [4]bool ?x, event [8]bool y) {
    loop{
        y[0] = x[0]&y[7];
        y[1] = x[1]|y[0];
        y[2] = x[2]&y[1];
        y[3] = x[3]|y[2];
        y[4] = x[0]&y[3];
        y[5] = x[1]|y[4];
        y[6] = x[2]&y[5];
        y[7] = x[3]|y[6];
        assert(y[0] == (x[0]&x[3] | x[0]&x[1]&x[2] | x[0]&x[2]&y[6]));
        assert(y[2] == (x[1]&x[2] | x[0]&x[2]&x[3] | x[0]&x[2]&y[6]));
        assert(y[4] == (x[0]&x[3] | x[0]&x[1]&x[2] | x[0]&x[2]&y[6]));
        assert(y[6] == (x[1]&x[2] | x[0]&x[2]&x[3] | x[0]&x[2]&y[6]));
        assert(y[1] == (x[1] | x[0]&x[3] | x[0]&x[2]&y[6]));
        assert(y[3] == (x[3] | x[1]&x[2] | x[0]&x[2]&y[6]));
        assert(y[5] == (x[1] | x[0]&x[3] | x[0]&x[2]&y[6]));
        assert(y[7] == (x[3] | x[1]&x[2] | x[0]&x[2]&y[6]));
        pause;
    }
}
drivenby {
    bv{4} w;
    for(i=0..15) {
        pause;
        w = nat2bv(i,4);
        for(j=0..3)
            x[j] = w{j};
    }
}