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