```// ************************************************************************** //
//                                                                            //
//    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 nonperforming division of 2-compl. numbers, i.e.  //
// in each step of the digit computation of the quotient, the shifted divisor //
// is subtracted from the current dividend. If the result is negative, it is  //
// neglected and the next dividend is just the shifted previous one; otherwise//
// the result of the subtraction defines the next dividend.                   //
// ************************************************************************** //

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 IntDivNonperform([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]))
}

// 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]))
}
// 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]);
// restore by neglecting s
for(j=0..N-1)
let(xin = (j==0 ? x[i] : rr[i+1][j-1]) )
rr[i][j] = (p[i] ? s[i][j] : xin);
}

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