From: Cesar Strauss Date: Sat, 16 Jan 2021 20:37:35 +0000 (-0300) Subject: Use RipleLSB in PartitionedXOR, and invert outputs X-Git-Tag: ls180-24jan2020 X-Git-Url: https://git.libre-soc.org/?p=ieee754fpu.git;a=commitdiff_plain;h=11e3f3eba7a589c61636ca0e4036be4ef294853a 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 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