From 11e3f3eba7a589c61636ca0e4036be4ef294853a Mon Sep 17 00:00:00 2001 From: Cesar Strauss Date: Sat, 16 Jan 2021 17:37:35 -0300 Subject: [PATCH] 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. --- src/ieee754/part/formal/proof_partition.py | 3 ++- src/ieee754/part_bits/xor.py | 7 ++++++- 2 files changed, 8 insertions(+), 2 deletions(-) diff --git a/src/ieee754/part/formal/proof_partition.py b/src/ieee754/part/formal/proof_partition.py index 5867cdb9..c8181153 100644 --- 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 c5471f51..02ace8db 100644 --- 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 -- 2.30.2