```// ************************************************************************** //
//                                                                            //
//    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);
}
```