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});
    emit(ready);
}
satisfies {
    // Verification with model checker is not testet, yet!
    x : assert(
    A (
        ready ->
            ( bv2nat(r)*bv2nat(r) <= bv2nat(a) &
              bv2nat(a) < (bv2nat(r)+1)*(bv2nat(r)+1)
            )
        )
    );
}
drivenby { // 0
    a = nat2bv(0, BITWIDTH);
    immediate await(ready);
    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);
    immediate await(ready);
    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);
    immediate await(ready);
    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);
    immediate await(ready);
    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);
    immediate await(ready);
    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);
    immediate await(ready);
    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);
    immediate await(ready);
    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);
    immediate await(ready);
    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);
    immediate await(ready);
    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);
    immediate await(ready);
    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);
    immediate await(ready);
    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);
    immediate await(ready);
    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);
    immediate await(ready);
    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 { // 13
    a = nat2bv(144, BITWIDTH);
    immediate await(ready);
    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) ) );
}