// ************************************************************************** // // // // 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 below is a specialization of NatDivModNonrestoreOpt for the // // special case of radix 2. The algorithm eliminates the inner while-loop and // // therefore produces in each step a valid digit of the quotient. // // ************************************************************************** // 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(2,i)); module NatDivNonrestoreOptRadix2([M]nat{2} ?x,[N]nat{2} ?y, [M]nat{2} q,[N]nat{2} r,event !rdy) { event [N+1]nat{2} c; event isNegative; // ------------------------------------------------------------------------- // r[N-1..0]@x[M-1..0] is the initial partial remainder z(m); // ------------------------------------------------------------------------- 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 // if isNegative add y[N-1..0], otherwise subtract y[N-1..0] c[0] = 0; for(j=0..N-1) // note that -2<=sm<=1, thus -1<=sm/2<=0 let(sJ = (j>0?r[j-1]:x[i])) let(sgn = (isNegative ? +1 : -1)) let(sm = sJ + sgn * (c[j]+y[j])) { next(r[j]) = abs(sm % 2); c[j+1] = abs(sm / 2); } // determine sign of computed sum s next(isNegative) = (isNegative ? (r[N-1]+c[N]<2) : (c[N]==1 & r[N-1]==0) ); sub: pause; // determine quotient digit q[i] = (isNegative ? 0 : 1); } // ------------------------------------------------------------------------- // finally, restore the partial remainder if it became negative // ------------------------------------------------------------------------- if(isNegative) { c[0] = 0; for(j=0..N-1) // note that 0<=sm<=2, thus 0<=sm/2<=1 let(sm = r[j] + c[j] + y[j]) { next(r[j]) = sm % 2; c[j+1] = sm / 2; } 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,1,0,1]; y = [1,0,1]; await(rdy); }