// ************************************************************************** //
//                                                                            //
//    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 specialization of NatDivModNonrestoreOpt for the    //
// special case of radix 2. The algorithm eliminates the inner while-loop and //
// therefore produces in each step a valid digit of the quotient.             //
// ************************************************************************** //

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 NatDivNonrestoreOptRadix2([M]nat{2} ?x,[N]nat{2} ?y,
                                    [M]nat{2}  q,[N]nat{2}  r,event !rdy) {
    event [N+1]nat{2} c;
    event isNegative; 
    // -------------------------------------------------------------------------
    // 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
        // if isNegative add y[N-1..0], otherwise subtract y[N-1..0]
        c[0] = 0;
        for(j=0..N-1)
            // note that -2<=sm<=1, thus -1<=sm/2<=0
            let(sJ = (j>0?r[j-1]:x[i]))
            let(sgn = (isNegative ? +1 : -1))
            let(sm = sJ + sgn * (c[j]+y[j])) {
            next(r[j]) = abs(sm % 2);
            c[j+1] = abs(sm / 2);
            }
        // determine sign of computed sum s
        next(isNegative) = (isNegative ? (r[N-1]+c[N]<2) : (c[N]==1 & r[N-1]==0) );
        sub: pause;
        // determine quotient digit
        q[i] = (isNegative ? 0 : 1);
    }
    // -------------------------------------------------------------------------
    // finally, restore the partial remainder if it became negative
    // -------------------------------------------------------------------------
    if(isNegative) {
        c[0] = 0;
        for(j=0..N-1)
            // note that 0<=sm<=2, thus 0<=sm/2<=1
            let(sm = r[j] + c[j] + y[j]) {
            next(r[j]) = sm % 2;
            c[j+1] = sm / 2;
            }
        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,1,0,1];
    y = [1,0,1];
    await(rdy);
}