```// ************************************************************************** //
//                                                                            //
//    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 division algorithm is an improvement of NatDivModSeq0: It eliminates  //
// the local variable z which was used to store the numbers z(j) mentioned    //
// below. It has to be remarked that only N+1 digits of the numbers z(j) are  //
// relevant for the subtractions, where the rightmost one is always x[i].     //
// Thus, in the algorithm below, the leftmost N of these N+1 digits are       //
// stored in number r, while the rightmost one is directly taken from x[i]    //
// (see macro z). The complete number is z(i) = r[N-1..0]@x[i-1..0].          //
// The remaining ideas of the algorithm are the same as in NatDivModSeq0, i.e.//
// for the given radix-B numbers x and y having M and N digits, it computes a //
// sequence of 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 mentioned above, the numbers z(i) are stored in r[N-1..0]@x[i-1..0].  //
// The quotient digit q[i-1] is determined naively by simply calculating      //
// z(i) - q[i-1] * y[N-1..0] * B^(i-1) for each digit q[i-1] starting from B-1//
// until the result is non-negative.                                          //
//   For the definition of isNegative, note again that the leading digit of s //
// would be c[N+1] = (-c[N] + z(i+N)) / B, which is either -1 or 0. Thus, we  //
// have isNegative <-> c[N+1]==-1 <-> -c[N] + z(i+N) < 0 <-> z(i+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));
macro z(i,j) = (j>0 ? r[j-1] : x[i]); // r[N-1..0]@x[i] replaces z[N+i..i]

module NatDivSeq1([M]nat{B} ?x,[N]nat{B} ?y,
[M]nat{B}  q,[N]nat{B}  r,event !rdy) {
[N+1]nat{B} s,c;  // auxiliary variables
event isNegative; // is set when subtraction yields negative result
// -------------------------------------------------------------------------
// prepare initial partial remainder z(m) = r[N-1..0]@x[m]
// -------------------------------------------------------------------------

for(i=0..N-1)
r[i] = 0;

//-------------------------------------------------------------------------
// computing the quotient digits
//-------------------------------------------------------------------------
for(iup=0..M-1)
let(i=M-1-iup) {// thus i=M-1..0
// try q[i] = 0,1,... until we reach one where z(i)-q[i]*y[N-1..0]
// becomes negative where z(i) = r[N-1..0]@x[i]
next(q[i]) = B-1;
do {
w0: pause;
//------------------------------------------------------------------
// compute s[N..0] = r[N-1..0]@x[i] - q[i] * y[N-1..0]
//------------------------------------------------------------------
c[0] = 0;
for(j=0..N-1)
// note that -B*(B-1)<=sm<=B-1, thus sm has type int{B}
// and -cout has type nat{B} due to -(B-1)<=sm/B<=0
let(sm = +z(i,j) - (q[i] * y[j] + c[j])) {
s[j]   = sm % B;
c[j+1] = -(sm / B);
}
s[N] = (+z(i,N) - c[N]) % B;
if(isNegative)
next(q[i]) = q[i] - 1;
} while(isNegative);
//----------------------------------------------------------------------
// Here, q[i] is the largest digit with non-negative s[N..0].
// We therefore commit the subtraction in that we copy the preliminary
// result from s to z before computing the next digit q[i].
//----------------------------------------------------------------------
w1: pause;
for(j=0..N-1)
r[j] = s[j];
}
emit(rdy);
//-------------------------------------------------------------------------
// check the 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);
}
```