```// ************************************************************************** //
//                                                                            //
//    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 the nonrestoring division algorithm as a further    //
// improvement of NatDivModRestore. As in the restoring division algorithm,   //
// the idea is to subtract the dividend as long as the resulting difference   //
// is non-negative. While in the restoring division algorithm the dividend is //
// then added to restore the correct partial remainder, this is not done in   //
// nonrestoring algorithm. Instead, the restoring addition is merged with the //
// next subtraction. A disadvantage compared to the nonrestoring division is  //
// that again a scaled addition operation is required which needs carry digits//
// in the range of nat{B}.                                                    //
//   As all other digit selection algorithms for division, also this version  //
// is based on the computation of the following numbers z(m),...,z(0):        //
//  (1) z(m) = x                                                              //
//  (2) z(i-1) = z(i) - q[i-1] * y[N-1..0] * B^(i-1) where q[i-1] is the      //
//      maximal digit ∈ {0,...,B−1} with q[i−1]*y[N-1..0]*B^(i-1) ≤ z(i).     //
// It can be easily proved that the following invariants are then true:       //
//  (1) x = z(i) + q[M−1,...,i]*y*B^i                                         //
//  (2) z(i) < y*B^i                                                          //
// Hence, for i=0, it follows that z(0) < y and x = q*y+z(0), so the the final//
// z(0) is the remainder and the q[i] are the digits of the quotient of the   //
// division of x by y.                                                        //
//   As in NatDivModRestore, the z(i) are stored in r[N-1..0]@x[i-1..0] and   //
// digits are determined by counting the number of subtractions that are done //
// before the result became negative. As explained above there is no addition //
// to restore the correct partial remainder z(i) in case the result became    //
// negative. Instead, an addition of (B-1)*y[N-1..0]*B^(i-1) is then performed//
// instead of subtracting y[N-1..0]*B^(i-1).                                  //
//   To this end, we have to remember whether the previous partial remainder  //
// was negative. See the comments in file NatDivModRestore for the explanation//
// of the computation of isNegative in case of the subtractions. In case of   //
// addition of (B-1)*y[N-1..0]*B^(i-1), this is seen as follows: In this case,//
// the number s'[N..0] was obtained by a subtraction that produced a negative //
// result, and since the carry digits for a simple subtraction are either 0 or//
// -1, it follows that a digit s'[N+1]=-1 could be added to generate a correct//
// sum. Using this corrected sum s', we see that the sum s obtained by adding //
// (B-1)*y[N-1..0] to s' is negative iff the carry c[N+1]=abs((+c[N]+s[N])/B) //
// generated is zero (since s[N+1]=s'[N+1]=-1 is negative). Otherwise, we have//
// c[N+1]==1, and thus s[N+1]==0, so that the sum s is not negative. Finally, //
// note that (-c[N]+s[N])/B!=0 iff (-c[N]+s[N])/B==-1 iff s[N]<c[N].          //
// ************************************************************************** //

macro B =  4;    // base of the radix numbers
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(B,i));

module NatDivNonrestore([M]nat{B} ?x,[N]nat{B} ?y,
[M]nat{B}  q,[N]nat{B}  r,event !rdy) {
[N+1]nat{B} c,s;
bool isNegative;
// -------------------------------------------------------------------------
// r[N-1..0]@x[M-1..0] is the initial partial remainder z(m);
// -------------------------------------------------------------------------
isNegative = false;
for(i=0..N-1)
r[i] = 0;

// -------------------------------------------------------------------------
// compute quotient digits
// -------------------------------------------------------------------------
for(iup=0..M-1)
let(i=M-1-iup) {// thus i=M-1..0
// ---------------------------------------------------------------------
// r[N-1..0]@x[i..0] is the partial remainder z(i+1);
// copy the prefix of the first N+1 digits of z(i+1) to s.
// ---------------------------------------------------------------------
s[0] = x[i];
for(j=1..N)
s[j] = r[j-1];
// ---------------------------------------------------------------------
// now subtract y[N-1..0] from z(i+1) until the result becomes negative
// ---------------------------------------------------------------------
next(q[i]) = 1;
do {
// -----------------------------------------------------------------
// compute either s[N..0] = s[N..0] - y[N-1..0]
// or subtract with restore s[N..0] = s[N..0] + (B-1) * y[N-1..0]
// -----------------------------------------------------------------
c[0] = 0;
for(j=0..N-1)
// note that -B<=sm<=B-1, thus -1<=sm/B<=0
let(sm = s[j] + (isNegative ? +c[j]+(B-1)*y[j] : -c[j]-y[j])) {
next(s[j]) = abs(sm % B);
c[j+1] = abs(sm / B);
}
let(sm = s[N] + (isNegative ? +c[N] : -c[N]))
next(s[N]) = abs(sm % B);
next(isNegative) = (isNegative ? (s[N]+c[N]<B) : (c[N]==1 & s[N]==0) );
sub: pause;
// -----------------------------------------------------------------
// update quotient digit
// -----------------------------------------------------------------
if(isNegative) next(q[i]) = q[i]-1;
else if(q[i]!=B-1) next(q[i]) = q[i]+1;
} while(!isNegative & q[i]!=B-1);
// ---------------------------------------------------------------------
// shift the resulting sum into r
// ---------------------------------------------------------------------
for(j=0..N-1)
next(r[j]) = s[j];
sft: pause;
}
// -------------------------------------------------------------------------
// finally, restore the partial remainder if it became negative
// -------------------------------------------------------------------------
if(isNegative) {
c[0] = 0;
for(j=0..N-1)
// note that 0<=sm<=2*B-1, thus 0<=sm/B<=1
let(sm = r[j] + c[j] + y[j]) {
next(r[j]) = sm % B;
c[j+1] = sm / B;
}
add: pause;
}
emit(rdy);
// -------------------------------------------------------------------------
// check assertions
// -------------------------------------------------------------------------
assert(natval(x,M) == natval(y,N) * natval(q,M) + natval(r,N));
assert(natval(r,N) < natval(y,N));
}
drivenby Test01 {
x = [1,3,0,1];
y = [2,1,3];
await(rdy);
}
```