// ************************************************************************** //
//                                                                            //
//    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 2-complement 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.                                                        //
// ************************************************************************** //

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


module IntMulCSACRA([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 carry-save array
    event [N]bool cr;       // carries for summation in final CRA
    event pM;               // for intermediate value of p[M-1]
    // construct carry-save array
    for(i=0..M-1) {
        for(j=0..N-1) {
            let(xyin = (i==M-1 xor j==N-1 ? !(x[i]&y[j]) : x[i]&y[j]))
            let(pin  = (i==0 ? (j==N-1) : (j==N-1 ? false : pp[i-1][j])))
            let(cin  = (i==0 ? false : cp[i-1][j]))
            let(pout = (j==0 ? (i==M-1 ? pM : p[i]) : pp[i][j-1]))
            let(cout = cp[i][j])
            FullAdd(xyin,pin,cin,cout,pout);
        }
    }
    p[M-1] = !pM;
    // carry-ripple addition of the last row
    for(j=0..N-1)
        let(xin  = cp[M-1][j])
        let(pin  = (j==N-1 ? true : pp[M-1][j]))
        let(cin  = (j==0 ? pM : cr[j-1]))
        let(sout = p[M+j])
        let(cout = cr[j])
        FullAdd(xin,pin,cin,cout,sout);
    // check the result
    assert(intval(p,M+N) == intval(x,M) * intval(y,N));
}