// ************************************************************************** // // // // 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 addition of signed digit numbers. // // It works for radix base B and digit set {-D,…,D} with (B/2)+1 <= D < B, // // thus it cannot be directly used for binary signed digit numbers. For B=2, // // one can however perform the algorithm below by grouping k bits into a digit// // to base B=2^k using D=2^k-1. // // ************************************************************************** // 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 // macro to evaluate a signed digit number macro sgnval(x,k) = sum(i=0..k-1) (x[i] * exp(B,i)); module SgnAdd([N]int{D+1} ?x,?y,[N+1]int{D+1} s) { [N+1]int{2} t; // transfer digits // compute sum and transfer digits in parallel t[0] = 0; for(i=0..N-1) let(ds = x[i]+y[i]) { t[i+1] = (ds>=D?1:(ds<=-D?-1:0)); s[i] = ds + t[i] - t[i+1] * B; } s[N] = t[N]; // assertion assert(sgnval(s,N+1) == sgnval(x,N) + sgnval(y,N)); }