```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                                             //
//                                                                            //
// ************************************************************************** //
// This module implements square root computation of fixed-point numbers.     //
// Consider this module as a helper function to implement square root         //
// computation of floating point numbers that conform to the IEEE standard.   //
// ************************************************************************** //

// BITWIDTH and FIXWIDTH are adapted to the floating point format of FloatSquareRoot.
// BITWIDTH is fixed to two bit: mantissa has one number left of the comma and may
// be shifted left to correct odd exponents (see FloatSquareRoot for explaination).
// The FIXWIDTH is computed as follows: width of mantissa plus additional precision
// bits to allow correct rounding and left shifts to get a normalized numbers.

// Set to use for test cases:
//macro BITWIDTH         = 8;  // use 8 bit int width for test cases
//macro FIXWIDTH         = 6;  // use 6 bit precision for test cases

// Set to use for call from FloatSquareRoot
macro BITWIDTH         = 2;   // use 2 bit for usage of FixedSquareRoot in FloatSquareRoot
macro FIXWIDTH         = 5;   // use width of mantissa + 1 (+ 1 to compute the r bit to determine rounding direction)

macro OVERALLWIDTH     = BITWIDTH + FIXWIDTH;
macro OVERALLWIDTH_TMP = BITWIDTH + FIXWIDTH*2;

macro MULT_CORR = exp(2,FIXWIDTH);

// fixed-point version
// 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 FixedSquareRoot(bv{OVERALLWIDTH} ?a, bv{OVERALLWIDTH} r, bool !exact, event !ready) {
bv{OVERALLWIDTH_TMP} ns;         // =n^2
bv{OVERALLWIDTH_TMP} n2i;        // =2^{2i}: used for iterative approximation of n.
bv{OVERALLWIDTH_TMP} ni;         // =2^i: used for iterative approximation of n.
bv{OVERALLWIDTH_TMP} remainingA; // aCopy - n^2

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

while ((n2i != {false::OVERALLWIDTH_TMP}) & (remainingA != {false::OVERALLWIDTH_TMP})) {
if(bv2nat(n2i) + bv2nat(ns) <= bv2nat(remainingA)) {
next(remainingA) = nat2bv(bv2nat(remainingA) - bv2nat(n2i) - bv2nat(ns), OVERALLWIDTH_TMP);
next(r) = r | ni{-1:FIXWIDTH};
next(ns) = nat2bv(bv2nat(false@ns{-1:1}) + bv2nat(n2i), OVERALLWIDTH_TMP);
} 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::OVERALLWIDTH_TMP});

}
satisfies {
// Verification with model checker is not testet, yet!
x : assert(
A (
( bv2nat(r)*bv2nat(r) <= bv2nat(a)*MULT_CORR &
bv2nat(a)*MULT_CORR < (bv2nat(r)+1)*(bv2nat(r)+1)
)
)
);
}
// input: int numbers
drivenby { // 1
a = nat2bv(0, BITWIDTH)@{false::FIXWIDTH};
assert( bv2nat(r)*bv2nat(r) <= bv2nat(a)*MULT_CORR & bv2nat(a)*MULT_CORR < (bv2nat(r)+1)*(bv2nat(r)+1) );
assert( exact -> ( bv2nat(r)*bv2nat(r) == bv2nat(a)*MULT_CORR ) );
assert( !exact -> ( bv2nat(r)*bv2nat(r) < bv2nat(a)*MULT_CORR ) );
}
drivenby { // 2
a = nat2bv(1, BITWIDTH)@{false::FIXWIDTH};
assert( bv2nat(r)*bv2nat(r) <= bv2nat(a)*MULT_CORR & bv2nat(a)*MULT_CORR < (bv2nat(r)+1)*(bv2nat(r)+1) );
assert( exact -> ( bv2nat(r)*bv2nat(r) == bv2nat(a)*MULT_CORR ) );
assert( !exact -> ( bv2nat(r)*bv2nat(r) < bv2nat(a)*MULT_CORR ) );
}
drivenby { // 3
a = nat2bv(1, BITWIDTH)@{false::FIXWIDTH};
assert( bv2nat(r)*bv2nat(r) <= bv2nat(a)*MULT_CORR & bv2nat(a)*MULT_CORR < (bv2nat(r)+1)*(bv2nat(r)+1) );
assert( exact -> ( bv2nat(r)*bv2nat(r) == bv2nat(a)*MULT_CORR ) );
assert( !exact -> ( bv2nat(r)*bv2nat(r) < bv2nat(a)*MULT_CORR ) );
}
drivenby { // 4
a = nat2bv(3, BITWIDTH)@{false::FIXWIDTH};
assert( bv2nat(r)*bv2nat(r) <= bv2nat(a)*MULT_CORR & bv2nat(a)*MULT_CORR < (bv2nat(r)+1)*(bv2nat(r)+1) );
assert( exact -> ( bv2nat(r)*bv2nat(r) == bv2nat(a)*MULT_CORR ) );
assert( !exact -> ( bv2nat(r)*bv2nat(r) < bv2nat(a)*MULT_CORR ) );
}
drivenby { // 5
a = nat2bv(4, BITWIDTH)@{false::FIXWIDTH};
assert( bv2nat(r)*bv2nat(r) <= bv2nat(a)*MULT_CORR & bv2nat(a)*MULT_CORR < (bv2nat(r)+1)*(bv2nat(r)+1) );
assert( exact -> ( bv2nat(r)*bv2nat(r) == bv2nat(a)*MULT_CORR ) );
assert( !exact -> ( bv2nat(r)*bv2nat(r) < bv2nat(a)*MULT_CORR ) );
}
drivenby { // 6
a = nat2bv(7, BITWIDTH)@{false::FIXWIDTH};
assert( bv2nat(r)*bv2nat(r) <= bv2nat(a)*MULT_CORR & bv2nat(a)*MULT_CORR < (bv2nat(r)+1)*(bv2nat(r)+1) );
assert( exact -> ( bv2nat(r)*bv2nat(r) == bv2nat(a)*MULT_CORR ) );
assert( !exact -> ( bv2nat(r)*bv2nat(r) < bv2nat(a)*MULT_CORR ) );
}
drivenby { // 7
a = nat2bv(13, BITWIDTH)@{false::FIXWIDTH};
assert( bv2nat(r)*bv2nat(r) <= bv2nat(a)*MULT_CORR & bv2nat(a)*MULT_CORR < (bv2nat(r)+1)*(bv2nat(r)+1) );
assert( exact -> ( bv2nat(r)*bv2nat(r) == bv2nat(a)*MULT_CORR ) );
assert( !exact -> ( bv2nat(r)*bv2nat(r) < bv2nat(a)*MULT_CORR ) );
}
drivenby { // 8
a = nat2bv(23, BITWIDTH)@{false::FIXWIDTH};
assert( bv2nat(r)*bv2nat(r) <= bv2nat(a)*MULT_CORR & bv2nat(a)*MULT_CORR < (bv2nat(r)+1)*(bv2nat(r)+1) );
assert( exact -> ( bv2nat(r)*bv2nat(r) == bv2nat(a)*MULT_CORR ) );
assert( !exact -> ( bv2nat(r)*bv2nat(r) < bv2nat(a)*MULT_CORR ) );
}
drivenby { // 9
a = nat2bv(67, BITWIDTH)@{false::FIXWIDTH};
assert( bv2nat(r)*bv2nat(r) <= bv2nat(a)*MULT_CORR & bv2nat(a)*MULT_CORR < (bv2nat(r)+1)*(bv2nat(r)+1) );
assert( exact -> ( bv2nat(r)*bv2nat(r) == bv2nat(a)*MULT_CORR ) );
assert( !exact -> ( bv2nat(r)*bv2nat(r) < bv2nat(a)*MULT_CORR ) );
}
drivenby { // 10
a = nat2bv(99, BITWIDTH)@{false::FIXWIDTH};
assert( bv2nat(r)*bv2nat(r) <= bv2nat(a)*MULT_CORR & bv2nat(a)*MULT_CORR < (bv2nat(r)+1)*(bv2nat(r)+1) );
assert( exact -> ( bv2nat(r)*bv2nat(r) == bv2nat(a)*MULT_CORR ) );
assert( !exact -> ( bv2nat(r)*bv2nat(r) < bv2nat(a)*MULT_CORR ) );
}
drivenby { // 11
a = nat2bv(100, BITWIDTH)@{false::FIXWIDTH};
assert( bv2nat(r)*bv2nat(r) <= bv2nat(a)*MULT_CORR & bv2nat(a)*MULT_CORR < (bv2nat(r)+1)*(bv2nat(r)+1) );
assert( exact -> ( bv2nat(r)*bv2nat(r) == bv2nat(a)*MULT_CORR ) );
assert( !exact -> ( bv2nat(r)*bv2nat(r) < bv2nat(a)*MULT_CORR ) );
}
drivenby { // 12
a = nat2bv(101, BITWIDTH)@{false::FIXWIDTH};
assert( bv2nat(r)*bv2nat(r) <= bv2nat(a)*MULT_CORR & bv2nat(a)*MULT_CORR < (bv2nat(r)+1)*(bv2nat(r)+1) );
assert( exact -> ( bv2nat(r)*bv2nat(r) == bv2nat(a)*MULT_CORR ) );
assert( !exact -> ( bv2nat(r)*bv2nat(r) < bv2nat(a)*MULT_CORR ) );
}
drivenby { // 13
a = nat2bv(144, BITWIDTH)@{false::FIXWIDTH};
assert( bv2nat(r)*bv2nat(r) <= bv2nat(a)*MULT_CORR & bv2nat(a)*MULT_CORR < (bv2nat(r)+1)*(bv2nat(r)+1) );
assert( exact -> ( bv2nat(r)*bv2nat(r) == bv2nat(a)*MULT_CORR ) );
assert( !exact -> ( bv2nat(r)*bv2nat(r) < bv2nat(a)*MULT_CORR ) );
}
drivenby { // 14
a = nat2bv(255, BITWIDTH)@{false::FIXWIDTH};
assert( bv2nat(r)*bv2nat(r) <= bv2nat(a)*MULT_CORR & bv2nat(a)*MULT_CORR < (bv2nat(r)+1)*(bv2nat(r)+1) );
assert( exact -> ( bv2nat(r)*bv2nat(r) == bv2nat(a)*MULT_CORR ) );
assert( !exact -> ( bv2nat(r)*bv2nat(r) < bv2nat(a)*MULT_CORR ) );
}
// input: real numbers
drivenby { // 15
a = nat2bv(0, BITWIDTH)@{true::FIXWIDTH};
assert( bv2nat(r)*bv2nat(r) <= bv2nat(a)*MULT_CORR & bv2nat(a)*MULT_CORR < (bv2nat(r)+1)*(bv2nat(r)+1) );
assert( exact -> ( bv2nat(r)*bv2nat(r) == bv2nat(a)*MULT_CORR ) );
assert( !exact -> ( bv2nat(r)*bv2nat(r) < bv2nat(a)*MULT_CORR ) );
}
drivenby { // 16
a = nat2bv(0, BITWIDTH)@true@{false::(FIXWIDTH-1)};
assert( bv2nat(r)*bv2nat(r) <= bv2nat(a)*MULT_CORR & bv2nat(a)*MULT_CORR < (bv2nat(r)+1)*(bv2nat(r)+1) );
assert( exact -> ( bv2nat(r)*bv2nat(r) == bv2nat(a)*MULT_CORR ) );
assert( !exact -> ( bv2nat(r)*bv2nat(r) < bv2nat(a)*MULT_CORR ) );
}
drivenby { // 17
a = nat2bv(0, BITWIDTH)@false@true@{false::(FIXWIDTH-2)};
assert( bv2nat(r)*bv2nat(r) <= bv2nat(a)*MULT_CORR & bv2nat(a)*MULT_CORR < (bv2nat(r)+1)*(bv2nat(r)+1) );
assert( exact -> ( bv2nat(r)*bv2nat(r) == bv2nat(a)*MULT_CORR ) );
assert( !exact -> ( bv2nat(r)*bv2nat(r) < bv2nat(a)*MULT_CORR ) );
}
drivenby { // 18
a = nat2bv(1, BITWIDTH)@true@true@{false::(FIXWIDTH-2)}; // 1.75
assert( bv2nat(r)*bv2nat(r) <= bv2nat(a)*MULT_CORR & bv2nat(a)*MULT_CORR < (bv2nat(r)+1)*(bv2nat(r)+1) );
assert( exact -> ( bv2nat(r)*bv2nat(r) == bv2nat(a)*MULT_CORR ) );
assert( !exact -> ( bv2nat(r)*bv2nat(r) < bv2nat(a)*MULT_CORR ) );
}
drivenby { // 19
a = nat2bv(1, BITWIDTH)@false@false@true@{false::(FIXWIDTH-3)}; // 1.125
assert( bv2nat(r)*bv2nat(r) <= bv2nat(a)*MULT_CORR & bv2nat(a)*MULT_CORR < (bv2nat(r)+1)*(bv2nat(r)+1) );
assert( exact -> ( bv2nat(r)*bv2nat(r) == bv2nat(a)*MULT_CORR ) );
assert( !exact -> ( bv2nat(r)*bv2nat(r) < bv2nat(a)*MULT_CORR ) );
}
drivenby { // 20
a = nat2bv(1, BITWIDTH)@false@true@{false::(FIXWIDTH-2)}; // 1.25
assert( bv2nat(r)*bv2nat(r) <= bv2nat(a)*MULT_CORR & bv2nat(a)*MULT_CORR < (bv2nat(r)+1)*(bv2nat(r)+1) );
assert( exact -> ( bv2nat(r)*bv2nat(r) == bv2nat(a)*MULT_CORR ) );
assert( !exact -> ( bv2nat(r)*bv2nat(r) < bv2nat(a)*MULT_CORR ) );
}

drivenby { // 21
a = nat2bv(1, BITWIDTH)@{true::4}@{false::(FIXWIDTH-4)};
assert( bv2nat(r)*bv2nat(r) <= bv2nat(a)*MULT_CORR & bv2nat(a)*MULT_CORR < (bv2nat(r)+1)*(bv2nat(r)+1) );
assert( exact -> ( bv2nat(r)*bv2nat(r) == bv2nat(a)*MULT_CORR ) );
assert( !exact -> ( bv2nat(r)*bv2nat(r) < bv2nat(a)*MULT_CORR ) );
}
drivenby { // 22
a = nat2bv(3, BITWIDTH)@{true::3}@{false::(FIXWIDTH-3)};
assert( bv2nat(r)*bv2nat(r) <= bv2nat(a)*MULT_CORR & bv2nat(a)*MULT_CORR < (bv2nat(r)+1)*(bv2nat(r)+1) );
assert( exact -> ( bv2nat(r)*bv2nat(r) == bv2nat(a)*MULT_CORR ) );
assert( !exact -> ( bv2nat(r)*bv2nat(r) < bv2nat(a)*MULT_CORR ) );
}
```