// ************************************************************************** //
//                                                                            //
//    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 encoding and decoding functions for Aiken encoding
// of decimal digits. We also check that it is a complementary code and that
// it is a weighted 2-4-2-1 sum.
// ************************************************************************** //

macro EncodeAiken(d) = nat2bv((d<=4?d:d+6),4);
macro DecodeAiken(b) = bv2nat(b)-(b{3}?6:0);
macro BV(b) = (b?1:0);

module AikenCode(nat{10} ?x, bv{4} y) {
    loop {
        // first encode x
        y = EncodeAiken(x);
        // now check that decoding reveals x
        assert(x == DecodeAiken(y));
        // check complementarity of the code
        assert(9-x == DecodeAiken(!y));
        // check weighted sum
        assert(x == 2*BV(y{3}) + 4*BV(y{2}) + 2*BV(y{1}) + 1*BV(y{0}));
        pause;
    }
}
drivenby {
    // enumerate all bitvectors of specified size
    for(i=0..9) {
         x = i;
         pause;
    }
}