// ************************************************************************** //
//                                                                            //
//    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                                             //
//                                                                            //
// ************************************************************************** //
// For the addition of B-complement numbers, one needs a special full adder to//
// add the most significant digits of the B-complement numbers. These digits  //
// are given as unsigned integers of type nat{B}, but they are interpreted by //
// function alpha given below as signed integers of type int{B/2}. Even though//
// alpha is a cast in programming languages like C, the value cout required   //
// for B-complement addition is not the overflow condition of signed addition.//
//  Instead, the intended values for cout and s must satisfy the following    //
// equation: alpha(x)+alpha(y)+cin == alpha(cout) * B + s. These values are   //
// obviously computed by the following reference implementation:              //
//                                                                            //
// module FullAddBC(nat{B} ?x,?y,nat{2} ?cin,nat{B} cout,nat{B} s) {          //
//     event int{B} sm;                                                       //
//     sm = alpha(x) + alpha(y) + cin;                                        //
//     s = sm % B;                                                            //
//     cout = gamma(sm / B);                                                  //
// }                                                                          //
//                                                                            //
// To show the correctness of the implementation given below, abbreviate the  //
// values xa:=alpha(x) and ya:=alpha(y). Then, the following bounds can be    //
// easily derived for sm=xa+ya+cin                                            //
//                                                                            //
// (1) xa>=0 and ya>=0 --> sm is in {0,…,b-1}+{0,…,b-1}+{0,1}={0,…,2b-1}      //
// (2) xa>=0 and ya<0  --> sm is in {0,…,b-1}+{-b,…,-1}+{0,1}={-b,…,b-1}      //
// (3) xa<0  and ya>=0 --> sm is in {-b,…,-1}+{0,…,b-1}+{0,1}={-b,…,b-1}      //
// (4) xa<0  and ya<0  --> sm is in {-b,…,-1}+{-b,…,-1}+{0,1}={-2b,…,-1}      //
//                                                                            //
// Thus, in case (1), we have (xa+ya+cin)/B=0 and therefore cout=0, and in    //
// case (4), we have (xa+ya+cin)/B=-1, and therefore cout=B-1. In cases (2)   //
// and (3), the value of (xa+ya+cin)/B depends on the sign of sm. However, the//
// sum is not computed by a processor whose word size allows us only to deal  //
// with nat{B} or int{B/2}. In cases (2) and (3) however, the sum sm fits into//
// the machine words, so that we can check the sum for its sign. Now, finally //
// note that x<b holds if and only if alpha(x)>=0 holds.                      //
// Remark: Overflow of signed addition would be cout=(ya>=0 ? s<xa : s>xa).   //
// The example B=4, x=0, y=3, cin=1 yields an overflow while cout should be 0.//
// ************************************************************************** //

macro B = 8;
macro b = 4;

macro alpha(x) = (x<b ? +x : +x-B);
macro gamma(y) = (y<0 ? y+B : y);

// note that addition of signed and unsigned numbers yields the same results 
// on a processor; only the definition of overflow is different

macro uadd(x,y) = (x+y)%B;


module IntFullAdd(nat{B} ?x,?y,nat{2} ?cin,nat{B} cout,s) {
    s = uadd(x,uadd(y,cin));
    if(x<b)
        if(y<b)
            // (1) alpha(x)>=0 & alpha(y)>=0
            cout = 0;
        else
            // (2) alpha(x)>=0 & alpha(y)<0
            cout = (s<b ? 0 : B-1);
    else
        if(y<b)
            // (3) alpha(x)<0 & alpha(y)>=0
            cout = (s<b ? 0 : B-1);
        else 
            // (4) alpha(x)<0 & alpha(y)<0
            cout = B-1;
    assert(alpha(x)+alpha(y)+cin == alpha(cout) * B + s);
}