// ************************************************************************** // // // // 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 // // // // ************************************************************************** // // The following module implements the basic digit recurrence algorithm for // // division of natural numbers: Given natural numbers x and y, the algorithm // // computes the quotient digits of the quotient x/y to radix B as well as the // // remainder r. Note that the given numbers x and y might not be given in // // radix-B format, but the algorithm needs to know the number M of digits that// // x has in radix-B format. The algorithm then 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 // // 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. // // The numbers z(i) are stored in the same variable z that is overwritten // // with these numbers step by step. 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. // // ************************************************************************** // macro B = 4; macro M = 6; module NatDivAlgo(nat ?x,?y,q,r,event !rdy) { nat z,qy,qi,i; // preliminary dividend event isNegative; // is set when z < qi * y * exp(B,i) z = x; i = M; do { // try digits qi = B-1,B-2,... until z >= qi * y * exp(B,i) next(qi) = B-1; next(i) = i-1; do { w0: pause; qy = qi * y * exp(B,i); isNegative = z<qy; if(isNegative) next(qi) = qi - 1; } while(isNegative); // here qi is the maximal digit with z >= qi * y * exp(B,i) next(z) = z - qy; next(q) = q + qi * exp(B,i); w1: pause; assert(z == x - q * y); assert(z<y * exp(B,i)); } while(i>0); // copy the remainder from z r = z; emit(rdy); assert(x == y * q + r); assert(r < y); } drivenby Test01 { x = 10231; y = 312; await(rdy); }