// ************************************************************************** //
//                                                                            //
//    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 restoring division algorithm for radix 2. See   //
// the detailed comments in NatDivModRestore.qrz for the general description  //
// of the algorithm.                                                          //
// ************************************************************************** //

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(2,i));


module NatDivRestoreRadix2([M]nat{2} ?x,[N]nat{2} ?y,
                              [M]nat{2}  q,[N]nat{2}  r,event !rdy) {
    [N+1]nat{2} s;    // sum digits of difference
    [N+1]nat{2} c;    // carry digits of subtraction
    event isNegative; // is set when subtraction yields negative result
    // -------------------------------------------------------------------------
    // 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
        // ---------------------------------------------------------------------
        // r[N-1..0]@x[M-1..0] is the initial partial remainder z(i+1);
        // copy the prefix of the first N+1 digits to s.
        // ---------------------------------------------------------------------
        s[0] = x[i];
        for(j=1..N)
            s[j] = r[j-1];
        // ---------------------------------------------------------------------
        // now subtract s[N..0] = s[N..0] - y[N-1..0]
        // ---------------------------------------------------------------------
        c[0] = 0;
        for(j=0..N-1)
            // note that -2<=sm<=1, thus -1<=sm/2<=0
            let(sm = -c[j] + s[j] - y[j]) {
            next(s[j]) = abs(sm % 2);
            c[j+1] = abs(sm / 2);
            }
        next(s[N]) = abs((-c[N] + s[N]) % 2);
        next(isNegative) = (c[N]==1 & s[N]==0);
        next(q[i]) = 1;
        sub: pause;
        // ---------------------------------------------------------------------
        // restore if s became negative; and in each case, put the 
        // result in r, so that the next partial remainder is obtained
        // ---------------------------------------------------------------------
        if(isNegative) { // then restore by adding y[N-1..0] to s[N-1..0]
            c[0] = 0;
            for(j=0..N-1)
                // note that 0<=sm<=2*2-1, thus 0<=sm/2<=1
                let(sm = c[j] + s[j] + y[j]) {
                next(r[j]) = sm % 2;
                c[j+1] = sm / 2;
                }
            next(q[i]) = q[i]-1;
            add: pause;
        } else {
            // shift the resulting sum into r
            for(j=0..N-1)
                next(r[j]) = s[j];
            sft: 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,1,0,1];
    y = [1,0,1];
    await(rdy);
}