```package FloatingPoint;

// ************************************************************************** //
//                                                                            //
//    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.
// ************************************************************************** //

macro BITWIDTH = 8;

// int-version of square root computation.
// a     = input number
// r     = result
// exact = true when r*r=a, false if r*r< a < (r+1)*(r+1)
// ready = result was computed, r and exact contain the result
module IntSquareRoot(bv{BITWIDTH} ?a, bv{BITWIDTH} r, bool !exact, event !ready) {
bv{BITWIDTH} ns;         // =n^2
bv{BITWIDTH} n2i;        // =2^{2i}: used for iterative approximation of n.
bv{BITWIDTH} ni;         // =2^i: used for iterative approximation of n.
bv{BITWIDTH} remainingA; // aCopy - n^2

r = {false::BITWIDTH};
ns = {false::BITWIDTH};
remainingA = a;
if(a=={false::BITWIDTH}) {
ni = {false::BITWIDTH};
} else {
ni = {false::(BITWIDTH/2)}@true@{false::(BITWIDTH/2-1)};
}
n2i = false@true@{false::(BITWIDTH-2)};

while ((ni != {false::BITWIDTH}) & (remainingA != {false::BITWIDTH})) {
if(bv2nat(n2i) + bv2nat(ns) <= bv2nat(remainingA)) {
next(remainingA) = nat2bv(bv2nat(remainingA) - bv2nat(n2i) - bv2nat(ns), BITWIDTH);
next(r) = nat2bv(bv2nat(r) + bv2nat(ni), BITWIDTH);
next(ns) = nat2bv(bv2nat(false@ns{-1:1}) + bv2nat(n2i), BITWIDTH);
} else {
next(ns) = false@ns{-1:1};  // ns/2
}
next(n2i) = {false::2}@(n2i{-1:2}); // n2i/4
next(ni) = false@(ni{-1:1}); // ni/2
pause;
}

// If remainingA!=0 => the result is not exact, r=floor(sqrt(a))<sqrt(a)
exact = (remainingA=={false::BITWIDTH});
}
satisfies {
// Verification with model checker is not testet, yet!
x : assert(
A (
( bv2nat(r)*bv2nat(r) <= bv2nat(a) &
bv2nat(a) < (bv2nat(r)+1)*(bv2nat(r)+1)
)
)
);
}
drivenby { // 0
a = nat2bv(0, BITWIDTH);
assert( bv2nat(r)*bv2nat(r) <= bv2nat(a) & bv2nat(a) < (bv2nat(r)+1)*(bv2nat(r)+1) );
assert( exact -> ( bv2nat(r)*bv2nat(r) == bv2nat(a) ) );
assert( !exact -> ( bv2nat(r)*bv2nat(r) < bv2nat(a) ) );
}
drivenby { // 1
a = nat2bv(1, BITWIDTH);
assert( bv2nat(r)*bv2nat(r) <= bv2nat(a) & bv2nat(a) < (bv2nat(r)+1)*(bv2nat(r)+1) );
assert( exact -> ( bv2nat(r)*bv2nat(r) == bv2nat(a) ) );
assert( !exact -> ( bv2nat(r)*bv2nat(r) < bv2nat(a) ) );
}
drivenby { // 2
a = nat2bv(2, BITWIDTH);
assert( bv2nat(r)*bv2nat(r) <= bv2nat(a) & bv2nat(a) < (bv2nat(r)+1)*(bv2nat(r)+1) );
assert( exact -> ( bv2nat(r)*bv2nat(r) == bv2nat(a) ) );
assert( !exact -> ( bv2nat(r)*bv2nat(r) < bv2nat(a) ) );
}
drivenby { // 3
a = nat2bv(3, BITWIDTH);
assert( bv2nat(r)*bv2nat(r) <= bv2nat(a) & bv2nat(a) < (bv2nat(r)+1)*(bv2nat(r)+1) );
assert( exact -> ( bv2nat(r)*bv2nat(r) == bv2nat(a) ) );
assert( !exact -> ( bv2nat(r)*bv2nat(r) < bv2nat(a) ) );
}
drivenby { // 4
a = nat2bv(4, BITWIDTH);
assert( bv2nat(r)*bv2nat(r) <= bv2nat(a) & bv2nat(a) < (bv2nat(r)+1)*(bv2nat(r)+1) );
assert( exact -> ( bv2nat(r)*bv2nat(r) == bv2nat(a) ) );
assert( !exact -> ( bv2nat(r)*bv2nat(r) < bv2nat(a) ) );
}
drivenby { // 5
a = nat2bv(7, BITWIDTH);
assert( bv2nat(r)*bv2nat(r) <= bv2nat(a) & bv2nat(a) < (bv2nat(r)+1)*(bv2nat(r)+1) );
assert( exact -> ( bv2nat(r)*bv2nat(r) == bv2nat(a) ) );
assert( !exact -> ( bv2nat(r)*bv2nat(r) < bv2nat(a) ) );
}
drivenby { // 6
a = nat2bv(13, BITWIDTH);
assert( bv2nat(r)*bv2nat(r) <= bv2nat(a) & bv2nat(a) < (bv2nat(r)+1)*(bv2nat(r)+1) );
assert( exact -> ( bv2nat(r)*bv2nat(r) == bv2nat(a) ) );
assert( !exact -> ( bv2nat(r)*bv2nat(r) < bv2nat(a) ) );
}
drivenby { // 7
a = nat2bv(23, BITWIDTH);
assert( bv2nat(r)*bv2nat(r) <= bv2nat(a) & bv2nat(a) < (bv2nat(r)+1)*(bv2nat(r)+1) );
assert( exact -> ( bv2nat(r)*bv2nat(r) == bv2nat(a) ) );
assert( !exact -> ( bv2nat(r)*bv2nat(r) < bv2nat(a) ) );
}
drivenby { // 8
a = nat2bv(67, BITWIDTH);
assert( bv2nat(r)*bv2nat(r) <= bv2nat(a) & bv2nat(a) < (bv2nat(r)+1)*(bv2nat(r)+1) );
assert( exact -> ( bv2nat(r)*bv2nat(r) == bv2nat(a) ) );
assert( !exact -> ( bv2nat(r)*bv2nat(r) < bv2nat(a) ) );
}
drivenby { // 9
a = nat2bv(99, BITWIDTH);
assert( bv2nat(r)*bv2nat(r) <= bv2nat(a) & bv2nat(a) < (bv2nat(r)+1)*(bv2nat(r)+1) );
assert( exact -> ( bv2nat(r)*bv2nat(r) == bv2nat(a) ) );
assert( !exact -> ( bv2nat(r)*bv2nat(r) < bv2nat(a) ) );
}
drivenby { // 10
a = nat2bv(100, BITWIDTH);
assert( bv2nat(r)*bv2nat(r) <= bv2nat(a) & bv2nat(a) < (bv2nat(r)+1)*(bv2nat(r)+1) );
assert( exact -> ( bv2nat(r)*bv2nat(r) == bv2nat(a) ) );
assert( !exact -> ( bv2nat(r)*bv2nat(r) < bv2nat(a) ) );
}
drivenby { // 11
a = nat2bv(101, BITWIDTH);
assert( bv2nat(r)*bv2nat(r) <= bv2nat(a) & bv2nat(a) < (bv2nat(r)+1)*(bv2nat(r)+1) );
assert( exact -> ( bv2nat(r)*bv2nat(r) == bv2nat(a) ) );
assert( !exact -> ( bv2nat(r)*bv2nat(r) < bv2nat(a) ) );
}
drivenby { // 12
a = nat2bv(255, BITWIDTH);