// ************************************************************************** //
//                                                                            //
//    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                                             //
//                                                                            //
// ************************************************************************** //
// Compute the integer square root. The idea behind the algorithm given below //
// is as follows: it can be easily proved that n^2 = sum(i=1..root(n)} 2i+1   //
// holds, i.e., that the square numbers are the sums of the first odd numbers //
// where root(n) summands have to be added. Hence, we simply compute the sum  //
// of the first odd numbers and stop as soon as this sum becomes larger than  //
// the given number. The computation time is therefore O(root(a)).            //
// ************************************************************************** //

macro N = 1000000;

module SquareRootCeil(nat{N} ?a,r,event !rdy) {
    nat{N*2} s;
    r = 0;
    s = 0;
    while(s < a) {
        next(r) = r + 1;
        next(s) = s + r + r + 1;
        pause;
    }
    emit(rdy);
    assert((r-1)*(r-1) < a & a <= r*r);
}
drivenby {
    a = 900;
    await(rdy);
}
drivenby {
    a = 4568;
    await(rdy);
}