From: Cesar Strauss <cestrauss@gmail.com>
Date: Sat, 23 Jan 2021 20:39:49 +0000 (-0300)
Subject: Return a PartitionedSignal from the bitwise "not" operation
X-Git-Url: https://git.libre-soc.org/?p=ieee754fpu.git;a=commitdiff_plain;h=21f4a109ce102eb088f80a342a6ddc91f294c955

Return a PartitionedSignal from the bitwise "not" operation

Adjust the proof to accommodate such operations.
---

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