From: Cesar Strauss <cestrauss@gmail.com>
Date: Sun, 17 Jan 2021 21:45:47 +0000 (-0300)
Subject: Fix PartitionedSignal.neg and its test case
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=15ba1ebff6dc8e1991118d9064338717ab582749;p=ieee754fpu.git

Fix PartitionedSignal.neg and its test case

For some reason, neg(a) was returning (a - 1) instead of (-a).
Implemented it as (0 - a).
For the test case, shifted down the input, negated it and shifted it
back again. Could have done it also by (0 - a), but this way it is more
independent of the implementation.
Added a formal proof.
---

diff --git a/src/ieee754/part/formal/proof_partition.py b/src/ieee754/part/formal/proof_partition.py
index 6d7b088e..3ef53c35 100644
--- a/src/ieee754/part/formal/proof_partition.py
+++ b/src/ieee754/part/formal/proof_partition.py
@@ -626,6 +626,36 @@ class PartitionTestCase(FHDLTestCase):
         module = OpDriver(operator.sub, part_out=False)
         self.assertFormal(module, mode="bmc", depth=1)
 
+    def test_partsig_neg(self):
+        style = {
+            'dec': {'base': 'dec'},
+            'bin': {'base': 'bin'}
+        }
+        traces = [
+            ('p_offset[2:0]', 'dec'),
+            ('p_width[3:0]', 'dec'),
+            ('p_gates[8:0]', 'bin'),
+            'i_1[63:0]',
+            ('add_1', {'submodule': 'add_1'}, [
+                ('gates[6:0]', 'bin'),
+                'a[63:0]', 'b[63:0]',
+                'output[63:0]']),
+            'p_1[63:0]',
+            'p_output[63:0]',
+            't3_1[23:0]',
+            'expected_3[23:0]']
+        write_gtkw(
+            'proof_partsig_neg_bmc.gtkw',
+            os.path.dirname(__file__) +
+            '/proof_partition_partsig_neg/engine_0/trace.vcd',
+            traces, style,
+            module='top',
+            zoom=-3
+        )
+
+        module = OpDriver(operator.neg, nops=1, part_out=False)
+        self.assertFormal(module, mode="bmc", depth=1)
+
 
 if __name__ == '__main__':
     unittest.main()
diff --git a/src/ieee754/part/partsig.py b/src/ieee754/part/partsig.py
index d710b7ff..3d3cd675 100644
--- a/src/ieee754/part/partsig.py
+++ b/src/ieee754/part/partsig.py
@@ -68,8 +68,8 @@ class PartitionedSignal:
     # unary ops that require partitioning
 
     def __neg__(self):
-        z = Const(0, len(self.partpoints)+1)
-        result, _ = self.add_op(self, ~0, carry=z)  # TODO, subop
+        z = Const(0, len(self.sig))
+        result, _ = self.sub_op(z, self)
         return result
 
     # binary ops that don't require partitioning
diff --git a/src/ieee754/part/test/test_partsig.py b/src/ieee754/part/test/test_partsig.py
index 8d9a179a..7d87ecee 100644
--- a/src/ieee754/part/test/test_partsig.py
+++ b/src/ieee754/part/test/test_partsig.py
@@ -280,7 +280,10 @@ class TestPartitionPoints(unittest.TestCase):
                 return result, carry
 
             def test_neg_fn(carry_in, a, b, mask):
-                return test_add_fn(0, a, ~0, mask)
+                lsb = mask & ~(mask - 1)  # has only LSB of mask set
+                pos = lsb.bit_length() - 1  # find bit position
+                a = (a & mask) >> pos  # shift it to the beginning
+                return ((-a) << pos) & mask, 0  # negate and shift it back
 
             def test_op(msg_prefix, carry, test_fn, mod_attr, *mask_list):
                 rand_data = []