// ************************************************************************** // // // // 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; isNegative = z(i,N)<c[N]; // determine sign instead of c[N+1] 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); }