// ************************************************************************** // // // // 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 a procedure for converting signed digit // // numbers to equivalent B-complement numbers. The idea is to represent the // // given number as the subtraction of two non-negative radix-B numbers pos and// // neg so that the conversion can be done by a radix-B subtraction. Since the // // determination of the numbers pos and neg can be done in one step, the time // // required is essentially the time for radix-B subtraction. The algorithm // // below makes use of a simple carry-ripple subtraction requiring O(N) time, // // but clearly, this can be reduced to O(log(N)) time by lookahead algorithms.// // ************************************************************************** // macro D = 3; // digit set is -D,...,-1,0,1,...,D macro B = 5; // base of the radix numbers macro N = 4; // number of digits used for the addition // macros for signed digit and B-complement numbers macro alpha(x) = (x<B/2 ? +x : +x-B); macro gamma(y) = (y<0 ? y+B : y); macro dval(x,i,k) = (i==k-1 ? alpha(x[i]) : +x[i]); macro intval(x,k) = sum(i=0..k-1) (dval(x,i,k) * exp(B,i)); macro sgnval(x,k) = sum(i=0..k-1) (x[i] * exp(B,i)); module Sgn2IntPrinciple([N]int{D+1} ?x,[N+1]nat{B} y) { [N]nat{B} pos,neg; // positive and negative digits [N+1]nat{2} c; // carry // extract positive and negative digits of given number a for(i=0..N-1) { if(x[i]<0) { pos[i] = 0; neg[i] = -x[i]; } else { pos[i] = +x[i]; neg[i] = 0; } } // pos and neg are both signed-digit and radix-B numbers; // hence, we can perform B-complement subtraction pos-neg for conversion c[0] = 0; for(i=0..N-1) if(pos[i]>=neg[i]+c[i]) { c[i+1] = 0; y[i] = (pos[i]-(neg[i]+c[i])) % B; } else { c[i+1] = 1; y[i] = (B+pos[i]-(neg[i]+c[i])) % B; } // final digit according to B-complement y[N] = gamma(-c[N-1]); // assertion assert(intval(y,N+1) == sgnval(x,N)); }