// ************************************************************************** //
//                                                                            //
//    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 Gray encoding of//
// bitvectors of arbitrary length "Length". The encoding can be done by a     //
// simple macro, while decoding requires a generic xor-expression that is     //
// computed in a for-loop with the local boolean array z.                     //
// ************************************************************************** //

macro Length = 8;

macro EncodeGray(b) = (false@b{-1:1} xor b);

module GrayCode(bv{Length} ?x,y) {
    [Length]bool z;
    loop {
        // first encode x
        y = EncodeGray(x);
        // now decode y
        for(i=0..Length-1)
            let(s=sum(j=i..Length-1) (y{j}?1:0))
            z[i] = s %2 == 1;
        // and assert that x and z are the same
        // note that bitvectors are enumerated b{n}..b{0} while arrays are
        // enumerated a[0..n]
        assert(reverse(x) == arr2bv(z));
        pause;
    }
}
drivenby {
    // enumerate all bitvectors of specified size
    for(i=0..exp(2,Length)-1) {
         x = nat2bv(i,Length);
         pause;
    }
}