// ************************************************************************** //
//                                                                            //
//    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 carry-lookahead adder for radix-B numbers with    //
// N digits. The adder has a depth of K+2 and a size of O(K*2^K) with K=log(N)//
// and allows the addition of N=2^K digit numbers in time O(K)=O(log(N)).     //
// The construction idea is therefore as follows: The adder consists of a row //
// of special full adders that is connected with a binary tree of the carry   //
// lookahead logic:                                                           //
//                                                                            //
//                  | | ^     | | ^        | | ^     | | ^                    //
//                  v v |     v v |        v v |     v v |                    //
//                  ----      ----         ----      ----    cin              //
//                 | FA |<-| | FA |<--|   | FA |<-| | FA |<--|                //
//                  ----   |  ----    |    ----   |  ----    |                //
//                  |  |   |  |  |    |    |  |   |  |  |    |                //
//                  v  v   |  v  v    |    v  v   |  v  v    |                //
//                  --------------    |    --------------    |                //
//                 |     CLG      |<--|   |     CLG      |<--|                //
//                  --------------    |    --------------    |                //
//                       |  |         |         |  |         |                //
//                       v  v         |         v  v         |                //
//                       ---------------------------         |                //
//                      |           CLG             |<-------|                //
//                       ---------------------------                          //
//                                  |  |                                      //
//                                  v  v                                      //
//                                                                            //
// where each CLG module has inputs g2,p2,g1,p1, and cin and outputs g,p, and //
// cout (which is the carry of the FA in the middle of the CLG module as well //
// as the cin-input of the CLG rightmost modules of the left subtree of the   //
// considered CLG module). These signals are defined as follows:              //
//                                                                            //
//      p = p1 & p2                                                           //
//      g = g2 | g1 & p2                                                      //
//      cout = g1 | p1 & cin                                                  //
//                                                                            //
// and have the following meaning: p holds iff cin propagates through all the //
// full adders connected with the CLG module, and g holds if a carry bit is   //
// generated by one of these adders.                                          //
// The implementation below has the weakness that the local arrays for p and g//
// are defined for N=exp(2,K) but require only exp(2,K-i) values in level i.  //
// ************************************************************************** //

macro B = 4;        // base of the radix numbers
macro N = 4;        // number of digits
macro K = log(N);   // depth of the carry lookahead tree
macro natval(x,m) = sum(i=0..m-1) (x[i] * exp(B,i));

// WidthOfLevel determines the number of wires at level i of the lookahead tree
macro WidthOfLevel(i,n) = (i==0 ? n : WidthOfLevel(i-1,(n+1)/2));

// recur and indices are used to determine the indices to define the carry signals
// if i=indices(k) holds, then 
//  - i.0 is the largest exponent s.t. exp(2,i.0) divides k
//  - i.1 := exp(2,i.0)
//  - i.2 is determined such that k=i.1*(i.2+1)
macro recur(x) = (x.0+1,2*x.1,x.2);

macro indices(k) = (k%2==1 ? (0,1,k-1) : recur(indices(k/2)));


module NatAddCLA([N]nat{B} ?x,?y,[N+1]nat{B} s){
    event [N]bool c;
    event [K+1][N]bool p,g;

    // first row of generate and propagate signals
    for(i=0..N-1) {
        g[0][i] = x[i] + y[i] >= B;
        p[0][i] = x[i] + y[i] == B-1;
    }

    // deeper levels of generate and propagate signals as parallel prefix tree
    for(i=0..K-1)
        let(s = exp(2,i))
        let(w1 = WidthOfLevel(i,N))
        let(w2 = (w1+1)/2)
        for(j=0..w2-1) {
            g[i+1][j] = (2*j+1==w1 
                        ? g[i][2*j]
                        : g[i][2*j+1] | g[i][2*j] & p[i][2*j+1]);
            p[i+1][j] = (2*j+1==w1 
                        ? p[i][2*j]
                        : p[i][2*j+1] & p[i][2*j]);
        }

    // determine the carry signals in terms of g[i][j] and p[i][j]
    c[0] = false;
    for(k=1..N-1)
        let(i = indices(k))
        c[k] = g[i.0][i.2] | c[i.1*i.2] & p[i.0][i.2];

    // compute the sum digits
    for(i=0..N-1) {
        s[i] = (x[i] + y[i] + (c[i]?1:0)) %B;
    }
    s[N] = (g[K][0] ? 1 : 0);

    // alltogether, the addition operation is performed
    assert(natval(s,N+1) == natval(x,N) + natval(y,N));
}
drivenby Test01 {
    for(i=0..N-1) {
        x[i] = B-1;
        y[i] = 1;
    }
}
drivenby Test02 {
    for(i=0..N-1) {
        x[i] = B-1;
        y[i] = (i==0 ? 1 : 0);
    }
}