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

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

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