// ************************************************************************** //
//                                                                            //
//    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 B-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.                                                        //
// 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.                  //
// ** Note: We are only interested in even values of B **                     // 
// ************************************************************************** //

macro B = 4;    // base of the radix numbers
macro M = 5;    // number of digits used
macro N = 3;    // number of digits used

macro alpha(x) = (x<(B/2) ? +x : +x-B);
macro gamma(y) = (y<0 ? y+B : y);
macro dval(x,i,k) = (i==k-1 ? alpha(x[i]) : +x[i]);
macro intval(x,k) = sum(i=0..k-1) (dval(x,i,k) * exp(B,i));


module IntMulCSACRA([M]nat{B} ?x,[N]nat{B} ?y,[M+N]nat{B} p) {
    event [M][N]nat{B} pp;    // digits of partial products
    event [M][N-1]int{B} cp;  // carries for summation in CSA array
    event [N-1]int{2} cr;     // carries for summation in final CRA
    assert(B==2*(B/2));       // check that B is even
    // construct carry-save adder array
    // this part has depth O(M) since each row can be evaluated in O(1)
    for(i=0..M-1) {
        for(j=0..N-2) {
            let(xin  = sat{B}((i==M-1?alpha(x[i]):+x[i])))
            let(pin  = (i==0 ? 0 : pp[i-1][j]))
            let(cin  = (i==0 ? 0 : cp[i-1][j]))
            let(pout = (j==0 ? p[i] : pp[i][j-1]))
            let(cout = cp[i][j])
            FullMulInt(xin,y[j],pin,cin,cout,pout);
        }
        // most significant digits of pp and y
        let(xin  = sat{B}((i==M-1?alpha(x[i]):+x[i])))
        let(pin  = (i==0 ? 0 : pp[i-1][N-1]))
        let(pout = pp[i][N-2])
        let(cout = pp[i][N-1])
        FullMulBC(xin,y[N-1],pin,0,cout,pout);
    }
    // final addition is done by carry-ripple addition; in this final row,
    // the numbers pp[M-1][N-1..0] and cp[M-1][N-2..0] are added;
    // this part has depth O(N) due to the carry propagation
    for(j=0..N-2)
        let(cin = (j==0 ? 0 : cr[j-1]))
        FullAddInt(pp[M-1][j],cp[M-1][j],cin,cr[j],p[M+j]);
    p[M+N-1] = gamma(pp[M-1][N-1] + cr[N-2]);

    // check the result
    assert(intval(p,M+N) == intval(x,M) * intval(y,N));
}
drivenby MinInt_MinInt {
    x[M-1] = B/2;
    for(i=0..M-2)
        x[i] = 0;
    y[N-1] = B/2;
    for(i=0..N-2)
        y[i] = 0;
}
drivenby MinInt_MaxInt {
    x[M-1] = B/2;
    for(i=0..M-2)
        x[i] = 0;
    y[N-1] = (B/2)-1;
    for(i=0..N-2)
        y[i] = B-1;
}
drivenby MaxInt_MinInt {
    x[M-1] = (B/2)-1;
    for(i=0..M-2)
        x[i] = B-1;
    y[N-1] = B/2;
    for(i=0..N-2)
        y[i] = 0;
}
drivenby MaxInt_MaxInt {
    x[M-1] = (B/2)-1;
    for(i=0..M-2)
        x[i] = B-1;
    y[N-1] = (B/2)-1;
    for(i=0..N-2)
        y[i] = B-1;
}
drivenby Test01 {
    for(i=0..M-1)
        x[i] = (-B/2-(i+1)) % B;
    for(i=0..N-1)
        y[i] = (-B/2-(i+1)) % B;
}
drivenby Test02 {
    for(i=0..M-1)
        x[i] = (-B/2-(i+1)) % B;
    for(i=0..N-1)
        y[i] = (-B-1-i) % B;
}
drivenby Test03 {
    for(i=0..M-1)
        x[i] = (-B-1-i) % B;
    for(i=0..N-1)
        y[i] = (-B/2-(i+1)) % B;
}
drivenby Test04 {
    for(i=0..M-1)
        x[i] = (-B-1-i) % B;
    for(i=0..N-1)
        y[i] = (-B-1-i) % B;
}