// ************************************************************************** // // // // 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 standard algorithm for signed digit addition of numbers to base B needs// // a digit set {-D,..,D} with (B/2)+1 <= D < B which does not exist for B=2. // // For this reason, [Parh88] suggested to recode the given binary SD-numbers // // to the digit set {-1,0,+1} such that there are no two neighboring digits // // x[i+1] and x[i] where x[i+1]*x[i]=1 holds. // // Below, we first analyze the problem and present then an alternative to // // previously used binary SD-addition algorithms. To define the addition, we // // have to add two digits xi and yi of given numbers plus the transfer digit // // tin that comes from the neighboring digits to the right. All of xi, yi, and// // tin belong to the digit set {-1,0,+1}, and we have to define digits tout // // and si such that the following holds: // // // // (1) xi + yi + ti = tout*2 + si // // (2) tout, si are digits from {-1,0,+1} // // (3) tout is defined independent of tin (to avoid propagation chains) // // // // To this, end consider the table given below: The first three columns list // // the possible inputs for xi, yi and tin. The next column contains values of // // another input lin that is discussed below, and should be first ignored. The// // next two columns are values for tout and si that were computed by the // // standard SD addition algorithm, i.e. // // / // // | +1 if xi+yi>=+1 // // tout := < -1 if xi+yi<=-1 and si := xi+yi+ti - tout * 2 // // | 0 otherwise // // \ // // solution // // ========================= ======= ======= ======= // // xi yi tin lin -> tout si tout si tout si tout si // // ========================= ======= ======= ======= // // -1 -1 -1 T -> -1 -1 -1 -1 // // -1 -1 0 * -> -1 0 -1 0 // // -1 -1 +1 F -> -1 +1 -1 +1 // // ------------------------- ------ // // -1 0 -1 T -> -1 0 + 0 -2 +1 -4 -1 0 // // -1 0 0 * -> -1 +1 + 0 -1 +1 -3 -1 +1 // // -1 0 +1 F -> -1 +2 * 0 0 +1 -2 0 0 // // ------------------------- ------ // // -1 +1 -1 T -> 0 -1 0 -1 // // -1 +1 0 * -> 0 0 0 0 // // -1 +1 +1 F -> 0 +1 0 +1 // // ------------------------- ------ // // 0 -1 -1 T -> -1 0 + -1 0 // // 0 -1 0 * -> -1 +1 + -1 +1 // // 0 -1 +1 F -> -1 +2 * 0 0 // // ------------------------- ------ // // 0 0 -1 T -> 0 -1 0 -1 // // 0 0 0 * -> 0 0 0 0 // // 0 0 +1 F -> 0 +1 0 +1 // // ------------------------- ------ // // 0 +1 -1 T -> +1 -2 * 0 0 // // 0 +1 0 * -> +1 -1 + +1 -1 // // 0 +1 +1 F -> +1 0 + +1 0 // // ------------------------- ------ // // +1 -1 -1 T -> 0 -1 0 -1 // // +1 -1 0 * -> 0 0 0 0 // // +1 -1 +1 F -> 0 +1 0 +1 // // ------------------------- ------ // // +1 0 -1 T -> +1 -2 * 0 0 // // +1 0 0 * -> +1 -1 + +1 -1 // // +1 0 +1 F -> +1 0 + +1 0 // // ------------------------- ------ // // +1 +1 -1 T -> +1 -1 +1 -1 // // +1 +1 0 * -> +1 0 +1 0 // // +1 +1 +1 F -> +1 +1 +1 +1 // // ========================= ====== // // // // As can be seen, the algorithm computes sometimes values for si that are not// // in the allowed range. The symbol * after the column of si marks these rows,// // and the symbol + denotes rows having input values for xi and yi that lead // // to a wrong value of si when another value of tin is chosen. Hence, triples // // (xi,yi,tin) are defined as equivalent if they have the same values for xi // // and yi, and to fulfill constraint (3), we have to assign the same value for// // tout for all equivalent inputs. The dashed lines group equivalent inputs. // // Now, consider the second input class (xi=-1; yi=0): Using tout=-1 leads // // to value si=+2 for tin=+1, using tout=0 leads to value si=-2 for tin=-1, // // and using tout=+1 leads to forbidden values of si for all values of tin. // // Thus, it is not possible to define a value for tout that only depends on xi// // and yi, but not on tin. // // The algorithm below uses however an additional information that solves the// // mentioned problem. As the algorithm describes a hardware circuit, we make // // use of an encoding of the digits {-1,0,+1} by a pair of booleans (x.0,x.1).// // There are many encodings of the digits {-1,0,+1}, but the following two are// // the most popular ones: // // // // +----+---------------+---------------+ // // | val| signed-value | neg-pos | // // + ---+---------------+---------------+ // // | -1 | (true,true) | (true,false) | // // | 0 | (false,false) | (false,false) | // // | +1 | (false,true) | (false,true) | // // +----+---------------+---------------+ // // // // The algorithm below is based on the neg-pos encoding. To add two digits, it// // makes use of an input lin such that (lin ? tin!=+1 : tin!=-1) holds, and we// // generate an output lout with (lout ? tout!=+1 : tout!=-1) that is forwarded// // to the leftmost full adder, while lin comes from output lout of the adder // // to the right. We define lout := x.0 | y.0, which means by to the encoding // // that lout holds if and only if at least one of the digits is -1. // // We prove that (lout ? tout!=+1 : tout!=-1) holds by inspecting the table // // above, where the solution computed by the algorithm below is given as the // // two rightmost columns, and we can also verify that the important equation // // dec(x) + dec(y) + dec(tin) == 2 * dec(tout) + dec(s) is given, and that all// // values computed are legal digits. // // It is interesting to note that lin and lout have strong relationships to // // tin and tout due to the mentioned invariants. However, lout only depends on// // the digits x and y, while tout depends on lin, but not on tin. This is very// // important: In principle, we could replace lin by (tin!=-1) without making // // the circuit incorrect. However, the circuit would then suffer from carry // // propagation since tout depend on tin, which is the tout of the neighbor. // // In the circuit below, lin only depends on the rightmost digits x’,y’, and // // therefore tout only depends on the current digits x,y, and x’,y’. Thus, all// // transfer digits can be computed in parallel in O(1). Then, the sum digits s// // can be computed in a second step in time O(1). Thus, the circuit below also// // allows a carry-free addition of binary SD-numbers without having the need // // to re-encode the inputs. The crucial fact used here is that we can extract // // enough information of the rightmost digits to distinguish the cases where // // forbidden digits for s would be computed within the critical inputs. Note // // that lin does not have the complete information to determine tin. // // Note that another way to derive a binary SD adder is to group pairs of // // binary SD digits into SD digits to base 4 with the digit set {-3,..,+3}. // // ************************************************************************** // macro enc(x) = (x==-1 ? (true,false) : (x==0 ? (false,false) : (false,true))); macro dec(x) = (x.0?-1:0) + (x.1?+1:0); module SgnFullAdd((bool*bool) ?tin,?x,?y,bool ?lin,lout,(bool*bool) tout,s) { event w1,w2,w3,w4,w,u1,u0; loop { pause; // define the critical input cases: w1 = !x.0 & !x.1 & y.1; // x==0 & y==+1 w2 = !x.0 & !x.1 & y.0; // x==0 & y==-1 w3 = !y.0 & !y.1 & x.1; // y==0 & x==+1 w4 = !y.0 & !y.1 & x.0; // y==0 & x==-1 w = w1 | w2 | w3 | w4; // whether one of the critical inputs is given u1 = !lin & w; // tin!=-1 & critical input u0 = lin & w; // tin!=+1 & critical input // note that lout does NEITHER depend on lin NOR on tin lout = x.0 | y.0; // tout tout.0 = x.0 & y.0 | lin & (w2 | w4); // x=y=-1 | tin!=+1 & x+y=-1 tout.1 = x.1 & y.1 | !lin & (w1 | w3); // x=y=+1 | tin!=-1 & x+y=+1 // s depends on tin,lin,x and y s.0 = tin.0 & !u0 | u1 & !tin.1; s.1 = tin.1 & !u1 | u0 & !tin.0; assert( !(x.0 & x.1) // (x.0,x.1) is a legal digit & !(y.0 & y.1) // (y.0,y.1) is a legal digit & !(tin.0 & tin.1) // (tin.0,tin.1) is a legal digit & (lin ? !tin.1 : !tin.0) // assume invariant for lin -> (// assert correct computation of tout and s dec(x) + dec(y) + dec(tin) == 2 * dec(tout) + dec(s) & !(tout.0 & tout.1) // (tout.0,tout.1) is a legal digit & !(s.0 & s.1) // (s.0,s.1) is a legal digit & (lout ? !tout.1 : !tout.0) // assert invariant for lout )); } } drivenby { bv{7} v; nat{129} i; pause; do { v = nat2bv(i,7); lin = v{6}; tin.0 = v{5}; tin.1 = v{4}; x.0 = v{3}; x.1 = v{2}; y.0 = v{1}; y.1 = v{0}; next(i) = i+1; pause; } while(i<128); }