// ************************************************************************** //
//                                                                            //
//    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                                             //
//                                                                            //
// ************************************************************************** //
// The following Quartz module is due to Malik (1994) and demonstrates that   //
// cyclic dependencies can arise due to operand sharing as used in high-level //
// synthesis. The module below makes use of only one occurrence of f and g,   //
// respectively, to compute y = g(f(x)) for c=false and f(g(x)) for c=true.   //
// Due to the dynamic dependencies on c, the following schedules have to be   //
// chosen at runtime to compute a reaction step:                              //
//                                                                            //
//    c==false:               c==true:                                        //
//          xf = x;                 xg = x;                                   //
//          yf = f(xf);             yg = g(xg);                               //
//          xg = yf;                xf = yg;                                  //
//          yg = g(xg);             yf = f(xf);                               //
//          y  = yg;                y  = yf;                                  //
//                                                                            //
// There is a cyclic dependency xf --> yf --> xg --> yg --> xf that is however//
// broken by c=false (yf --> xg but not yg --> xf) or c=true (yg --> xf but   //
// not yf --> xg). An acyclic version must make use of two occurrences of f   //
// and g which is e.g. y = (c ? f(g(x)) : g(f(x))).                           //
// ************************************************************************** //

macro f(x) = 2*x;       // functions f and g are chosen arbitrarily
macro g(x) = 3+x;


module Malik(nat ?x,bool ?c, nat !y) {
    nat xf,xg,yf,yg;

    loop {
        pause;
        xf = (c ? yg : x);
        xg = (c ? x : yf);
        yf = f(xf);
        yg = g(xg);
        y  = (c ? yf : yg);
    }
}
drivenby {
    pause;
    c = false;
    x = 10;
    pause;
    c = true;
    x = 10;
}