// ************************************************************************** //
//                                                                            //
//    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 subtraction of B-complement numbers requires 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}. Hence, 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 reference implementation:       //
//                                                                            //
// module FullSubBC(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})={-b,…,b-1}    //
// (2) xa>=0 and ya<0  --> sm is in {0,…,b-1}-({-b,…,-1}+{0,1})={0,…,2b-1}    //
// (3) xa<0  and ya>=0 --> sm is in {-b,…,-1}-({0,…,b-1}+{0,1})={-2b,…,-1}    //
// (4) xa<0  and ya<0  --> sm is in {-b,…,-1}-({-b,…,-1}+{0,1})={-b,…,b-1}    //
//                                                                            //
// Thus, in case (2), we have (xa-(ya+cin))/B=0 and therefore cout=0, and in  //
// case (3), we have (xa-(ya+cin))/B=-1, and therefore cout=B-1. In cases (1) //
// and (4), the value of (xa-(ya+cin))/B depends on the sign of sm. As can be //
// seen, the sum sm fits into a machine word in these cases, so that variable //
// s holds this value in these cases. Finally, note that x<b holds if and only//
// if alpha(x)>=0 holds.                                                      //
// ************************************************************************** //

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/subtraction 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;
macro usub(x,y) = (+x-y)%B;


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