From: Cesar Strauss 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 = []