Use RipleLSB in PartitionedXOR, and invert outputs ls180-24jan2020
authorCesar Strauss <cestrauss@gmail.com>
Sat, 16 Jan 2021 20:37:35 +0000 (17:37 -0300)
committerCesar Strauss <cestrauss@gmail.com>
Sat, 16 Jan 2021 20:42:30 +0000 (17:42 -0300)
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.

src/ieee754/part/formal/proof_partition.py
src/ieee754/part_bits/xor.py

index 5867cdb..c818115 100644 (file)
@@ -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)
 
 
index c5471f5..02ace8d 100644 (file)
@@ -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