// ************************************************************************** // // // // 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); }