// ************************************************************************** //
//                                                                            //
//    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 constructive cyclic program is due to Riedel [Ried04]. The assertions //
// indicate an equivalent acyclic version.                                    //
// ************************************************************************** //


module Riedel1(event ?x1,?x2,?x3,y1,y2,y3) {
    event w1,w2,w3,w4,w5,w6;
    always{
        w1 = x1 & y1;
        w2 = !x1 & y2;
        w3 = x2 & w5;
        w4 = !x2 & w6;
        w5 = x1 | y3;
        w6 = !x1 | y3;
        y1 = x3 | w3;
        y2 = !x3 | w4;
        y3 = !(w1 | !w2);
        assert(y1 == (x2 | x3));
        assert(y2 == (!x3 | !x1 & !x2));
        assert(y3 == (!x1 & !(x2&x3)));
    }
}
drivenby {
    bv{3} w;
    for(i=0..7) {
        pause;
        w = nat2bv(i,3);
        x1 = w{0};
        x2 = w{1};
        x3 = w{2};
    }
}