// ************************************************************************** //
//                                                                            //
//    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 BCD code full adder that adds two decimal digits  //
// and a possible carry input (0 or 1) to a decimal sum digits and an boolean //
// carry output. The idea is to first perform a normal radix-2 addition and   //
// then checking whether the result is greater than 9 (which determines c).   //
// In case there is a carry out, the computed sum must be taken modulo 10.    //
// This is easily computed by adding 6 to the preliminary sum.                //
//  Note that with such a BCD code full adder, the usual circuits for CRA/CLA //
// addition as well as the multipliers like Wallace tree multipliers etc can  //
// be generated.                                                              //
// ************************************************************************** //


module BCD_FullAdd(bv{4} ?x,?y,z,bool ?cin,cout) {

    loop {
        [4]bool s,c,u,v;

        // perform a simple binary carry ripple addition
        // this requires 20 gates with depth 4
        for(i=0..3) {
            u[i] = x{i} xor y{i};
            v[i] = x{i} and y{i};
            c[i] = v[i] or  (i==0 ? cin : c[i-1]) and u[i];
            s[i] = u[i] xor (i==0 ? cin : c[i-1]);
        }
        
        // cout holds if the binary sum is >9
        cout = c[3] or s[3] and (s[2] or s[1]); 
    
        // a correction step is necessary if cout holds; in principle we have
        // to compute s[3..0] mod 10 which can be also done by adding 6
        // this in turn can be done with six more gates as follows:
        let(b3 = s[3] xor (cout and (s[2] or s[1])))
        let(b2 = s[2] xor (cout and !s[1]))
        let(b1 = s[1] xor cout)
        z = b3@b2@b1@s[0];

        pause;
    }
}
//drivenby verify {
//    // run the circuit with all possible inputs
//    for(k=0..1) {
//        cin = k==1;
//        for(i=0..9)
//            for(j=0..9) {
//                x = nat2bv(i,4);
//                y = nat2bv(j,4);
//                assert(i+j+(cin?1:0) == (cout?10:0) + bv2nat(z));
//                pause;
//            }
//    }
//}