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 6d7b088ef146df7db96e33562625d2c12702f561..3ef53c35f09687ef4dbade911f3aea3e81433ebf 100644 (file)
--- 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)
 
         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()
 
 if __name__ == '__main__':
     unittest.main()

diff --git a/src/ieee754/part/partsig.py b/src/ieee754/part/partsig.py
index d710b7ff186620dd60435fa4265bc27b5bd448f1..3d3cd675dae4ea82248cdc4261d6a9cc030ad6ae 100644 (file)
--- 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):
     # 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
         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 8d9a179a66ebe04bf299b6211c23d188e52251fa..7d87eceebac77801362179bdb4a8ca50140ded55 100644 (file)
--- 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 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 = []
 
             def test_op(msg_prefix, carry, test_fn, mod_attr, *mask_list):
                 rand_data = []