// ************************************************************************** //
//                                                                            //
//    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                                             //
//                                                                            //
// ************************************************************************** //
// The following module implements the basic digit recurrence algorithm for   //
// division of integers: Given integers x and y, the algorithm computes the   //
// quotient digits of the quotient x/y to radix B as well as the remainder r. //
// Note that the given numbers x and y might not be given as B-complement     //
// numbers, but the algorithm needs to know the number M of digits that x has //
// in B-complement format. The algorithm then computes a sequence of numbers  //
// z(m),...,z(0):                                                             //
//  (1) z(m) = x + q[M] * y[N-1..0] * B^M                                     //
//  (2) z(i-1) = z(i) - q[i-1] * y[N-1..0] * B^(i-1) where q[i-1] is the      //
//      maximal digit ∈ {0,...,B−1} with q[i−1]*y[N-1..0]*B^(i-1) ≤ z         //
// It can be easily proved that the following invariants are then true:       //
//  (1) x = z(i) + q[M−1,...,i]*y*B^i                                         //
//  (2) 0 <= z(i) < |y|*B^i                                                   //
// Hence, for i=0, it follows that z(0) < y and x = q*y+z(0), so that the     //
// final z(0) is the remainder and the q[i] are the digits of the quotient of //
// the division of x by y.                                                    //
//   The numbers z(i) are stored in the same variable z that is overwritten   //
// with these numbers step by step. The quotient digit q[i-1] is determined   //
// naively by simply calculating z(i) - q[i-1] * y[N-1..0] * B^(i-1) for each //
// digit q[i-1] starting from B-1 until the result is non-negative.           //
// ************************************************************************** //

macro B = 10;
macro M = 5;

module IntDivAlgo(int ?x,?y,q,r,event !rdy) {
    nat z,i;
    int qy,qi,sgn_y;
    event isNegative;   // is set when z < qi * sgn_y * y * exp(B,i)

    assume(-(B/2)*exp(B,M-1) <=x & x<(B/2)*exp(B,M-1));
    sgn_y = (y<0 ? -1 : +1); 
    qi = (x>=0 ? 0 : -1);
    q  = qi * exp(B,M);
    z  = x - qi * sgn_y * y * exp(B,M);
    i = M;
    do {
        // try digits qi = B-1,…,0 until z >= qi * sgn_y * y * exp(B,i)
        next(qi) = B-1;
        next(i) = i-1;
        do {
            w0: pause;
            qy = qi * sgn_y * y * exp(B,i);
            isNegative = z<qy;
            if(isNegative) 
                next(qi) = qi - 1;
        } while(isNegative);
        // here qi is the maximal digit with z >= qy = qi * sgn_y * y * exp(B,i)
        next(z) = z - qy;
        next(q) = q + qi * exp(B,i);
        w1: pause;
        assert(z == x - q * sgn_y * y);
        assert(0<= z & z<abs(y) * exp(B,i));
    } while(i>0);
    // determine quotient and remainder
    next(q) = (y<0 ? -q : q);
    next(r) = z;
    pause;
    emit(rdy);
    assert(x == q * y + r);
    assert(0<= r & r < abs(y));
}
drivenby Test01 {
    x = +34322;
    y = +27;
    await(rdy);
}
drivenby Test02 {
    x = +34322;
    y = -27;
    await(rdy);
}
drivenby Test03 {
    x = -34322;
    y = +27;
    await(rdy);
}
drivenby Test04 {
    x = -34322;
    y = -27;
    await(rdy);
}