// ************************************************************************** // // // // 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 a nonrestoring division of radix-2. numbers; i.e. in// // each step, the divisor is subtracted from the dividend and the quotient bit// // is determined by the sign of the result. If the result is negative, the // // correction is combined with the next subtraction which together is then a // // simple addition. // // As can be seen, we need (M+1)*N full adders plus 2*M XOR gates for the // // implementation. // // ************************************************************************** // macro M = 5; // 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] ? 1 : 0) * exp(2,i)); module NatDivNonrestore([M]bool ?x,[N]bool ?y,[M]bool q,[N]bool r) { event [M][N+1]bool c; event [M][N]bool rr; event [N+1]bool cr; for(iup=0..M-1) let(i=M-1-iup) // thus, i=M-1..0 let(doSub = (i==M-1 ? true : q[i+1])) { //subtract or add for(j=0..N-1) { // compute rr[i][N-1..0] = rr[i+1][N-2..0]@x[i] +/- y[N-1..0] let(xin = (j==0 ? x[i] : (i==M-1 ? false : rr[i+1][j-1])) ) let(yin = doSub xor y[j]) let(cin = (j==0 ? doSub : c[i][j])) FullAdd(xin,yin,cin,c[i][j+1],rr[i][j]); } // q[i]=false iff rr[i][N-1..0] is negative q[i] = !(i==M-1 ? !c[i][N] : doSub xor c[i][N] xor rr[i+1][N-1]); } // if the final partial remainder should be negative, // we have to restore the remainder by an addition cr[0] = false; for(j=0..N-1) FullAdd(rr[0][j],!q[0] & y[j],cr[j],cr[j+1],r[j]); // check the specification if(exists(i=0..N-1) y[i]) { assert(natval(x,M) == natval(y,N) * natval(q,M) + natval(r,N)); assert(natval(r,N) < natval(y,N)); } }