src/ieee754/fpfma/test/test_fma_formal.py

   1 import unittest
   2 from nmutil.formaltest import FHDLTestCase
   3 from ieee754.fpfma.pipeline import FPFMABasePipe
   4 from nmigen.hdl.dsl import Module
   5 from nmigen.hdl.ast import Initial, Assert, AnyConst, Signal, Assume, Mux
   6 from nmigen.hdl.smtlib2 import SmtFloatingPoint, SmtSortFloatingPoint, \
   7     SmtSortFloat16, SmtSortFloat32, SmtSortFloat64, SmtBool, \
   8     SmtRoundingMode, ROUND_TOWARD_POSITIVE, ROUND_TOWARD_NEGATIVE, SmtBitVec
   9 from ieee754.fpcommon.fpbase import FPFormat, FPRoundingMode
  10 from ieee754.pipeline import PipelineSpec
  11 import os
  12
  13 ENABLE_FMA_F32_FORMAL = os.getenv("ENABLE_FMA_F32_FORMAL") is not None
  14
  15
  16 class TestFMAFormal(FHDLTestCase):
  17     @unittest.skip("not finished implementing")  # FIXME: remove skip
  18     def tst_fma_formal(self, sort, rm, negate_addend, negate_product):
  19         assert isinstance(sort, SmtSortFloatingPoint)
  20         assert isinstance(rm, FPRoundingMode)
  21         assert isinstance(negate_addend, bool)
  22         assert isinstance(negate_product, bool)
  23         width = sort.width
  24         pspec = PipelineSpec(width, id_width=4, n_ops=3)
  25         pspec.fpformat = FPFormat(e_width=sort.eb,
  26                                   m_width=sort.mantissa_field_width)
  27         dut = FPFMABasePipe(pspec)
  28         m = Module()
  29         m.submodules.dut = dut
  30         m.d.comb += dut.n.i_ready.eq(True)
  31         m.d.comb += dut.p.i_valid.eq(Initial())
  32         m.d.comb += dut.p.i_data.rm.eq(Mux(Initial(), rm, 0))
  33         out = Signal(width)
  34         out_full = Signal(reset=False)
  35         with m.If(dut.n.trigger):
  36             # check we only got output for one cycle
  37             m.d.comb += Assert(~out_full)
  38             m.d.sync += out.eq(dut.n.o_data.z)
  39             m.d.sync += out_full.eq(True)
  40         a = Signal(width)
  41         b = Signal(width)
  42         c = Signal(width)
  43         with m.If(Initial() | True):  # FIXME: remove | True
  44             m.d.comb += [
  45                 dut.p.i_data.a.eq(a),
  46                 dut.p.i_data.b.eq(b),
  47                 dut.p.i_data.c.eq(c),
  48                 dut.p.i_data.negate_addend.eq(negate_addend),
  49                 dut.p.i_data.negate_product.eq(negate_product),
  50             ]
  51
  52         def smt_op(a_fp, b_fp, c_fp, rm):
  53             assert isinstance(a_fp, SmtFloatingPoint)
  54             assert isinstance(b_fp, SmtFloatingPoint)
  55             assert isinstance(c_fp, SmtFloatingPoint)
  56             assert isinstance(rm, SmtRoundingMode)
  57             if negate_addend:
  58                 b_fp = -b_fp
  59             if negate_product:
  60                 a_fp = -a_fp
  61             return a_fp.fma(c_fp, b_fp, rm=rm)
  62         a_fp = SmtFloatingPoint.from_bits(a, sort=sort)
  63         b_fp = SmtFloatingPoint.from_bits(b, sort=sort)
  64         c_fp = SmtFloatingPoint.from_bits(c, sort=sort)
  65         out_fp = SmtFloatingPoint.from_bits(out, sort=sort)
  66         if rm in (FPRoundingMode.ROUND_TO_ODD_UNSIGNED_ZEROS_ARE_POSITIVE,
  67                   FPRoundingMode.ROUND_TO_ODD_UNSIGNED_ZEROS_ARE_NEGATIVE):
  68             rounded_up = Signal(width)
  69             m.d.comb += rounded_up.eq(AnyConst(width))
  70             rounded_up_fp = smt_op(a_fp, b_fp, c_fp, rm=ROUND_TOWARD_POSITIVE)
  71             rounded_down_fp = smt_op(a_fp, b_fp, c_fp,
  72                                      rm=ROUND_TOWARD_NEGATIVE)
  73             m.d.comb += Assume(SmtFloatingPoint.from_bits(
  74                 rounded_up, sort=sort).same(rounded_up_fp).as_value())
  75             use_rounded_up = SmtBool.make(rounded_up[0])
  76             if rm is FPRoundingMode.ROUND_TO_ODD_UNSIGNED_ZEROS_ARE_POSITIVE:
  77                 is_zero = rounded_up_fp.is_zero() & rounded_down_fp.is_zero()
  78                 use_rounded_up |= is_zero
  79             expected_fp = use_rounded_up.ite(rounded_up_fp, rounded_down_fp)
  80         else:
  81             smt_rm = SmtRoundingMode.make(rm.to_smtlib2())
  82             expected_fp = smt_op(a_fp, b_fp, c_fp, rm=smt_rm)
  83         expected = Signal(width)
  84         m.d.comb += expected.eq(AnyConst(width))
  85         quiet_bit = 1 << (sort.mantissa_field_width - 1)
  86         nan_exponent = ((1 << sort.eb) - 1) << sort.mantissa_field_width
  87         with m.If(expected_fp.is_nan().as_value()):
  88             with m.If(a_fp.is_nan().as_value()):
  89                 m.d.comb += Assume(expected == (a | quiet_bit))
  90             with m.Elif(b_fp.is_nan().as_value()):
  91                 m.d.comb += Assume(expected == (b | quiet_bit))
  92             with m.Elif(c_fp.is_nan().as_value()):
  93                 m.d.comb += Assume(expected == (c | quiet_bit))
  94             with m.Else():
  95                 m.d.comb += Assume(expected == (nan_exponent | quiet_bit))
  96         with m.Else():
  97             m.d.comb += Assume(SmtFloatingPoint.from_bits(expected, sort=sort)
  98                                .same(expected_fp).as_value())
  99         m.d.comb += a.eq(AnyConst(width))
 100         m.d.comb += b.eq(AnyConst(width))
 101         m.d.comb += c.eq(AnyConst(width))
 102         with m.If(out_full):
 103             m.d.comb += Assert(out_fp.same(expected_fp).as_value())
 104             m.d.comb += Assert(out == expected)
 105
 106         def fp_from_int(v):
 107             return SmtFloatingPoint.from_signed_bv(
 108                 SmtBitVec.make(v, width=128),
 109                 rm=ROUND_TOWARD_POSITIVE, sort=sort)
 110
 111         # FIXME: remove:
 112         if False:
 113             m.d.comb += Assume(a == 0x05C1)
 114             m.d.comb += Assume(b == 0x877F)
 115             m.d.comb += Assume(c == 0x7437)
 116             with m.If(out_full):
 117                 m.d.comb += Assert(out == 0x0000)
 118                 m.d.comb += Assert(out == 0x0001)
 119
 120         self.assertFormal(m, depth=5, solver="bitwuzla")
 121
 122     # FIXME: check exception flags
 123
 124     def test_fmadd_f16_rne_formal(self):
 125         self.tst_fma_formal(sort=SmtSortFloat16(), rm=FPRoundingMode.RNE,
 126                             negate_addend=False, negate_product=False)
 127
 128     def test_fmsub_f16_rne_formal(self):
 129         self.tst_fma_formal(sort=SmtSortFloat16(), rm=FPRoundingMode.RNE,
 130                             negate_addend=True, negate_product=False)
 131
 132     def test_fnmadd_f16_rne_formal(self):
 133         self.tst_fma_formal(sort=SmtSortFloat16(), rm=FPRoundingMode.RNE,
 134                             negate_addend=True, negate_product=True)
 135
 136     def test_fnmsub_f16_rne_formal(self):
 137         self.tst_fma_formal(sort=SmtSortFloat16(), rm=FPRoundingMode.RNE,
 138                             negate_addend=False, negate_product=True)
 139
 140     def test_fmadd_f16_rtz_formal(self):
 141         self.tst_fma_formal(sort=SmtSortFloat16(), rm=FPRoundingMode.RTZ,
 142                             negate_addend=False, negate_product=False)
 143
 144     def test_fmsub_f16_rtz_formal(self):
 145         self.tst_fma_formal(sort=SmtSortFloat16(), rm=FPRoundingMode.RTZ,
 146                             negate_addend=True, negate_product=False)
 147
 148     def test_fnmadd_f16_rtz_formal(self):
 149         self.tst_fma_formal(sort=SmtSortFloat16(), rm=FPRoundingMode.RTZ,
 150                             negate_addend=True, negate_product=True)
 151
 152     def test_fnmsub_f16_rtz_formal(self):
 153         self.tst_fma_formal(sort=SmtSortFloat16(), rm=FPRoundingMode.RTZ,
 154                             negate_addend=False, negate_product=True)
 155
 156     def test_fmadd_f16_rtp_formal(self):
 157         self.tst_fma_formal(sort=SmtSortFloat16(), rm=FPRoundingMode.RTP,
 158                             negate_addend=False, negate_product=False)
 159
 160     def test_fmsub_f16_rtp_formal(self):
 161         self.tst_fma_formal(sort=SmtSortFloat16(), rm=FPRoundingMode.RTP,
 162                             negate_addend=True, negate_product=False)
 163
 164     def test_fnmadd_f16_rtp_formal(self):
 165         self.tst_fma_formal(sort=SmtSortFloat16(), rm=FPRoundingMode.RTP,
 166                             negate_addend=True, negate_product=True)
 167
 168     def test_fnmsub_f16_rtp_formal(self):
 169         self.tst_fma_formal(sort=SmtSortFloat16(), rm=FPRoundingMode.RTP,
 170                             negate_addend=False, negate_product=True)
 171
 172     def test_fmadd_f16_rtn_formal(self):
 173         self.tst_fma_formal(sort=SmtSortFloat16(), rm=FPRoundingMode.RTN,
 174                             negate_addend=False, negate_product=False)
 175
 176     def test_fmsub_f16_rtn_formal(self):
 177         self.tst_fma_formal(sort=SmtSortFloat16(), rm=FPRoundingMode.RTN,
 178                             negate_addend=True, negate_product=False)
 179
 180     def test_fnmadd_f16_rtn_formal(self):
 181         self.tst_fma_formal(sort=SmtSortFloat16(), rm=FPRoundingMode.RTN,
 182                             negate_addend=True, negate_product=True)
 183
 184     def test_fnmsub_f16_rtn_formal(self):
 185         self.tst_fma_formal(sort=SmtSortFloat16(), rm=FPRoundingMode.RTN,
 186                             negate_addend=False, negate_product=True)
 187
 188     def test_fmadd_f16_rna_formal(self):
 189         self.tst_fma_formal(sort=SmtSortFloat16(), rm=FPRoundingMode.RNA,
 190                             negate_addend=False, negate_product=False)
 191
 192     def test_fmsub_f16_rna_formal(self):
 193         self.tst_fma_formal(sort=SmtSortFloat16(), rm=FPRoundingMode.RNA,
 194                             negate_addend=True, negate_product=False)
 195
 196     def test_fnmadd_f16_rna_formal(self):
 197         self.tst_fma_formal(sort=SmtSortFloat16(), rm=FPRoundingMode.RNA,
 198                             negate_addend=True, negate_product=True)
 199
 200     def test_fnmsub_f16_rna_formal(self):
 201         self.tst_fma_formal(sort=SmtSortFloat16(), rm=FPRoundingMode.RNA,
 202                             negate_addend=False, negate_product=True)
 203
 204     def test_fmadd_f16_rtop_formal(self):
 205         self.tst_fma_formal(sort=SmtSortFloat16(), rm=FPRoundingMode.RTOP,
 206                             negate_addend=False, negate_product=False)
 207
 208     def test_fmsub_f16_rtop_formal(self):
 209         self.tst_fma_formal(sort=SmtSortFloat16(), rm=FPRoundingMode.RTOP,
 210                             negate_addend=True, negate_product=False)
 211
 212     def test_fnmadd_f16_rtop_formal(self):
 213         self.tst_fma_formal(sort=SmtSortFloat16(), rm=FPRoundingMode.RTOP,
 214                             negate_addend=True, negate_product=True)
 215
 216     def test_fnmsub_f16_rtop_formal(self):
 217         self.tst_fma_formal(sort=SmtSortFloat16(), rm=FPRoundingMode.RTOP,
 218                             negate_addend=False, negate_product=True)
 219
 220     def test_fmadd_f16_rton_formal(self):
 221         self.tst_fma_formal(sort=SmtSortFloat16(), rm=FPRoundingMode.RTON,
 222                             negate_addend=False, negate_product=False)
 223
 224     def test_fmsub_f16_rton_formal(self):
 225         self.tst_fma_formal(sort=SmtSortFloat16(), rm=FPRoundingMode.RTON,
 226                             negate_addend=True, negate_product=False)
 227
 228     def test_fnmadd_f16_rton_formal(self):
 229         self.tst_fma_formal(sort=SmtSortFloat16(), rm=FPRoundingMode.RTON,
 230                             negate_addend=True, negate_product=True)
 231
 232     def test_fnmsub_f16_rton_formal(self):
 233         self.tst_fma_formal(sort=SmtSortFloat16(), rm=FPRoundingMode.RTON,
 234                             negate_addend=False, negate_product=True)
 235
 236     @unittest.skipUnless(ENABLE_FMA_F32_FORMAL,
 237                          "ENABLE_FMA_F32_FORMAL not in environ")
 238     def test_fmadd_f32_rne_formal(self):
 239         self.tst_fma_formal(sort=SmtSortFloat32(), rm=FPRoundingMode.RNE,
 240                             negate_addend=False, negate_product=False)
 241
 242     @unittest.skipUnless(ENABLE_FMA_F32_FORMAL,
 243                          "ENABLE_FMA_F32_FORMAL not in environ")
 244     def test_fmsub_f32_rne_formal(self):
 245         self.tst_fma_formal(sort=SmtSortFloat32(), rm=FPRoundingMode.RNE,
 246                             negate_addend=True, negate_product=False)
 247
 248     @unittest.skipUnless(ENABLE_FMA_F32_FORMAL,
 249                          "ENABLE_FMA_F32_FORMAL not in environ")
 250     def test_fnmadd_f32_rne_formal(self):
 251         self.tst_fma_formal(sort=SmtSortFloat32(), rm=FPRoundingMode.RNE,
 252                             negate_addend=True, negate_product=True)
 253
 254     @unittest.skipUnless(ENABLE_FMA_F32_FORMAL,
 255                          "ENABLE_FMA_F32_FORMAL not in environ")
 256     def test_fnmsub_f32_rne_formal(self):
 257         self.tst_fma_formal(sort=SmtSortFloat32(), rm=FPRoundingMode.RNE,
 258                             negate_addend=False, negate_product=True)
 259
 260     @unittest.skipUnless(ENABLE_FMA_F32_FORMAL,
 261                          "ENABLE_FMA_F32_FORMAL not in environ")
 262     def test_fmadd_f32_rtz_formal(self):
 263         self.tst_fma_formal(sort=SmtSortFloat32(), rm=FPRoundingMode.RTZ,
 264                             negate_addend=False, negate_product=False)
 265
 266     @unittest.skipUnless(ENABLE_FMA_F32_FORMAL,
 267                          "ENABLE_FMA_F32_FORMAL not in environ")
 268     def test_fmsub_f32_rtz_formal(self):
 269         self.tst_fma_formal(sort=SmtSortFloat32(), rm=FPRoundingMode.RTZ,
 270                             negate_addend=True, negate_product=False)
 271
 272     @unittest.skipUnless(ENABLE_FMA_F32_FORMAL,
 273                          "ENABLE_FMA_F32_FORMAL not in environ")
 274     def test_fnmadd_f32_rtz_formal(self):
 275         self.tst_fma_formal(sort=SmtSortFloat32(), rm=FPRoundingMode.RTZ,
 276                             negate_addend=True, negate_product=True)
 277
 278     @unittest.skipUnless(ENABLE_FMA_F32_FORMAL,
 279                          "ENABLE_FMA_F32_FORMAL not in environ")
 280     def test_fnmsub_f32_rtz_formal(self):
 281         self.tst_fma_formal(sort=SmtSortFloat32(), rm=FPRoundingMode.RTZ,
 282                             negate_addend=False, negate_product=True)
 283
 284     @unittest.skipUnless(ENABLE_FMA_F32_FORMAL,
 285                          "ENABLE_FMA_F32_FORMAL not in environ")
 286     def test_fmadd_f32_rtp_formal(self):
 287         self.tst_fma_formal(sort=SmtSortFloat32(), rm=FPRoundingMode.RTP,
 288                             negate_addend=False, negate_product=False)
 289
 290     @unittest.skipUnless(ENABLE_FMA_F32_FORMAL,
 291                          "ENABLE_FMA_F32_FORMAL not in environ")
 292     def test_fmsub_f32_rtp_formal(self):
 293         self.tst_fma_formal(sort=SmtSortFloat32(), rm=FPRoundingMode.RTP,
 294                             negate_addend=True, negate_product=False)
 295
 296     @unittest.skipUnless(ENABLE_FMA_F32_FORMAL,
 297                          "ENABLE_FMA_F32_FORMAL not in environ")
 298     def test_fnmadd_f32_rtp_formal(self):
 299         self.tst_fma_formal(sort=SmtSortFloat32(), rm=FPRoundingMode.RTP,
 300                             negate_addend=True, negate_product=True)
 301
 302     @unittest.skipUnless(ENABLE_FMA_F32_FORMAL,
 303                          "ENABLE_FMA_F32_FORMAL not in environ")
 304     def test_fnmsub_f32_rtp_formal(self):
 305         self.tst_fma_formal(sort=SmtSortFloat32(), rm=FPRoundingMode.RTP,
 306                             negate_addend=False, negate_product=True)
 307
 308     @unittest.skipUnless(ENABLE_FMA_F32_FORMAL,
 309                          "ENABLE_FMA_F32_FORMAL not in environ")
 310     def test_fmadd_f32_rtn_formal(self):
 311         self.tst_fma_formal(sort=SmtSortFloat32(), rm=FPRoundingMode.RTN,
 312                             negate_addend=False, negate_product=False)
 313
 314     @unittest.skipUnless(ENABLE_FMA_F32_FORMAL,
 315                          "ENABLE_FMA_F32_FORMAL not in environ")
 316     def test_fmsub_f32_rtn_formal(self):
 317         self.tst_fma_formal(sort=SmtSortFloat32(), rm=FPRoundingMode.RTN,
 318                             negate_addend=True, negate_product=False)
 319
 320     @unittest.skipUnless(ENABLE_FMA_F32_FORMAL,
 321                          "ENABLE_FMA_F32_FORMAL not in environ")
 322     def test_fnmadd_f32_rtn_formal(self):
 323         self.tst_fma_formal(sort=SmtSortFloat32(), rm=FPRoundingMode.RTN,
 324                             negate_addend=True, negate_product=True)
 325
 326     @unittest.skipUnless(ENABLE_FMA_F32_FORMAL,
 327                          "ENABLE_FMA_F32_FORMAL not in environ")
 328     def test_fnmsub_f32_rtn_formal(self):
 329         self.tst_fma_formal(sort=SmtSortFloat32(), rm=FPRoundingMode.RTN,
 330                             negate_addend=False, negate_product=True)
 331
 332     @unittest.skipUnless(ENABLE_FMA_F32_FORMAL,
 333                          "ENABLE_FMA_F32_FORMAL not in environ")
 334     def test_fmadd_f32_rna_formal(self):
 335         self.tst_fma_formal(sort=SmtSortFloat32(), rm=FPRoundingMode.RNA,
 336                             negate_addend=False, negate_product=False)
 337
 338     @unittest.skipUnless(ENABLE_FMA_F32_FORMAL,
 339                          "ENABLE_FMA_F32_FORMAL not in environ")
 340     def test_fmsub_f32_rna_formal(self):
 341         self.tst_fma_formal(sort=SmtSortFloat32(), rm=FPRoundingMode.RNA,
 342                             negate_addend=True, negate_product=False)
 343
 344     @unittest.skipUnless(ENABLE_FMA_F32_FORMAL,
 345                          "ENABLE_FMA_F32_FORMAL not in environ")
 346     def test_fnmadd_f32_rna_formal(self):
 347         self.tst_fma_formal(sort=SmtSortFloat32(), rm=FPRoundingMode.RNA,
 348                             negate_addend=True, negate_product=True)
 349
 350     @unittest.skipUnless(ENABLE_FMA_F32_FORMAL,
 351                          "ENABLE_FMA_F32_FORMAL not in environ")
 352     def test_fnmsub_f32_rna_formal(self):
 353         self.tst_fma_formal(sort=SmtSortFloat32(), rm=FPRoundingMode.RNA,
 354                             negate_addend=False, negate_product=True)
 355
 356     @unittest.skipUnless(ENABLE_FMA_F32_FORMAL,
 357                          "ENABLE_FMA_F32_FORMAL not in environ")
 358     def test_fmadd_f32_rtop_formal(self):
 359         self.tst_fma_formal(sort=SmtSortFloat32(), rm=FPRoundingMode.RTOP,
 360                             negate_addend=False, negate_product=False)
 361
 362     @unittest.skipUnless(ENABLE_FMA_F32_FORMAL,
 363                          "ENABLE_FMA_F32_FORMAL not in environ")
 364     def test_fmsub_f32_rtop_formal(self):
 365         self.tst_fma_formal(sort=SmtSortFloat32(), rm=FPRoundingMode.RTOP,
 366                             negate_addend=True, negate_product=False)
 367
 368     @unittest.skipUnless(ENABLE_FMA_F32_FORMAL,
 369                          "ENABLE_FMA_F32_FORMAL not in environ")
 370     def test_fnmadd_f32_rtop_formal(self):
 371         self.tst_fma_formal(sort=SmtSortFloat32(), rm=FPRoundingMode.RTOP,
 372                             negate_addend=True, negate_product=True)
 373
 374     @unittest.skipUnless(ENABLE_FMA_F32_FORMAL,
 375                          "ENABLE_FMA_F32_FORMAL not in environ")
 376     def test_fnmsub_f32_rtop_formal(self):
 377         self.tst_fma_formal(sort=SmtSortFloat32(), rm=FPRoundingMode.RTOP,
 378                             negate_addend=False, negate_product=True)
 379
 380     @unittest.skipUnless(ENABLE_FMA_F32_FORMAL,
 381                          "ENABLE_FMA_F32_FORMAL not in environ")
 382     def test_fmadd_f32_rton_formal(self):
 383         self.tst_fma_formal(sort=SmtSortFloat32(), rm=FPRoundingMode.RTON,
 384                             negate_addend=False, negate_product=False)
 385
 386     @unittest.skipUnless(ENABLE_FMA_F32_FORMAL,
 387                          "ENABLE_FMA_F32_FORMAL not in environ")
 388     def test_fmsub_f32_rton_formal(self):
 389         self.tst_fma_formal(sort=SmtSortFloat32(), rm=FPRoundingMode.RTON,
 390                             negate_addend=True, negate_product=False)
 391
 392     @unittest.skipUnless(ENABLE_FMA_F32_FORMAL,
 393                          "ENABLE_FMA_F32_FORMAL not in environ")
 394     def test_fnmadd_f32_rton_formal(self):
 395         self.tst_fma_formal(sort=SmtSortFloat32(), rm=FPRoundingMode.RTON,
 396                             negate_addend=True, negate_product=True)
 397
 398     @unittest.skipUnless(ENABLE_FMA_F32_FORMAL,
 399                          "ENABLE_FMA_F32_FORMAL not in environ")
 400     def test_fnmsub_f32_rton_formal(self):
 401         self.tst_fma_formal(sort=SmtSortFloat32(), rm=FPRoundingMode.RTON,
 402                             negate_addend=False, negate_product=True)
 403
 404     @unittest.skip("too slow")
 405     def test_fmadd_f64_rne_formal(self):
 406         self.tst_fma_formal(sort=SmtSortFloat64(), rm=FPRoundingMode.RNE,
 407                             negate_addend=False, negate_product=False)
 408
 409     @unittest.skip("too slow")
 410     def test_fmsub_f64_rne_formal(self):
 411         self.tst_fma_formal(sort=SmtSortFloat64(), rm=FPRoundingMode.RNE,
 412                             negate_addend=True, negate_product=False)
 413
 414     @unittest.skip("too slow")
 415     def test_fnmadd_f64_rne_formal(self):
 416         self.tst_fma_formal(sort=SmtSortFloat64(), rm=FPRoundingMode.RNE,
 417                             negate_addend=True, negate_product=True)
 418
 419     @unittest.skip("too slow")
 420     def test_fnmsub_f64_rne_formal(self):
 421         self.tst_fma_formal(sort=SmtSortFloat64(), rm=FPRoundingMode.RNE,
 422                             negate_addend=False, negate_product=True)
 423
 424     @unittest.skip("too slow")
 425     def test_fmadd_f64_rtz_formal(self):
 426         self.tst_fma_formal(sort=SmtSortFloat64(), rm=FPRoundingMode.RTZ,
 427                             negate_addend=False, negate_product=False)
 428
 429     @unittest.skip("too slow")
 430     def test_fmsub_f64_rtz_formal(self):
 431         self.tst_fma_formal(sort=SmtSortFloat64(), rm=FPRoundingMode.RTZ,
 432                             negate_addend=True, negate_product=False)
 433
 434     @unittest.skip("too slow")
 435     def test_fnmadd_f64_rtz_formal(self):
 436         self.tst_fma_formal(sort=SmtSortFloat64(), rm=FPRoundingMode.RTZ,
 437                             negate_addend=True, negate_product=True)
 438
 439     @unittest.skip("too slow")
 440     def test_fnmsub_f64_rtz_formal(self):
 441         self.tst_fma_formal(sort=SmtSortFloat64(), rm=FPRoundingMode.RTZ,
 442                             negate_addend=False, negate_product=True)
 443
 444     @unittest.skip("too slow")
 445     def test_fmadd_f64_rtp_formal(self):
 446         self.tst_fma_formal(sort=SmtSortFloat64(), rm=FPRoundingMode.RTP,
 447                             negate_addend=False, negate_product=False)
 448
 449     @unittest.skip("too slow")
 450     def test_fmsub_f64_rtp_formal(self):
 451         self.tst_fma_formal(sort=SmtSortFloat64(), rm=FPRoundingMode.RTP,
 452                             negate_addend=True, negate_product=False)
 453
 454     @unittest.skip("too slow")
 455     def test_fnmadd_f64_rtp_formal(self):
 456         self.tst_fma_formal(sort=SmtSortFloat64(), rm=FPRoundingMode.RTP,
 457                             negate_addend=True, negate_product=True)
 458
 459     @unittest.skip("too slow")
 460     def test_fnmsub_f64_rtp_formal(self):
 461         self.tst_fma_formal(sort=SmtSortFloat64(), rm=FPRoundingMode.RTP,
 462                             negate_addend=False, negate_product=True)
 463
 464     @unittest.skip("too slow")
 465     def test_fmadd_f64_rtn_formal(self):
 466         self.tst_fma_formal(sort=SmtSortFloat64(), rm=FPRoundingMode.RTN,
 467                             negate_addend=False, negate_product=False)
 468
 469     @unittest.skip("too slow")
 470     def test_fmsub_f64_rtn_formal(self):
 471         self.tst_fma_formal(sort=SmtSortFloat64(), rm=FPRoundingMode.RTN,
 472                             negate_addend=True, negate_product=False)
 473
 474     @unittest.skip("too slow")
 475     def test_fnmadd_f64_rtn_formal(self):
 476         self.tst_fma_formal(sort=SmtSortFloat64(), rm=FPRoundingMode.RTN,
 477                             negate_addend=True, negate_product=True)
 478
 479     @unittest.skip("too slow")
 480     def test_fnmsub_f64_rtn_formal(self):
 481         self.tst_fma_formal(sort=SmtSortFloat64(), rm=FPRoundingMode.RTN,
 482                             negate_addend=False, negate_product=True)
 483
 484     @unittest.skip("too slow")
 485     def test_fmadd_f64_rna_formal(self):
 486         self.tst_fma_formal(sort=SmtSortFloat64(), rm=FPRoundingMode.RNA,
 487                             negate_addend=False, negate_product=False)
 488
 489     @unittest.skip("too slow")
 490     def test_fmsub_f64_rna_formal(self):
 491         self.tst_fma_formal(sort=SmtSortFloat64(), rm=FPRoundingMode.RNA,
 492                             negate_addend=True, negate_product=False)
 493
 494     @unittest.skip("too slow")
 495     def test_fnmadd_f64_rna_formal(self):
 496         self.tst_fma_formal(sort=SmtSortFloat64(), rm=FPRoundingMode.RNA,
 497                             negate_addend=True, negate_product=True)
 498
 499     @unittest.skip("too slow")
 500     def test_fnmsub_f64_rna_formal(self):
 501         self.tst_fma_formal(sort=SmtSortFloat64(), rm=FPRoundingMode.RNA,
 502                             negate_addend=False, negate_product=True)
 503
 504     @unittest.skip("too slow")
 505     def test_fmadd_f64_rtop_formal(self):
 506         self.tst_fma_formal(sort=SmtSortFloat64(), rm=FPRoundingMode.RTOP,
 507                             negate_addend=False, negate_product=False)
 508
 509     @unittest.skip("too slow")
 510     def test_fmsub_f64_rtop_formal(self):
 511         self.tst_fma_formal(sort=SmtSortFloat64(), rm=FPRoundingMode.RTOP,
 512                             negate_addend=True, negate_product=False)
 513
 514     @unittest.skip("too slow")
 515     def test_fnmadd_f64_rtop_formal(self):
 516         self.tst_fma_formal(sort=SmtSortFloat64(), rm=FPRoundingMode.RTOP,
 517                             negate_addend=True, negate_product=True)
 518
 519     @unittest.skip("too slow")
 520     def test_fnmsub_f64_rtop_formal(self):
 521         self.tst_fma_formal(sort=SmtSortFloat64(), rm=FPRoundingMode.RTOP,
 522                             negate_addend=False, negate_product=True)
 523
 524     @unittest.skip("too slow")
 525     def test_fmadd_f64_rton_formal(self):
 526         self.tst_fma_formal(sort=SmtSortFloat64(), rm=FPRoundingMode.RTON,
 527                             negate_addend=False, negate_product=False)
 528
 529     @unittest.skip("too slow")
 530     def test_fmsub_f64_rton_formal(self):
 531         self.tst_fma_formal(sort=SmtSortFloat64(), rm=FPRoundingMode.RTON,
 532                             negate_addend=True, negate_product=False)
 533
 534     @unittest.skip("too slow")
 535     def test_fnmadd_f64_rton_formal(self):
 536         self.tst_fma_formal(sort=SmtSortFloat64(), rm=FPRoundingMode.RTON,
 537                             negate_addend=True, negate_product=True)
 538
 539     @unittest.skip("too slow")
 540     def test_fnmsub_f64_rton_formal(self):
 541         self.tst_fma_formal(sort=SmtSortFloat64(), rm=FPRoundingMode.RTON,
 542                             negate_addend=False, negate_product=True)
 543
 544     def test_all_rounding_modes_covered(self):
 545         for width in 16, 32, 64:
 546             for rm in FPRoundingMode:
 547                 rm_s = rm.name.lower()
 548                 name = f"test_fmadd_f{width}_{rm_s}_formal"
 549                 assert callable(getattr(self, name))
 550                 name = f"test_fmsub_f{width}_{rm_s}_formal"
 551                 assert callable(getattr(self, name))
 552                 name = f"test_fnmadd_f{width}_{rm_s}_formal"
 553                 assert callable(getattr(self, name))
 554                 name = f"test_fnmsub_f{width}_{rm_s}_formal"
 555                 assert callable(getattr(self, name))
 556
 557
 558 if __name__ == '__main__':
 559     unittest.main()