// ************************************************************************** // // // // 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 integers: Given integers 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 as B-complement // // numbers, but the algorithm needs to know the number M of digits that x has // // in B-complement format. The algorithm then computes a sequence of numbers // // z(m),...,z(0): // // (1) z(m) = x + q[M] * y[N-1..0] * B^M // // (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) 0 <= z(i) < |y|*B^i // // Hence, for i=0, it follows that z(0) < y and x = q*y+z(0), so that 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 = 10; macro M = 5; module IntDivAlgo(int ?x,?y,q,r,event !rdy) { nat z,i; int qy,qi,sgn_y; event isNegative; // is set when z < qi * sgn_y * y * exp(B,i) assume(-(B/2)*exp(B,M-1) <=x & x<(B/2)*exp(B,M-1)); sgn_y = (y<0 ? -1 : +1); qi = (x>=0 ? 0 : -1); q = qi * exp(B,M); z = x - qi * sgn_y * y * exp(B,M); i = M; do { // try digits qi = B-1,…,0 until z >= qi * sgn_y * y * exp(B,i) next(qi) = B-1; next(i) = i-1; do { w0: pause; qy = qi * sgn_y * y * exp(B,i); isNegative = z<qy; if(isNegative) next(qi) = qi - 1; } while(isNegative); // here qi is the maximal digit with z >= qy = qi * sgn_y * y * exp(B,i) next(z) = z - qy; next(q) = q + qi * exp(B,i); w1: pause; assert(z == x - q * sgn_y * y); assert(0<= z & z<abs(y) * exp(B,i)); } while(i>0); // determine quotient and remainder next(q) = (y<0 ? -q : q); next(r) = z; pause; emit(rdy); assert(x == q * y + r); assert(0<= r & r < abs(y)); } drivenby Test01 { x = +34322; y = +27; await(rdy); } drivenby Test02 { x = +34322; y = -27; await(rdy); } drivenby Test03 { x = -34322; y = +27; await(rdy); } drivenby Test04 { x = -34322; y = -27; await(rdy); }