add first cut at formal proof for PartitionedXOR

[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 a84a127b8d3e5f37c5193667ef56387ccdaa3386..5867cdb931f358d0ebe16fbbf4fc96bce26d27d3 100644 (file)
--- a/src/ieee754/part/formal/proof_partition.py
+++ b/src/ieee754/part/formal/proof_partition.py
@@ -563,6 +563,14 @@ class PartitionTestCase(FHDLTestCase):
         module = ComparisonOpDriver(op_any, nops=1)
         self.assertFormal(module, mode="bmc", depth=1)
 
+    def test_partsig_xor(self):
+
+        def op_xor(obj):
+            return obj.xor()
+
+        module = ComparisonOpDriver(op_xor, nops=1)
+        self.assertFormal(module, mode="bmc", depth=1)
+
 
 if __name__ == '__main__':
     unittest.main()