// ************************************************************************** //
//                                                                            //
//    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 example is taken from [Ried04], where the 7-segment display is encoded//
// as follows:                                                                //
//        c                                                                   //
//       ---                                                                  //
//      |   |                                                                 //
//    a |   |f                                                                //
//      | d |                                                                 //
//       ---                                                                  //
//      |   |                                                                 //
//    b |   |g                                                                //
//      | e |                                                                 //
//       ---                                                                  //
//                                                                            //
// Hence, the display should produce the following outputs (note the unusual  //
// digits 6 and 9):                                                           //
//                                                                            //
//    Digit   x3 x2 x1 x0  abcdefg                                            //
//        0   0  0  0  0   1110111                                            //
//        1   0  0  0  1   0000011                                            //
//        2   0  0  1  0   0111110                                            //
//        3   0  0  1  1   0011111                                            //
//        4   0  1  0  0   1001011                                            //
//        5   0  1  0  1   1011101                                            //
//        6   0  1  1  0   1101101                                            //
//        7   0  1  1  1   0010011                                            //
//        8   1  0  0  0   1111111                                            //
//        9   1  0  0  1   1011011                                            //
//                                                                            //
// ************************************************************************** //

module Segment7(event ?x3,?x2,?x1,?x0,a,b,c,d,e,f,g) {
    always{
        // the following is given in Ried04, but it does not stabelize for digits 0 and 2
//         a = !x0 & !x3 & !c | !x1 & c;
//         b = !x0 & e;
//         c = !x3 & x2 & x0 | !x2 & (!x1 & x3 | e);
//         d = a & (x2 | x3) | e & x1;
//         e = !x2 & (!x0 | x1) & f | !(x3 | f);
//         f = (!x2 | !(x1 | x0)) & g | !x3 & !a;
//         g = !x3 & !b | a;
        // the following modification stabelizes for all digits
         a = !x0 & !x3 & !c | !x1 & c;
         b = !x0 & e;
         c = !x3 & x2 & x0 | !x2 & (!x1 & x3 | e);
         d = a & (x2 | x3) | e & x1;
         e = !x2 & (!x0 | x1) & (f | !x3) | !(x3 | f);
         f = (!x2 | !(x1 | x0)) & g | !x3 & !a;
         g = !x3 & !b | a;
        // this is the specification of the 7-segment display in minimal DNF
        assert(a <-> (!x3 & x2 & !x1 | !x1 & !x0 | x3 & !x2 | x2 & !x0 | x3 & x1));
        assert(b <-> (x1 & !x0 | x3 & x1 | x3 & x2 | !x2 & !x0));
        assert(c <-> (x3 | !x2 & !x0 | x2 & x0 | !x2 & x1));
        assert(d <-> (!x3 & x2 & !x1 | x3 & !x2 | x1 & !x0 | !x2 & x1 | x3 & x0));
        assert(e <-> (!x3 & x2 & !x1 & x0 | !x2 & !x1 & !x0 | !x3 & x1 & !x0 | !x3 & !x2 & x1));
        assert(f <-> (!x3 & !x1 & !x0 | x3 & !x1 & x0 | !x3 & x1 & x0 | !x2 & !x0 | !x3 & !x2));
        assert(g <-> (!x3 & !x1 | x3 & !x2 | !x3 & x2 | !x1 & x0 | !x3 & x0));
    }
}
drivenby {
    bv{4} w;
    for(i=0..9) {
        pause;
        w = nat2bv(i,4);
        x0 = w{0};
        x1 = w{1};
        x2 = w{2};
        x3 = w{3};
    }
}