// ************************************************************************** //
//                                                                            //
//    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 a nonrestoring division of radix-2. numbers; i.e. in//
// each step, the divisor is subtracted from the dividend and the quotient bit//
// is determined by the sign of the result. If the result is negative, the    //
// correction is combined with the next subtraction which together is then a  //
// simple addition.                                                           //
// As can be seen, we need (M+1)*N full adders plus 2*M XOR gates for the     //
// implementation.                                                            //
// ************************************************************************** //

macro M =  5;    // 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] ? 1 : 0) * exp(2,i));


module NatDivNonrestore([M]bool ?x,[N]bool ?y,[M]bool q,[N]bool r) {
    event [M][N+1]bool c;
    event [M][N]bool rr;
    event [N+1]bool cr;

    for(iup=0..M-1)
        let(i=M-1-iup) // thus, i=M-1..0
        let(doSub = (i==M-1 ? true : q[i+1])) { //subtract or add
        for(j=0..N-1) {
            // compute rr[i][N-1..0] = rr[i+1][N-2..0]@x[i] +/- y[N-1..0]
            let(xin = (j==0 ? x[i] : (i==M-1 ? false : rr[i+1][j-1])) )
            let(yin = doSub xor y[j])
            let(cin = (j==0 ? doSub : c[i][j]))
            FullAdd(xin,yin,cin,c[i][j+1],rr[i][j]);
        }
        // q[i]=false iff rr[i][N-1..0] is negative
        q[i] = !(i==M-1 ? !c[i][N] : doSub xor c[i][N] xor rr[i+1][N-1]);
    }
    // if the final partial remainder should be negative, 
    // we have to restore the remainder by an addition
    cr[0] = false;
    for(j=0..N-1)
        FullAdd(rr[0][j],!q[0] & y[j],cr[j],cr[j+1],r[j]);

    // check the specification
    if(exists(i=0..N-1) y[i]) {
        assert(natval(x,M) == natval(y,N) * natval(q,M) + natval(r,N));
        assert(natval(r,N) < natval(y,N));
    }
}