// ************************************************************************** //
//                                                                            //
//    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 Generator = 0b10011;
macro InputSize = 9;
macro FrameSize = sizeOf(Generator)-1;

module CRC(bv{InputSize} ?x, bv{FrameSize} y, bool okay, event !rdy) {
    bv{FrameSize+1} u;
    bv{FrameSize} f;
    loop {
        u = x{InputSize-1:InputSize-FrameSize-1};
        for(i=0..InputSize-FrameSize-2) {
            if(u{-1})
                next(u) = (u xor Generator){FrameSize-1:0}@x{InputSize-FrameSize-2-i};
            else
                next(u) = u{FrameSize-1:0}@x{InputSize-FrameSize-2-i};
            pause;
        }
        emit(rdy);
        // determine the correct frame: should be 
            if(u{-1})
                f = (u xor Generator){FrameSize-1:0};
            else
                f = u{FrameSize-1:0};
        okay = (f=={false::FrameSize});
        pause;
    }
}
drivenby d1 {
    x = 0b110011101;
    await(rdy);
}
// test with wrong code word; f will contain the
drivenby d2 {
    x = 0b110010000;
    await(rdy);
}