// ************************************************************************** //
//                                                                            //
//    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 the nonrestoring division algorithm as a further    //
// improvement of NatDivModRestore. As in the restoring division algorithm,   //
// the idea is to subtract the dividend as long as the resulting difference   //
// is non-negative. While in the restoring division algorithm the dividend is //
// then added to restore the correct partial remainder, this is not done in   //
// nonrestoring algorithm. Instead, the restoring addition is merged with the //
// next subtraction. A disadvantage compared to the nonrestoring division is  //
// that again a scaled addition operation is required which needs carry digits//
// in the range of nat{B}.                                                    //
//   As all other digit selection algorithms for division, also this version  //
// is based on the computation of the following 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 in NatDivModRestore, the z(i) are stored in r[N-1..0]@x[i-1..0] and   //
// digits are determined by counting the number of subtractions that are done //
// before the result became negative. As explained above there is no addition //
// to restore the correct partial remainder z(i) in case the result became    //
// negative. Instead, an addition of (B-1)*y[N-1..0]*B^(i-1) is then performed//
// instead of subtracting y[N-1..0]*B^(i-1).                                  //
//   To this end, we have to remember whether the previous partial remainder  //
// was negative. See the comments in file NatDivModRestore for the explanation//
// of the computation of isNegative in case of the subtractions. In case of   //
// addition of (B-1)*y[N-1..0]*B^(i-1), this is seen as follows: In this case,//
// the number s'[N..0] was obtained by a subtraction that produced a negative //
// result, and since the carry digits for a simple subtraction are either 0 or//
// -1, it follows that a digit s'[N+1]=-1 could be added to generate a correct//
// sum. Using this corrected sum s', we see that the sum s obtained by adding //
// (B-1)*y[N-1..0] to s' is negative iff the carry c[N+1]=abs((+c[N]+s[N])/B) //
// generated is zero (since s[N+1]=s'[N+1]=-1 is negative). Otherwise, we have//
// c[N+1]==1, and thus s[N+1]==0, so that the sum s is not negative. Finally, //
// note that (-c[N]+s[N])/B!=0 iff (-c[N]+s[N])/B==-1 iff s[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));


module NatDivNonrestore([M]nat{B} ?x,[N]nat{B} ?y,
                           [M]nat{B}  q,[N]nat{B}  r,event !rdy) {
    [N+1]nat{B} c,s;
    bool isNegative;
    // -------------------------------------------------------------------------
    // r[N-1..0]@x[M-1..0] is the initial partial remainder z(m);   
    // -------------------------------------------------------------------------
    isNegative = false;
    for(i=0..N-1)
        r[i] = 0;
    
    // -------------------------------------------------------------------------
    // compute quotient digits
    // -------------------------------------------------------------------------
    for(iup=0..M-1)
        let(i=M-1-iup) {// thus i=M-1..0
        // ---------------------------------------------------------------------
        // r[N-1..0]@x[i..0] is the partial remainder z(i+1);
        // copy the prefix of the first N+1 digits of z(i+1) to s.
        // ---------------------------------------------------------------------
        s[0] = x[i];
        for(j=1..N)
            s[j] = r[j-1];
        // ---------------------------------------------------------------------
        // now subtract y[N-1..0] from z(i+1) until the result becomes negative
        // ---------------------------------------------------------------------
        next(q[i]) = 1;
        do {
            // -----------------------------------------------------------------
            // compute either s[N..0] = s[N..0] - y[N-1..0] 
            // or subtract with restore s[N..0] = s[N..0] + (B-1) * y[N-1..0]
            // -----------------------------------------------------------------
            c[0] = 0;
            for(j=0..N-1)
                // note that -B<=sm<=B-1, thus -1<=sm/B<=0
                let(sm = s[j] + (isNegative ? +c[j]+(B-1)*y[j] : -c[j]-y[j])) {
                next(s[j]) = abs(sm % B);
                c[j+1] = abs(sm / B);
                }
            let(sm = s[N] + (isNegative ? +c[N] : -c[N]))
                next(s[N]) = abs(sm % B);
            next(isNegative) = (isNegative ? (s[N]+c[N]<B) : (c[N]==1 & s[N]==0) );
            sub: pause;
            // -----------------------------------------------------------------
            // update quotient digit
            // -----------------------------------------------------------------
            if(isNegative) next(q[i]) = q[i]-1;
            else if(q[i]!=B-1) next(q[i]) = q[i]+1;
        } while(!isNegative & q[i]!=B-1);
        // ---------------------------------------------------------------------
        // shift the resulting sum into r
        // ---------------------------------------------------------------------
        for(j=0..N-1)
            next(r[j]) = s[j];
        sft: pause;
    }
    // -------------------------------------------------------------------------
    // finally, restore the partial remainder if it became negative
    // -------------------------------------------------------------------------
    if(isNegative) {
        c[0] = 0;
        for(j=0..N-1)
            // note that 0<=sm<=2*B-1, thus 0<=sm/B<=1
            let(sm = r[j] + c[j] + y[j]) {
            next(r[j]) = sm % B;
            c[j+1] = sm / B;
            }
        add: pause;
    }
    emit(rdy);
    // -------------------------------------------------------------------------
    // check 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);
}