clean up remaining fixmes for fma

diff --git a/src/ieee754/fpfma/test/test_fma_formal.py b/src/ieee754/fpfma/test/test_fma_formal.py
index bb437d2d3c8c00843ea2df76964f3d396f84858f..0ee68e37d1dbd980f3a135efb920efc87ed6473f 100644 (file)
--- a/src/ieee754/fpfma/test/test_fma_formal.py
+++ b/src/ieee754/fpfma/test/test_fma_formal.py
@@ -40,7 +40,7 @@ class TestFMAFormal(FHDLTestCase):
         a = Signal(width)
         b = Signal(width)
         c = Signal(width)
         a = Signal(width)
         b = Signal(width)
         c = Signal(width)

-        with m.If(Initial() | True):  # FIXME: remove | True
+        with m.If(Initial()):

             m.d.comb += [
                 dut.p.i_data.a.eq(a),
                 dut.p.i_data.b.eq(b),
             m.d.comb += [
                 dut.p.i_data.a.eq(a),
                 dut.p.i_data.b.eq(b),


@@ -103,20 +103,6 @@ class TestFMAFormal(FHDLTestCase):
             m.d.comb += Assert(out_fp.same(expected_fp).as_value())
             m.d.comb += Assert(out == expected)
 
             m.d.comb += Assert(out_fp.same(expected_fp).as_value())
             m.d.comb += Assert(out == expected)
 

-        def fp_from_int(v):
-            return SmtFloatingPoint.from_signed_bv(
-                SmtBitVec.make(v, width=128),
-                rm=ROUND_TOWARD_POSITIVE, sort=sort)
-
-        # FIXME: remove:
-        if False:
-            m.d.comb += Assume(a == 0x05C1)
-            m.d.comb += Assume(b == 0x877F)
-            m.d.comb += Assume(c == 0x7437)
-            with m.If(out_full):
-                m.d.comb += Assert(out == 0x0000)
-                m.d.comb += Assert(out == 0x0001)
-

         self.assertFormal(m, depth=5, solver="bitwuzla")
 
     # FIXME: check exception flags
         self.assertFormal(m, depth=5, solver="bitwuzla")
 
     # FIXME: check exception flags

diff --git a/src/ieee754/fpfma/util.py b/src/ieee754/fpfma/util.py
index 5f2ec62906872703894242de95777019cbf46e02..da3bfeea7fbdac205a650120d24cfd51bf8caec3 100644 (file)
--- a/src/ieee754/fpfma/util.py
+++ b/src/ieee754/fpfma/util.py
@@ -7,7 +7,7 @@ def expanded_exponent_shape(fpformat):
     return signed(fpformat.e_width + 3)
 
 
     return signed(fpformat.e_width + 3)
 
 

-EXPANDED_MANTISSA_SPACE_BETWEEN_SUM_PROD = 16  # FIXME: change back to 3
+EXPANDED_MANTISSA_SPACE_BETWEEN_SUM_PROD = 2

 r""" the number of bits of space between the lsb of a large addend and the msb
 of the product of two small factors to guarantee that the product ends up
 entirely in the sticky bit.
 r""" the number of bits of space between the lsb of a large addend and the msb
 of the product of two small factors to guarantee that the product ends up
 entirely in the sticky bit.


@@ -35,12 +35,12 @@ less hardware)
 
 # the number of extra LSBs needed by the expanded mantissa to avoid
 # having a tiny addend conflict with the lsb of the product.
 
 # the number of extra LSBs needed by the expanded mantissa to avoid
 # having a tiny addend conflict with the lsb of the product.

-EXPANDED_MANTISSA_EXTRA_LSBS = 16  # FIXME: change back to 2
+EXPANDED_MANTISSA_EXTRA_LSBS = 3

 
 
 # the number of extra MSBs needed by the expanded mantissa to avoid
 # overflowing. 2 bits -- 1 bit for carry out of addition, 1 bit for sign.
 
 
 # the number of extra MSBs needed by the expanded mantissa to avoid
 # overflowing. 2 bits -- 1 bit for carry out of addition, 1 bit for sign.

-EXPANDED_MANTISSA_EXTRA_MSBS = 16  # FIXME: change back to 2
+EXPANDED_MANTISSA_EXTRA_MSBS = 1

 
 
 def expanded_mantissa_shape(fpformat):
 
 
 def expanded_mantissa_shape(fpformat):