// ************************************************************************** //
//                                                                            //
//    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                                             //
//                                                                            //
// ************************************************************************** //
    
package latex.QuartzLRM.Experiments.Arithmetic;
import examples.Algorithms.Arithmetic.RadixB.*;
    
macro B = 4;    // base of the radix numbers
macro M = 4;    // number of digits used for x
macro N = 4;    // number of digits used for y

module TestIntSubCRA([N]nat{B} ?x,[N]nat{B} ?y,[N+1]nat{B} s) {
    loop {
        IntSubCRA(x,y,s);
        pause;
    }
}
drivenby {
    [M+N+1]nat{2} carry;
    do {
        carry[0] = 1;
        for(i=0..N-1)
            let(sm = y[i] + carry[i]) {
            next(y[i]) = sm % B;
            carry[i+1] = sm / B;
        }
        for(i=0..M-1)
            let(sm = x[i] + carry[N+i]) {
            next(x[i]) = sm % B;
            carry[N+i+1] = sm / B;
        }
        pause;
    } while(!(forall(i=0..M-1) (x[i]==0) & forall(j=0..N-1) (y[j]==0)));
}