// ************************************************************************** //
//                                                                            //
//    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-2 numbers         //
// With a depth of log(N) and a size of O(N), the circuit is therefore optimal//
// both concerning the depth and the size. For explanations on the macros to  //
// define the prefix tree, see the modules on general radix-B arithmetic.     //
// ************************************************************************** //

macro N = 6;        // number of digits
macro K = log(N);   // depth of the carry lookahead tree
macro natval(x,m) = sum(i=0..m-1) ((x[i]?1:0) * exp(2,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));
macro SumOfWidths(j) = sum(i=0..j) WidthOfLevel(i,N);
// index mapping to map the two-dimensional arrays p,g to a one-dimensional ones
macro idm(i,j) = (i==0 ? j : j+SumOfWidths(i-1));
// recur and indices are used to determine 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 NatAddCLAOpt([N]bool ?x,?y,[N+1]bool s){
    event [N]bool c;
    event [SumOfWidths(K)]bool p,g;

    // first row of generate and propagate signals
    for(i=0..N-1) {
        g[idm(0,i)] = x[i] & y[i];
        p[idm(0,i)] = x[i] | y[i];
    }

    // 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[idm(i+1,j)] = (2*j+1==w1 
                            ? g[idm(i,2*j)]
                            : g[idm(i,2*j+1)] | g[idm(i,2*j)] & p[idm(i,2*j+1)]);
            p[idm(i+1,j)] = (2*j+1==w1 
                            ? p[idm(i,2*j)]
                            : p[idm(i,2*j+1)] & p[idm(i,2*j)]);
        }

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

    // compute the sum digits
    for(i=0..N-1) {
        s[i] = x[i] xor y[i] xor c[i];
    }
    s[N] = g[idm(K,0)];

    // alltogether, the addition operation is performed
    assert(natval(s,N+1) == natval(x,N) + natval(y,N));
}