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