From: Luke Kenneth Casson Leighton <lkcl@lkcl.net>
Date: Sat, 16 Jan 2021 19:07:41 +0000 (+0000)
Subject: add first cut at formal proof for PartitionedXOR
X-Git-Tag: ls180-24jan2020~1
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=25a26dd9a82267e94f6af3a84964f7e4f5eaa03f;p=ieee754fpu.git

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 a84a127b..5867cdb9 100644
--- 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 168a0e0b..d710b7ff 100644
--- 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):