```// ************************************************************************** //
//                                                                            //
//    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 is a combinational implementation of NatDivModNonrestoreOpt for//
// the special case of radix 2. Since the entire computation is done within a //
// single macro step, the different partial remainders have to be stored      //
// separately in variables rr[i]. The same holds for the carry digits of the  //
// subtractions/additions. The variable isNegated has been replaced with q[i] //
// itself since q[i]==0 holds iff isNegated is false.                         //
// ************************************************************************** //

macro M =  4;    // 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] * exp(2,i));

[M]nat{2}  q,[N]nat{2}  r) {
event [M][N+1]nat{2} c,rr;
event [N+1]nat{2} cr;
// -------------------------------------------------------------------------
// compute quotient digits
// -------------------------------------------------------------------------
for(iup=0..M-1)
let(i=M-1-iup) {// thus, i=M-1..0
c[i][0] = 0;
for(j=0..N-1)
// note that -2<=sm<=1, thus -1<=sm/2<=0
let(sJ  = (j==0 ? x[i] : (i==M-1 ? 0 : rr[i+1][j-1])) )
let(sgn = (i==M-1 ? -1 : (q[i+1]==0 ? +1 : -1)))
let(sm  = sJ + sgn * (c[i][j]+y[j])) {
rr[i][j]  = abs(sm % 2);
c[i][j+1] = abs(sm / 2);
}
// q[i]=0 iff rr[i] is negative
q[i] = (i==M-1 ? (c[i][N]==1 ? 0 : 1)
: (q[i+1]==0 ? (rr[i+1][N-1]+c[i][N]<2 ? 0 : 1)
: (c[i][N]==1 & rr[i+1][N-1]==0 ? 0 : 1)));
}
// -------------------------------------------------------------------------
// finally, restore the partial remainder if it became negative
// -------------------------------------------------------------------------
if(q[0]==0) {
cr[0] = 0;
for(j=0..N-1)
// note that 0<=sm<=2, thus 0<=sm/2<=1
let(sm = rr[0][j] + cr[j] + y[j]) {
r[j] = sm % 2;
cr[j+1] = sm / 2;
}
} else {
for(j=0..N-1)
r[j] = rr[0][j];
}
// -------------------------------------------------------------------------
// check assertions
// -------------------------------------------------------------------------
if(exists(i=0..N-1) (y[i]!=0)) {
assert(natval(x,M) == natval(y,N) * natval(q,M) + natval(r,N));
assert(natval(r,N) < natval(y,N));
}

}
drivenby Test01 {
x = [1,1,0,1];
y = [1,0,1];
}

```