Add tests for bitwise logical operators

[ieee754fpu.git] / src / ieee754 / part / formal / proof_partition.py

diff --git a/src/ieee754/part/formal/proof_partition.py b/src/ieee754/part/formal/proof_partition.py
index 3ef53c35f09687ef4dbade911f3aea3e81433ebf..6bf39351dcec61ef14a0132d079284c2be6bafdd 100644 (file)
--- a/src/ieee754/part/formal/proof_partition.py
+++ b/src/ieee754/part/formal/proof_partition.py
@@ -656,6 +656,31 @@ class PartitionTestCase(FHDLTestCase):
         module = OpDriver(operator.neg, nops=1, part_out=False)
         self.assertFormal(module, mode="bmc", depth=1)
 
+    def test_partsig_and(self):
+        module = OpDriver(operator.and_, part_out=False)
+        self.assertFormal(module, mode="bmc", depth=1)
+
+    def test_partsig_or(self):
+        module = OpDriver(operator.or_, part_out=False)
+        self.assertFormal(module, mode="bmc", depth=1)
+
+    def test_partsig_logical_xor(self):
+        module = OpDriver(operator.xor, part_out=False)
+        self.assertFormal(module, mode="bmc", depth=1)
+
+    def test_partsig_not(self):
+        module = OpDriver(operator.inv, nops=1, part_out=False)
+        self.assertFormal(module, mode="bmc", depth=1)
+
+    def test_partsig_implies(self):
+
+        def op_implies(a, b):
+            return a.implies(b)
+
+        # 8 x 8-bit partitions take a long time, for some reason
+        module = OpDriver(op_implies, part_out=False, width=32, mwidth=8)
+        self.assertFormal(module, mode="bmc", depth=1)
+
 
 if __name__ == '__main__':
     unittest.main()