// ************************************************************************** //
//                                                                            //
//    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 following module implements a multiplication of radix-2 numbers. The   //
// computation is done by summing up the usual partial products by the use of //
// carry-save adders for the intermediate steps and a carry-ripple adder for  //
// the final step.                                                            //
// The depth of the circuit is seen by observing that the evaluation can      //
// proceed row-wise for i=0..M-2, and columnwise for the final row. Thus, the //
// depth of the circuit is O(M+N) and therefore not optimal.                  //
// ************************************************************************** //

macro M = 5;     // number of digits used for x
macro N = 3;     // number of digits used for y
macro natval(x,m) = sum(i=0..m-1) ((x[i]?1:0) * exp(2,i));


module NatMulCSACRA([M]bool ?x,[N]bool ?y,[M+N]bool p) {
    event [M][N-1]bool pp;  // digits of partial products
    event [M][N]bool cp;    // carries for summation in CSA array
    event [N]bool cr;       // carries for summation in final CRA
    // construct carry-save adder array
    // this part has depth O(M) since each row can be evaluted in O(1)
    for(i=0..M-1) {
        for(j=0..N-1) {
            let(pin  = (i==0 | j==N-1 ? false : pp[i-1][j]))
            let(cin  = (i==0 ? false : cp[i-1][j]))
            let(pout = (j==0 ? p[i] : pp[i][j-1]))
            let(cout = cp[i][j])
            FullAdd(x[i]&y[j],pin,cin,cout,pout);
        }
    }
    // final addition is done by carry-ripple addition; in this final row,
    // the numbers pp[M-1][N-2..0] and cp[M-1][N-1..0] are added;
    // this part has depth O(N) due to the carry propagation
    for(j=0..N-1)
        let(s1 = (j==N-1 ? false : pp[M-1][j]))
        let(s2 = cp[M-1][j])
        let(cin = (j==0 ? false : cr[j-1]))
        FullAdd(s1,s2,cin,cr[j],p[M+j]);
    // check the specification
    assert(natval(p,M+N) == natval(x,M) * natval(y,N));
}