From: Cesar Strauss <cestrauss@gmail.com>
Date: Wed, 20 Jan 2021 10:35:01 +0000 (-0300)
Subject: Add tests for bitwise logical operators
X-Git-Url: https://git.libre-soc.org/?p=ieee754fpu.git;a=commitdiff_plain;h=55da2d5af83c90b3c6ac3d9bcec704501bf70dc5

Add tests for bitwise logical operators
---

diff --git a/src/ieee754/part/formal/proof_partition.py b/src/ieee754/part/formal/proof_partition.py
index 3ef53c35..6bf39351 100644
--- 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()