// ************************************************************************** // // // // 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. It is essentially a subtraction// // of two radix-B numbers as shown in SD2IntPrinciple. The version below uses // // the numbers pos and neg used in SD2IntPrinciple only implicitly and is // // therefore more space efficient. // // ************************************************************************** // 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 // 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 Sgn2Int([N]int{D+1} ?x,[N+1]nat{B} y) { [N+1]nat{2} c; // we perform B-complement subtraction pos-neg for conversion c[0] = 0; for(i=0..N-1) if(x[i]>=c[i]) { c[i+1] = 0; y[i] = (x[i] - c[i]) % B; } else { c[i+1] = 1; y[i] = (B + x[i] - c[i]) % B; } // final digit according to B-complement y[N] = gamma(-c[N-1]); // specification assert(intval(y,N+1) == sgnval(x,N)); }