// ************************************************************************** // // // // 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)). // // In contrast to SquareRoot1, we introduce a further local variable n that is// // invariantly n=2*r+1, so that we avoid the multiplication operation with r. // // This way, we only need additions to compute the square root. // // ************************************************************************** // macro N = 1000000; module SquareRoot2(nat{N} ?a,r,event !rdy) { nat{N*2} s; nat{N} n; r = 0; // preliminary root n = 1; // invariant: n = 2*r+1 s = 1; // invariant: s = sum(int i=1..r+1} 2i+1 while(s <= a) { next(r) = r + 1; next(n) = n + 2; next(s) = s + n + 2; pause; } emit(rdy); assert(r*r <= a & a < (r+1)*(r+1)); } drivenby { a = 900; await(rdy); } drivenby { a = 4568; await(rdy); }