// ************************************************************************** //
//                                                                            //
//    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 Exzess3 encoding
// of decimal digits. We also check that it is a complementary code.
// ************************************************************************** //

macro EncodeExzess3(d) = nat2bv(d+3,4);
macro DecodeExzess3(b) = bv2nat(b)-3;

module Exzess3Code(nat{10} ?x, bv{4} y) {
    loop {
        // first encode x
        y = EncodeExzess3(x);
        // now check that decoding reveals x
        assert(x == DecodeExzess3(y));
        // check complementarity of the code
        assert(9-x == DecodeExzess3(!y));
        pause;
    }
}
drivenby {
    // enumerate all bitvectors of specified size
    for(i=0..9) {
         x = i;
         pause;
    }
}