// **************************************************************************
//
//    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
//
// **************************************************************************
//
//  Check bitwise Boolean operations.
//
//  Reference:  http://en.wikipedia.org/wiki/Boolean_algebra
//
// **************************************************************************

module BitwiseOperations(bv{4} x,y,z) {
   nothing;
} satisfies {
  // Involution
  invol: assert !!x == x;

  // Idempotency
  idem0: assert (x & x) == x;
  idem1: assert (x | x) == x;

  // Absorption
  absorp0: assert (x & (x | y)) == x;
  absorp1: assert (x | (x & y)) == x;

  // Commutativity
  comm0: assert (x & y) == (y & x);
  comm1: assert (x | y) == (y | x);

  // Associativity
  assoc0: assert ((x & y) & z) == (x & (y & z));
  assoc1: assert ((x | y) | z) == (x | (y | z));

  // Distributivity
  dist0: assert (x & (y | z)) == ((x & y) | (x & z));
  dist1: assert (x | (y & z)) == ((x | y) & (x | z));

  // De Morgan
  demorg0: assert !(x & y) == (!x | !y);
  demorg1: assert !(x | y) == (!x & !y);

  // Complement
  comp2: assert (x & !x) == 0b0000;
  comp3: assert (x | !x) == 0b1111;

  // Boundedness
  bound0: assert (x & 0b0000) == 0b0000;
  bound1: assert (x | 0b0000) == x;
  bound2: assert (x & 0b1111) == x;
  bound3: assert (x | 0b1111) == 0b1111;
}