// ************************************************************************** //
//                                                                            //
//    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 is a combinational implementation of NatDivModNonrestoreOpt for//
// the special case of radix 2. Since the entire computation is done within a //
// single macro step, the different partial remainders have to be stored      //
// separately in variables rr[i]. The same holds for the carry digits of the  //
// subtractions/additions. The variable isNegated has been replaced with q[i] //
// itself since q[i]==0 holds iff isNegated is false.                         //
// ************************************************************************** //

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 NatDivNonrestoreOptCombRadix2([M]nat{2} ?x,[N]nat{2} ?y,
                                        [M]nat{2}  q,[N]nat{2}  r) {
    event [M][N+1]nat{2} c,rr;
    event [N+1]nat{2} cr;
    // -------------------------------------------------------------------------
    // compute quotient digits
    // -------------------------------------------------------------------------
    for(iup=0..M-1)
        let(i=M-1-iup) {// thus, i=M-1..0
        c[i][0] = 0;
        for(j=0..N-1)
            // note that -2<=sm<=1, thus -1<=sm/2<=0
            let(sJ  = (j==0 ? x[i] : (i==M-1 ? 0 : rr[i+1][j-1])) )
            let(sgn = (i==M-1 ? -1 : (q[i+1]==0 ? +1 : -1)))
            let(sm  = sJ + sgn * (c[i][j]+y[j])) {
            rr[i][j]  = abs(sm % 2);
            c[i][j+1] = abs(sm / 2);
            }
        // q[i]=0 iff rr[i] is negative
        q[i] = (i==M-1 ? (c[i][N]==1 ? 0 : 1)
                       : (q[i+1]==0 ? (rr[i+1][N-1]+c[i][N]<2 ? 0 : 1) 
                                    : (c[i][N]==1 & rr[i+1][N-1]==0 ? 0 : 1)));
    }
    // -------------------------------------------------------------------------
    // finally, restore the partial remainder if it became negative
    // -------------------------------------------------------------------------
    if(q[0]==0) {
        cr[0] = 0;
        for(j=0..N-1)
            // note that 0<=sm<=2, thus 0<=sm/2<=1
            let(sm = rr[0][j] + cr[j] + y[j]) {
            r[j] = sm % 2;
            cr[j+1] = sm / 2;
            }
    } else {
        for(j=0..N-1)
            r[j] = rr[0][j];
    }
    // -------------------------------------------------------------------------
    // check assertions
    // -------------------------------------------------------------------------
    if(exists(i=0..N-1) (y[i]!=0)) {
        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];
}