```// ************************************************************************** //
//                                                                            //
//    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 radix-2 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 natval(x,m) = sum(i=0..m-1) ((x[i] ? 1 : 0) * exp(2,i));

module NatDivNonperform([M]bool ?x,[N]bool ?y,[M]bool q,[N]bool r) {
event [M][N+1]bool c;
event [M][N]bool s,rr;

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] : (i==M-1 ? false : rr[i+1][j-1])) )
let(cin = (j==0 ? true : c[i][j]))
}
// q[i]=false iff s[i][N-1..0] is negative
q[i] = (i==M-1 ? c[i][N] : c[i][N] xor rr[i+1][N-1]);
// determine next partial remainder
for(j=0..N-1)
let(xin = (j==0 ? x[i] : (i==M-1 ? false : rr[i+1][j-1])) )
rr[i][j] = (q[i] ? s[i][j] : xin);
}
// determine final remainder
for(j=0..N-1)
r[j] = rr[0][j];

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