// ************************************************************************** //
//                                                                            //
//    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 division algorithm is an improvement of NatDivModSeq0: It eliminates  //
// the local variable z which was used to store the numbers z(j) mentioned    //
// below. It has to be remarked that only N+1 digits of the numbers z(j) are  //
// relevant for the subtractions, where the rightmost one is always x[i].     //
// Thus, in the algorithm below, the leftmost N of these N+1 digits are       //
// stored in number r, while the rightmost one is directly taken from x[i]    //
// (see macro z). The complete number is z(i) = r[N-1..0]@x[i-1..0].          //
// The remaining ideas of the algorithm are the same as in NatDivModSeq0, i.e.//
// for the given radix-B numbers x and y having M and N digits, it 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(i).     //
// 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.                                                        //
//   As mentioned above, the numbers z(i) are stored in r[N-1..0]@x[i-1..0].  //
// 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.                                          //
//   For the definition of isNegative, note again that the leading digit of s //
// would be c[N+1] = (-c[N] + z(i+N)) / B, which is either -1 or 0. Thus, we  //
// have isNegative <-> c[N+1]==-1 <-> -c[N] + z(i+N) < 0 <-> z(i+N) < c[N].   //
// ************************************************************************** //

macro B = 4;    // base of the radix numbers
macro 
M = 4;          // number of digits used for x

macro N = 3;    // number of digits used for y

macro natval(x,m) = sum(i=0..m-1) (x[i] * exp(B,i));
macro z(i,j) = (j>0 ? r[j-1] : x[i]); // r[N-1..0]@x[i] replaces z[N+i..i]


module NatDivSeq1([M]nat{B} ?x,[N]nat{B} ?y,
                     [M]nat{B}  q,[N]nat{B}  r,event !rdy) {
    [N+1]nat{B} s,c;  // auxiliary variables
    event isNegative; // is set when subtraction yields negative result
    // -------------------------------------------------------------------------
    // prepare initial partial remainder z(m) = r[N-1..0]@x[m]
    // -------------------------------------------------------------------------

   for(i=0..N-1)
        r[i] = 0;

    //-------------------------------------------------------------------------
    // computing the quotient digits
    //-------------------------------------------------------------------------
    for(iup=0..M-1)
        let(i=M-1-iup) {// thus i=M-1..0
        // try q[i] = 0,1,... until we reach one where z(i)-q[i]*y[N-1..0]
        // becomes negative where z(i) = r[N-1..0]@x[i]
        next(q[i]) = B-1;
        do {
            w0: pause;
            //------------------------------------------------------------------
            // compute s[N..0] = r[N-1..0]@x[i] - q[i] * y[N-1..0]
            //------------------------------------------------------------------
            c[0] = 0;
            for(j=0..N-1)
                // note that -B*(B-1)<=sm<=B-1, thus sm has type int{B}
                // and -cout has type nat{B} due to -(B-1)<=sm/B<=0
                let(sm = +z(i,j) - (q[i] * y[j] + c[j])) {
                s[j]   = sm % B;
                c[j+1] = -(sm / B);
                }
            s[N] = (+z(i,N) - c[N]) % B;
            isNegative = z(i,N)<c[N]; // determine sign instead of c[N+1]
            if(isNegative) 
                next(q[i]) = q[i] - 1;
        } while(isNegative);
        //----------------------------------------------------------------------
        // Here, q[i] is the largest digit with non-negative s[N..0].
        // We therefore commit the subtraction in that we copy the preliminary
        // result from s to z before computing the next digit q[i].
        //----------------------------------------------------------------------
        w1: pause;
        for(j=0..N-1)
            r[j] = s[j];
    }
    emit(rdy);
    //-------------------------------------------------------------------------
    // check the assertions
    //-------------------------------------------------------------------------
    assert(natval(x,M) == natval(y,N) * natval(q,M) + natval(r,N));
    assert(natval(r,N) < natval(y,N));
}
drivenby Test01 {
    x = [1,3,0,1];
    y = [2,1,3];
    await(rdy);
}