// ************************************************************************** // // // // 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; } }