Use RipleLSB in PartitionedXOR, and invert outputs

The combiner was built to give inverted outputs, since it was designed
for ORing "not equals" signals, instead of ANDing equals signals.

Use 4-bit partitions when checking, 8-bit takes a long time for some
reason.

diff --git a/src/ieee754/part/formal/proof_partition.py b/src/ieee754/part/formal/proof_partition.py
index 5867cdb931f358d0ebe16fbbf4fc96bce26d27d3..c8181153289b945232746aa25dea9bd6980afeaf 100644 (file)
--- a/src/ieee754/part/formal/proof_partition.py
+++ b/src/ieee754/part/formal/proof_partition.py
@@ -568,7 +568,8 @@ class PartitionTestCase(FHDLTestCase):
         def op_xor(obj):
             return obj.xor()
 
-        module = ComparisonOpDriver(op_xor, nops=1)
+        # 8-bit partitions take a long time, for some reason
+        module = ComparisonOpDriver(op_xor, nops=1, width=32, mwidth=4)
         self.assertFormal(module, mode="bmc", depth=1)
 
 

diff --git a/src/ieee754/part_bits/xor.py b/src/ieee754/part_bits/xor.py
index c5471f51020aab84e5c3502dc9eeb76e886ee3d1..02ace8dbbbf8cc5d5e8c652afbe8de24a2d523a9 100644 (file)
--- a/src/ieee754/part_bits/xor.py
+++ b/src/ieee754/part_bits/xor.py
@@ -15,6 +15,7 @@ See:
 
 from nmigen import Signal, Module, Elaboratable, Cat, C, Mux, Repl
 from nmigen.cli import main
+from nmutil.ripple import RippleLSB
 
 from ieee754.part_mul_add.partpoints import PartitionPoints
 from ieee754.part_cmp.experiments.eq_combiner import XORCombiner
@@ -52,6 +53,10 @@ class PartitionedXOR(Elaboratable):
         # put the partial results through the combiner
         comb += xorc.gates.eq(self.partition_points.as_sig())
         comb += xorc.neqs.eq(xors)
-        comb += self.output.eq(xorc.outputs)
+
+        m.submodules.ripple = ripple = RippleLSB(self.mwidth)
+        comb += ripple.results_in.eq(xorc.outputs)
+        comb += ripple.gates.eq(self.partition_points.as_sig())
+        comb += self.output.eq(~ripple.output)
 
         return m