// ************************************************************************** //
//                                                                            //
//    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 2-compl. 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.                                                           //
// ************************************************************************** //

macro M =  5;    // number of digits used for x
macro N =  3;    // number of digits used for y
macro dval(x,i,k) = (i==k-1 ? -(x[i]?1:0) : (x[i]?1:0));
macro intval(x,k) = sum(i=0..k-1) (dval(x,i,k) * exp(2,i));


module IntDivNonrestore([M]bool ?x,[N]bool ?y,[M+1]bool q,[N]bool r) {
    event [M+1][N+1]bool crr;   // carry bits for computing rr
    event [M+1][N]bool rr;      // result of restored remainders
    event [M+1]bool p;          // preliminary quotient
    event [M+1]bool cp;         // carry bits to complement the preliminary quotient
    event [M]bool cr;           // carry bits to compute the final remainder

    // According to the B-complement digit recursion, we have to compute 
    // rr[m] := x[M-1..0] - alpha(p[M])*y[N-1..0] which is done as follows:
    //  (1) x>=0:     computes rr[M][N-1..0] = [false,...,false]
    //  (2) x<0,y>=0: computes rr[M][N-1..0] = [x[M-1],…,x[M-1]] + y[N-1..0]
    //  (3) x<0,y<0:  computes rr[M][N-1..0] = [x[M-1],…,x[M-1]] - y[N-1..0]
    // so that the number rr[M][N-1..0]@x[M-1..0] represents the non-negative
    // first remainder as required for the digit recursion below.
    p[M] = x[M-1];
    for(j=0..N-1) {
        let(xin = x[M-1])
        let(yin = x[M-1] & (y[N-1] xor y[j]))
        let(cin = (j==0 ? x[M-1] & y[N-1] : crr[M][j]))
        FullAdd(xin,yin,cin,crr[M][j+1],rr[M][j]);
    }

    // compute remaining quotient digits by subtraction and addition
    for(iup=0..M-1)
        let(i=M-1-iup) // thus, i=M-1..0
        let(doSub = (i==M-1 ? true : p[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] : rr[i+1][j-1]) )
            let(yin = doSub xor y[N-1] xor y[j])
            let(cin = (j==0 ? doSub xor y[N-1] : crr[i][j]))
            FullAdd(xin,yin,cin,crr[i][j+1],rr[i][j]);
        }
        // p[i]=false iff rr[i][N-1..0] is negative
        p[i] = !(i==M-1 ? !crr[i][N] : doSub xor crr[i][N] xor rr[i+1][N-1]);
    }

    // determine final quotient and remainder: q = -p if y<0, otherwise q=p
    for(j=0..M)
        let(xin = y[N-1] xor p[j])
        let(cin = (j==0 ? y[N-1] : cp[j-1]))
        FullAdd(xin,false,cin,cp[j],q[j]);

    // if the final partial remainder should be negative, 
    // we have to restore the remainder by an addition
    for(j=0..N-1)
        let(yin = !p[0] & (y[N-1] xor y[j]))
        let(cin = (j==0 ? !p[0] & y[N-1] : cr[j-1]))
        FullAdd(rr[0][j],yin,cin,cr[j],r[j]);

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