```// ************************************************************************** //
//                                                                            //
//    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 carry-lookahead subtraction in analogy to module    //
// NatAddCLA. The only difference is in the rules for the initial generation  //
// and propagation of carry digits.                                           //
// ************************************************************************** //

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 NatSubCLA([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];
p[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[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);

// specification:
if(natval(x,N) >= natval(y,N))
assert(natval(s,N+1) == natval(x,N) - natval(y,N));
assert(s[N]==0 <-> natval(x,N) >= natval(y,N));
assert(s[N]==1 <-> natval(x,N) < natval(y,N));
}
drivenby Test01 {
for(i=0..N-1) {
x[i] = 1;
y[i] = 2;
}
}
drivenby Test02 {
for(i=0..N-1) {
x[i] = (i==N-1 ? 1 : 0);
y[i] = (i==0 ? 1 : 0);
}
}
```