// ************************************************************************** //
//                                                                            //
//    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 natural numbers: Given natural numbers 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 in     //
// radix-B format, but the algorithm needs to know the number M of digits that//
// x has in radix-B format. The algorithm then computes a sequence of numbers //
// z(m),...,z(0):                                                             //
//  (1) z(m) = x                                                              //
//  (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) z(i) < y*B^i                                                          //
// Hence, for i=0, it follows that z(0) < y and x = q*y+z(0), so the 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 = 4;
macro M = 6;

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

    z = x;
    i = M;
    do {
        // try digits qi = B-1,B-2,... until z >= qi * y * exp(B,i)
        next(qi) = B-1;
        next(i) = i-1;
        do {
            w0: pause;
            qy = qi * y * exp(B,i);
            isNegative = z<qy;
            if(isNegative) 
                next(qi) = qi - 1;
        } while(isNegative);
        // here qi is the maximal digit with z >= qi * y * exp(B,i)
        next(z) = z - qy;
        next(q) = q + qi * exp(B,i);
        w1: pause;
        assert(z == x - q * y);
        assert(z<y * exp(B,i));
    } while(i>0);
    // copy the remainder from z
    r = z;
    emit(rdy);
    assert(x == y * q + r);
    assert(r < y);
}
drivenby Test01 {
    x = 10231;
    y = 312;
    await(rdy);
}