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)
-        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),
@@ -103,20 +103,6 @@ class TestFMAFormal(FHDLTestCase):
             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

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)
 
 
-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.
@@ -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.
-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.
-EXPANDED_MANTISSA_EXTRA_MSBS = 16  # FIXME: change back to 2
+EXPANDED_MANTISSA_EXTRA_MSBS = 1
 
 
 def expanded_mantissa_shape(fpformat):