// ************************************************************************** //
//                                                                            //
//    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 adder for radix-B numbers that makes use of a//
// processors arithmetic where the full word size is used to represent radix-B//
// digits. For this reason, the carry digit  must be computed differently to  //
// the reference implementation of a full adder given in module FullAdd.      //
// The correctness of the module below is seen as follows:                    //
//                                                                            //
// Case 1: 0<=x+y+cin<B: In this case, we must have cout=0, so that we have to//
// prove that s<x will never happen, and that in case s==x, we have cin=0. To //
// this end, we note that by the case assumption, we have s = x+y+cin, thus:  //
//                                                                            //
//    * s<x <=> y+cin<0 <=> false                                             //
//    * s=x <=> y+cin=0 <=> y=cin=0                                           //
//                                                                            //
// Case 2: B<=x+y+cin<2B-1: In this case, we must have cout=1, so that we have//
// to prove that s>x will never happen, and that in case s==x, we have cin=1. //
// To this end, note that in this case, we have s = x+y+cin-B, and therefore: //
//                                                                            //
//    * s<x <=> y+cin<B <=> !(y=B-1 & cin=1)                                  //
//    * s=x <=> y+cin=B <=>  (y=B-1 & cin=1)                                  //
//    * s>x <=> y+cin>B <=> false                                             //
//                                                                            //
// ************************************************************************** //

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 NatFullAdd(nat{B} ?x,?y,nat{2} ?cin,cout,nat{B} s) {
    s = uadd(x,uadd(y,cin));
    cout = ((s<x)?1:((s==x)?cin:0));
    assert(x+y+cin == cout * B + s);
}