```// ************************************************************************** //
//                                                                            //
//    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  //
// ************************************************************************** //

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]))
}

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

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

// 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)));
}
}
```