// ************************************************************************** //
//                                                                            //
//    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 restoring 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 immediately done by adding the divisor. Restoring division is//
// can be easily improved by the nonperforming or nonrestoring division.      //
// ************************************************************************** //

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 IntDivRestore([M]bool ?x,[N]bool ?y,[M+1]bool q,[N]bool r) {
    event [M+1][N+1]bool cr;    // carry bits for computing rr
    event [M][N+1]bool cs;      // carry bits for computing s
    event [M+1][N]bool rr;      // result of restored remainders
    event [M][N]bool s;         // result of subtractions
    event [M+1]bool p;          // preliminary quotient
    event [M+1]bool cp;         // carry bits to complement the preliminary quotient

    // 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] : cr[M][j]))
        FullAdd(xin,yin,cin,cr[M][j+1],rr[M][j]);
    }

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

    // 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]);

    for(j=0..N-1)
        r[j] = rr[0][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)));
    }
}