// ************************************************************************** //
//                                                                            //
//    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 below is a further improvement of the nonrestoring division    //
// algorithm. It avoids the additional shift steps in that at the first time  //
// where the inner loop is started, the operand used is r[N-1..0]@x[i]        //
// instead of s[N..0]. To this end, we define an event startDigitSearch to    //
// distinguish a first iteration from later ones.                             //
// ************************************************************************** //

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 NatDivNonrestoreOpt([M]nat{B} ?x,[N]nat{B} ?y,
                              [M]nat{B}  q,[N]nat{B}  r,event !rdy) {
    [N+1]nat{B} c,s;
    event isNegative,startDigitSearch; 
    // -------------------------------------------------------------------------
    // r[N-1..0]@x[M-1..0] is the initial partial remainder z(m);   
    // -------------------------------------------------------------------------

   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
        next(q[i]) = 1; // try digits q[i]=1,2,... 
        startDigitSearch = true; // means s=r[N-1..0]@x[i] (implicit shift)
        do {
            // if isNegative add (B-1)*y[N-1..0], otherwise subtract y[N-1..0]
            c[0] = 0;
            for(j=0..N-1)
                // note that -B<=sm<=B-1, thus -1<=sm/B<=0
                let(sJ = (startDigitSearch ? (j>0?r[j-1]:x[i]) : s[j]))
                let(sm = sJ + (isNegative ? +c[j]+(B-1)*y[j] : -c[j]-y[j])) {
                next(s[j]) = abs(sm % B);
                c[j+1] = abs(sm / B);
                }
            let(sN = (startDigitSearch ? r[N-1] : s[N]))
            let(sm = sN + (isNegative ? +c[N] : -c[N])) {
            next(s[N]) = abs(sm % B);
            // determine sign of computed sum s
            next(isNegative) = (isNegative ? (sN+c[N]<B) : (c[N]==1 & sN==0) );
            }
            sub: pause;
            // determine quotient digit for next iteration
            next(q[i]) = (isNegative ? q[i]-1 : (q[i]!=B-1 ? q[i]+1 : q[i]));
        } while(!isNegative & q[i]!=B-1);
        // copy the resulting sum into r
        for(j=0..N-1)
            r[j] = s[j];
    }
    // -------------------------------------------------------------------------
    // 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);
}