From 21f4a109ce102eb088f80a342a6ddc91f294c955 Mon Sep 17 00:00:00 2001 From: Cesar Strauss Date: Sat, 23 Jan 2021 17:39:49 -0300 Subject: [PATCH] Return a PartitionedSignal from the bitwise "not" operation Adjust the proof to accommodate such operations. --- src/ieee754/part/formal/proof_partition.py | 7 ++++++- src/ieee754/part/partsig.py | 4 +++- 2 files changed, 9 insertions(+), 2 deletions(-) diff --git a/src/ieee754/part/formal/proof_partition.py b/src/ieee754/part/formal/proof_partition.py index fa5d7323..534e9e54 100644 --- a/src/ieee754/part/formal/proof_partition.py +++ b/src/ieee754/part/formal/proof_partition.py @@ -358,7 +358,12 @@ class OpDriver(Elaboratable): out_step = step output = Signal(out_width) # perform the operation on the partitioned signals - comb += output.eq(self.op(*operands)) + result = self.op(*operands) + if isinstance(result, PartitionedSignal): + comb += output.eq(result.sig) + # TODO: remove when all operations return PartitionedSignal + else: + comb += output.eq(result) # instantiate the partitioned gate generator and connect the gates m.submodules.gen = gen = GateGenerator(mwidth) comb += gates.eq(gen.gates) diff --git a/src/ieee754/part/partsig.py b/src/ieee754/part/partsig.py index fb06a1b9..84a96188 100644 --- a/src/ieee754/part/partsig.py +++ b/src/ieee754/part/partsig.py @@ -71,7 +71,9 @@ class PartitionedSignal: # unary ops that do not require partitioning def __invert__(self): - return ~self.sig + result = PartitionedSignal.like(self) + self.m.d.comb += result.sig.eq(~self.sig) + return result # unary ops that require partitioning -- 2.30.2