// ************************************************************************** //
//                                                                            //
//    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                                             //
//                                                                            //
// ************************************************************************** //
// This module implements a full subtractor for radix-B numbers that makes use//
// of a processors arithmetic where the full word size is used to represent   //
// radix-B digits. Compared to the reference module FullSub, the carry digit  //
// must be computed in a different manner as seen below. The correctness is   //
// seen as follows:                                                           //
//                                                                            //
// Case 1: y=B-1 & cin=1: In this case, the intermediate sum uadd(y,cin) is 0 //
// due to machine arithmetic, so that s=x holds. Thus, the program assigns    //
// cout=1 which is correct in this case.                                      //
//                                                                            //
// Case 2: x>=y+cin & y+cin<B: In this case, we have s = x-(y+cin) >= 0, and  //
// the correct value of cout is 0. Since s = x-(y+cin), we have the following //
// equivalences:                                                              //
//                                                                            //
//    * s<x <=> 0<y+cin <=> cin=1 | y>0                                       //
//    * s=x <=> 0=y+cin <=> y=cin=0                                           //
//    * s>x <=> 0>y+cin <=> false                                             //
//                                                                            //
// Thus, in all cases, the program assigns cout=0 as desired.                 //
//                                                                            //
// Case 3: x<y+cin & y+cin<B: In this case, the correct value of cout is 1,   //
// and we have uadd(y,cin)=y+cin and s = B+x-(y+cin), thus                    //
//                                                                            //
//    * s<x <=> B<y+cin <=> false                                             //
//    * s=x <=> B=y+cin <=> y=B-1 & cin=1                                     //
//    * s>x <=> B>y+cin <=> cin=0 | y<B-1                                     //
//                                                                            //
// Again, in all cases, the program assigns cout=1 as desired.                //
//                                                                            //
// ************************************************************************** //

macro B = 8;

// machine arithmetic for unsigned integers
macro umod(x) = (x%B);
macro uadd(x,y) = umod(x+y);
macro usub(x,y) = umod((B+x)-y);
macro umul(x,y) = umod(x*y);


module NatFullSub(nat{B} ?x,?y,nat{2} ?cin,cout,nat{B} s) {
    s = usub(x,uadd(y,cin));
    cout = ((s>x) ? 1 : ((s==x) ? cin : 0));
    if(x>=y+cin)
        assert(x-(y+cin) == cout * B + s);
}