add first cut at formal proof for PartitionedXOR
authorLuke Kenneth Casson Leighton <lkcl@lkcl.net>
Sat, 16 Jan 2021 19:07:41 +0000 (19:07 +0000)
committerLuke Kenneth Casson Leighton <lkcl@lkcl.net>
Sat, 16 Jan 2021 19:07:41 +0000 (19:07 +0000)
src/ieee754/part/formal/proof_partition.py
src/ieee754/part/partsig.py

index a84a127..5867cdb 100644 (file)
@@ -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()
index 168a0e0..d710b7f 100644 (file)
@@ -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):