add first cut at formal proof for PartitionedXOR

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()

diff --git a/src/ieee754/part/partsig.py b/src/ieee754/part/partsig.py
index 168a0e0b354836a21b3a028cf9cc28eb197e9a7d..d710b7ff186620dd60435fa4265bc27b5bd448f1 100644 (file)
--- a/src/ieee754/part/partsig.py
+++ b/src/ieee754/part/partsig.py
@@ -47,7 +47,7 @@ class PartitionedSignal:
         else:
             self.partpoints = make_partition(mask, width)
         self.modnames = {}
-        for name in ['add', 'eq', 'gt', 'ge', 'ls']:
+        for name in ['add', 'eq', 'gt', 'ge', 'ls', 'xor']:
             self.modnames[name] = 0
 
     def set_module(self, m):
@@ -304,9 +304,10 @@ class PartitionedSignal:
             ``1`` if an odd number of bits are set, ``0`` if an
                   even number of bits are set.
         """
+        width = len(self.sig)
         pa = PartitionedXOR(width, self.partpoints)
         setattr(self.m.submodules, self.get_modname("xor"), pa)
-        self.m.d.comb += pa.a.eq(self)
+        self.m.d.comb += pa.a.eq(self.sig)
         return pa.output
 
     def implies(premise, conclusion):