```// ************************************************************************** //
//                                                                            //
//    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 SquareRoot1(nat{N} ?a,r,event !rdy) {
nat{N*2} s;
r = 0;            // preliminary root
s = 1;
while(s <= a) {
// invariant: s = sum(int i=1..r+1} 2i+1
next(r) = r + 1;
next(s) = s + 2*r + 3;
pause;
}
emit(rdy);
assert(r*r <= a & a < (r+1)*(r+1));
}
drivenby {
a = 900;
await(rdy);
}
drivenby {
a = 4568;
await(rdy);
}
```