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 fa5d73234ec44536b715ecfdafec426a48673b43..534e9e549d53cfc0bf4cb78f7093e62f5a9f1c36 100644 (file)
--- 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 fb06a1b9e0a625889db4ef5c15cb4145cf6da776..84a96188bdb31e0931c9e9afe55274a2e1c9d321 100644 (file)
--- 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