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_F16_FORMAL = os.getenv("ENABLE_FMA_F16_FORMAL") is not None
  14 ENABLE_FMA_F32_FORMAL = os.getenv("ENABLE_FMA_F32_FORMAL") is not None
  15
  16
  17 class TestFMAFormal(FHDLTestCase):
  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_f8_rne_formal(self):
 125         self.tst_fma_formal(sort=SmtSortFloatingPoint(eb=5, sb=3),
 126                             rm=FPRoundingMode.RNE,
 127                             negate_addend=False, negate_product=False)
 128
 129     def test_fmsub_f8_rne_formal(self):
 130         self.tst_fma_formal(sort=SmtSortFloatingPoint(eb=5, sb=3),
 131                             rm=FPRoundingMode.RNE,
 132                             negate_addend=True, negate_product=False)
 133
 134     def test_fnmadd_f8_rne_formal(self):
 135         self.tst_fma_formal(sort=SmtSortFloatingPoint(eb=5, sb=3),
 136                             rm=FPRoundingMode.RNE,
 137                             negate_addend=True, negate_product=True)
 138
 139     def test_fnmsub_f8_rne_formal(self):
 140         self.tst_fma_formal(sort=SmtSortFloatingPoint(eb=5, sb=3),
 141                             rm=FPRoundingMode.RNE,
 142                             negate_addend=False, negate_product=True)
 143
 144     def test_fmadd_f8_rtz_formal(self):
 145         self.tst_fma_formal(sort=SmtSortFloatingPoint(eb=5, sb=3),
 146                             rm=FPRoundingMode.RTZ,
 147                             negate_addend=False, negate_product=False)
 148
 149     def test_fmsub_f8_rtz_formal(self):
 150         self.tst_fma_formal(sort=SmtSortFloatingPoint(eb=5, sb=3),
 151                             rm=FPRoundingMode.RTZ,
 152                             negate_addend=True, negate_product=False)
 153
 154     def test_fnmadd_f8_rtz_formal(self):
 155         self.tst_fma_formal(sort=SmtSortFloatingPoint(eb=5, sb=3),
 156                             rm=FPRoundingMode.RTZ,
 157                             negate_addend=True, negate_product=True)
 158
 159     def test_fnmsub_f8_rtz_formal(self):
 160         self.tst_fma_formal(sort=SmtSortFloatingPoint(eb=5, sb=3),
 161                             rm=FPRoundingMode.RTZ,
 162                             negate_addend=False, negate_product=True)
 163
 164     def test_fmadd_f8_rtp_formal(self):
 165         self.tst_fma_formal(sort=SmtSortFloatingPoint(eb=5, sb=3),
 166                             rm=FPRoundingMode.RTP,
 167                             negate_addend=False, negate_product=False)
 168
 169     def test_fmsub_f8_rtp_formal(self):
 170         self.tst_fma_formal(sort=SmtSortFloatingPoint(eb=5, sb=3),
 171                             rm=FPRoundingMode.RTP,
 172                             negate_addend=True, negate_product=False)
 173
 174     def test_fnmadd_f8_rtp_formal(self):
 175         self.tst_fma_formal(sort=SmtSortFloatingPoint(eb=5, sb=3),
 176                             rm=FPRoundingMode.RTP,
 177                             negate_addend=True, negate_product=True)
 178
 179     def test_fnmsub_f8_rtp_formal(self):
 180         self.tst_fma_formal(sort=SmtSortFloatingPoint(eb=5, sb=3),
 181                             rm=FPRoundingMode.RTP,
 182                             negate_addend=False, negate_product=True)
 183
 184     def test_fmadd_f8_rtn_formal(self):
 185         self.tst_fma_formal(sort=SmtSortFloatingPoint(eb=5, sb=3),
 186                             rm=FPRoundingMode.RTN,
 187                             negate_addend=False, negate_product=False)
 188
 189     def test_fmsub_f8_rtn_formal(self):
 190         self.tst_fma_formal(sort=SmtSortFloatingPoint(eb=5, sb=3),
 191                             rm=FPRoundingMode.RTN,
 192                             negate_addend=True, negate_product=False)
 193
 194     def test_fnmadd_f8_rtn_formal(self):
 195         self.tst_fma_formal(sort=SmtSortFloatingPoint(eb=5, sb=3),
 196                             rm=FPRoundingMode.RTN,
 197                             negate_addend=True, negate_product=True)
 198
 199     def test_fnmsub_f8_rtn_formal(self):
 200         self.tst_fma_formal(sort=SmtSortFloatingPoint(eb=5, sb=3),
 201                             rm=FPRoundingMode.RTN,
 202                             negate_addend=False, negate_product=True)
 203
 204     def test_fmadd_f8_rna_formal(self):
 205         self.tst_fma_formal(sort=SmtSortFloatingPoint(eb=5, sb=3),
 206                             rm=FPRoundingMode.RNA,
 207                             negate_addend=False, negate_product=False)
 208
 209     def test_fmsub_f8_rna_formal(self):
 210         self.tst_fma_formal(sort=SmtSortFloatingPoint(eb=5, sb=3),
 211                             rm=FPRoundingMode.RNA,
 212                             negate_addend=True, negate_product=False)
 213
 214     def test_fnmadd_f8_rna_formal(self):
 215         self.tst_fma_formal(sort=SmtSortFloatingPoint(eb=5, sb=3),
 216                             rm=FPRoundingMode.RNA,
 217                             negate_addend=True, negate_product=True)
 218
 219     def test_fnmsub_f8_rna_formal(self):
 220         self.tst_fma_formal(sort=SmtSortFloatingPoint(eb=5, sb=3),
 221                             rm=FPRoundingMode.RNA,
 222                             negate_addend=False, negate_product=True)
 223
 224     def test_fmadd_f8_rtop_formal(self):
 225         self.tst_fma_formal(sort=SmtSortFloatingPoint(eb=5, sb=3),
 226                             rm=FPRoundingMode.RTOP,
 227                             negate_addend=False, negate_product=False)
 228
 229     def test_fmsub_f8_rtop_formal(self):
 230         self.tst_fma_formal(sort=SmtSortFloatingPoint(eb=5, sb=3),
 231                             rm=FPRoundingMode.RTOP,
 232                             negate_addend=True, negate_product=False)
 233
 234     def test_fnmadd_f8_rtop_formal(self):
 235         self.tst_fma_formal(sort=SmtSortFloatingPoint(eb=5, sb=3),
 236                             rm=FPRoundingMode.RTOP,
 237                             negate_addend=True, negate_product=True)
 238
 239     def test_fnmsub_f8_rtop_formal(self):
 240         self.tst_fma_formal(sort=SmtSortFloatingPoint(eb=5, sb=3),
 241                             rm=FPRoundingMode.RTOP,
 242                             negate_addend=False, negate_product=True)
 243
 244     def test_fmadd_f8_rton_formal(self):
 245         self.tst_fma_formal(sort=SmtSortFloatingPoint(eb=5, sb=3),
 246                             rm=FPRoundingMode.RTON,
 247                             negate_addend=False, negate_product=False)
 248
 249     def test_fmsub_f8_rton_formal(self):
 250         self.tst_fma_formal(sort=SmtSortFloatingPoint(eb=5, sb=3),
 251                             rm=FPRoundingMode.RTON,
 252                             negate_addend=True, negate_product=False)
 253
 254     def test_fnmadd_f8_rton_formal(self):
 255         self.tst_fma_formal(sort=SmtSortFloatingPoint(eb=5, sb=3),
 256                             rm=FPRoundingMode.RTON,
 257                             negate_addend=True, negate_product=True)
 258
 259     def test_fnmsub_f8_rton_formal(self):
 260         self.tst_fma_formal(sort=SmtSortFloatingPoint(eb=5, sb=3),
 261                             rm=FPRoundingMode.RTON,
 262                             negate_addend=False, negate_product=True)
 263
 264     @unittest.skipUnless(ENABLE_FMA_F16_FORMAL,
 265                          "ENABLE_FMA_F16_FORMAL not in environ")
 266     def test_fmadd_f16_rne_formal(self):
 267         self.tst_fma_formal(sort=SmtSortFloat16(), rm=FPRoundingMode.RNE,
 268                             negate_addend=False, negate_product=False)
 269
 270     @unittest.skipUnless(ENABLE_FMA_F16_FORMAL,
 271                          "ENABLE_FMA_F16_FORMAL not in environ")
 272     def test_fmsub_f16_rne_formal(self):
 273         self.tst_fma_formal(sort=SmtSortFloat16(), rm=FPRoundingMode.RNE,
 274                             negate_addend=True, negate_product=False)
 275
 276     @unittest.skipUnless(ENABLE_FMA_F16_FORMAL,
 277                          "ENABLE_FMA_F16_FORMAL not in environ")
 278     def test_fnmadd_f16_rne_formal(self):
 279         self.tst_fma_formal(sort=SmtSortFloat16(), rm=FPRoundingMode.RNE,
 280                             negate_addend=True, negate_product=True)
 281
 282     @unittest.skipUnless(ENABLE_FMA_F16_FORMAL,
 283                          "ENABLE_FMA_F16_FORMAL not in environ")
 284     def test_fnmsub_f16_rne_formal(self):
 285         self.tst_fma_formal(sort=SmtSortFloat16(), rm=FPRoundingMode.RNE,
 286                             negate_addend=False, negate_product=True)
 287
 288     @unittest.skipUnless(ENABLE_FMA_F16_FORMAL,
 289                          "ENABLE_FMA_F16_FORMAL not in environ")
 290     def test_fmadd_f16_rtz_formal(self):
 291         self.tst_fma_formal(sort=SmtSortFloat16(), rm=FPRoundingMode.RTZ,
 292                             negate_addend=False, negate_product=False)
 293
 294     @unittest.skipUnless(ENABLE_FMA_F16_FORMAL,
 295                          "ENABLE_FMA_F16_FORMAL not in environ")
 296     def test_fmsub_f16_rtz_formal(self):
 297         self.tst_fma_formal(sort=SmtSortFloat16(), rm=FPRoundingMode.RTZ,
 298                             negate_addend=True, negate_product=False)
 299
 300     @unittest.skipUnless(ENABLE_FMA_F16_FORMAL,
 301                          "ENABLE_FMA_F16_FORMAL not in environ")
 302     def test_fnmadd_f16_rtz_formal(self):
 303         self.tst_fma_formal(sort=SmtSortFloat16(), rm=FPRoundingMode.RTZ,
 304                             negate_addend=True, negate_product=True)
 305
 306     @unittest.skipUnless(ENABLE_FMA_F16_FORMAL,
 307                          "ENABLE_FMA_F16_FORMAL not in environ")
 308     def test_fnmsub_f16_rtz_formal(self):
 309         self.tst_fma_formal(sort=SmtSortFloat16(), rm=FPRoundingMode.RTZ,
 310                             negate_addend=False, negate_product=True)
 311
 312     @unittest.skipUnless(ENABLE_FMA_F16_FORMAL,
 313                          "ENABLE_FMA_F16_FORMAL not in environ")
 314     def test_fmadd_f16_rtp_formal(self):
 315         self.tst_fma_formal(sort=SmtSortFloat16(), rm=FPRoundingMode.RTP,
 316                             negate_addend=False, negate_product=False)
 317
 318     @unittest.skipUnless(ENABLE_FMA_F16_FORMAL,
 319                          "ENABLE_FMA_F16_FORMAL not in environ")
 320     def test_fmsub_f16_rtp_formal(self):
 321         self.tst_fma_formal(sort=SmtSortFloat16(), rm=FPRoundingMode.RTP,
 322                             negate_addend=True, negate_product=False)
 323
 324     @unittest.skipUnless(ENABLE_FMA_F16_FORMAL,
 325                          "ENABLE_FMA_F16_FORMAL not in environ")
 326     def test_fnmadd_f16_rtp_formal(self):
 327         self.tst_fma_formal(sort=SmtSortFloat16(), rm=FPRoundingMode.RTP,
 328                             negate_addend=True, negate_product=True)
 329
 330     @unittest.skipUnless(ENABLE_FMA_F16_FORMAL,
 331                          "ENABLE_FMA_F16_FORMAL not in environ")
 332     def test_fnmsub_f16_rtp_formal(self):
 333         self.tst_fma_formal(sort=SmtSortFloat16(), rm=FPRoundingMode.RTP,
 334                             negate_addend=False, negate_product=True)
 335
 336     @unittest.skipUnless(ENABLE_FMA_F16_FORMAL,
 337                          "ENABLE_FMA_F16_FORMAL not in environ")
 338     def test_fmadd_f16_rtn_formal(self):
 339         self.tst_fma_formal(sort=SmtSortFloat16(), rm=FPRoundingMode.RTN,
 340                             negate_addend=False, negate_product=False)
 341
 342     @unittest.skipUnless(ENABLE_FMA_F16_FORMAL,
 343                          "ENABLE_FMA_F16_FORMAL not in environ")
 344     def test_fmsub_f16_rtn_formal(self):
 345         self.tst_fma_formal(sort=SmtSortFloat16(), rm=FPRoundingMode.RTN,
 346                             negate_addend=True, negate_product=False)
 347
 348     @unittest.skipUnless(ENABLE_FMA_F16_FORMAL,
 349                          "ENABLE_FMA_F16_FORMAL not in environ")
 350     def test_fnmadd_f16_rtn_formal(self):
 351         self.tst_fma_formal(sort=SmtSortFloat16(), rm=FPRoundingMode.RTN,
 352                             negate_addend=True, negate_product=True)
 353
 354     @unittest.skipUnless(ENABLE_FMA_F16_FORMAL,
 355                          "ENABLE_FMA_F16_FORMAL not in environ")
 356     def test_fnmsub_f16_rtn_formal(self):
 357         self.tst_fma_formal(sort=SmtSortFloat16(), rm=FPRoundingMode.RTN,
 358                             negate_addend=False, negate_product=True)
 359
 360     @unittest.skipUnless(ENABLE_FMA_F16_FORMAL,
 361                          "ENABLE_FMA_F16_FORMAL not in environ")
 362     def test_fmadd_f16_rna_formal(self):
 363         self.tst_fma_formal(sort=SmtSortFloat16(), rm=FPRoundingMode.RNA,
 364                             negate_addend=False, negate_product=False)
 365
 366     @unittest.skipUnless(ENABLE_FMA_F16_FORMAL,
 367                          "ENABLE_FMA_F16_FORMAL not in environ")
 368     def test_fmsub_f16_rna_formal(self):
 369         self.tst_fma_formal(sort=SmtSortFloat16(), rm=FPRoundingMode.RNA,
 370                             negate_addend=True, negate_product=False)
 371
 372     @unittest.skipUnless(ENABLE_FMA_F16_FORMAL,
 373                          "ENABLE_FMA_F16_FORMAL not in environ")
 374     def test_fnmadd_f16_rna_formal(self):
 375         self.tst_fma_formal(sort=SmtSortFloat16(), rm=FPRoundingMode.RNA,
 376                             negate_addend=True, negate_product=True)
 377
 378     @unittest.skipUnless(ENABLE_FMA_F16_FORMAL,
 379                          "ENABLE_FMA_F16_FORMAL not in environ")
 380     def test_fnmsub_f16_rna_formal(self):
 381         self.tst_fma_formal(sort=SmtSortFloat16(), rm=FPRoundingMode.RNA,
 382                             negate_addend=False, negate_product=True)
 383
 384     @unittest.skipUnless(ENABLE_FMA_F16_FORMAL,
 385                          "ENABLE_FMA_F16_FORMAL not in environ")
 386     def test_fmadd_f16_rtop_formal(self):
 387         self.tst_fma_formal(sort=SmtSortFloat16(), rm=FPRoundingMode.RTOP,
 388                             negate_addend=False, negate_product=False)
 389
 390     @unittest.skipUnless(ENABLE_FMA_F16_FORMAL,
 391                          "ENABLE_FMA_F16_FORMAL not in environ")
 392     def test_fmsub_f16_rtop_formal(self):
 393         self.tst_fma_formal(sort=SmtSortFloat16(), rm=FPRoundingMode.RTOP,
 394                             negate_addend=True, negate_product=False)
 395
 396     @unittest.skipUnless(ENABLE_FMA_F16_FORMAL,
 397                          "ENABLE_FMA_F16_FORMAL not in environ")
 398     def test_fnmadd_f16_rtop_formal(self):
 399         self.tst_fma_formal(sort=SmtSortFloat16(), rm=FPRoundingMode.RTOP,
 400                             negate_addend=True, negate_product=True)
 401
 402     @unittest.skipUnless(ENABLE_FMA_F16_FORMAL,
 403                          "ENABLE_FMA_F16_FORMAL not in environ")
 404     def test_fnmsub_f16_rtop_formal(self):
 405         self.tst_fma_formal(sort=SmtSortFloat16(), rm=FPRoundingMode.RTOP,
 406                             negate_addend=False, negate_product=True)
 407
 408     @unittest.skipUnless(ENABLE_FMA_F16_FORMAL,
 409                          "ENABLE_FMA_F16_FORMAL not in environ")
 410     def test_fmadd_f16_rton_formal(self):
 411         self.tst_fma_formal(sort=SmtSortFloat16(), rm=FPRoundingMode.RTON,
 412                             negate_addend=False, negate_product=False)
 413
 414     @unittest.skipUnless(ENABLE_FMA_F16_FORMAL,
 415                          "ENABLE_FMA_F16_FORMAL not in environ")
 416     def test_fmsub_f16_rton_formal(self):
 417         self.tst_fma_formal(sort=SmtSortFloat16(), rm=FPRoundingMode.RTON,
 418                             negate_addend=True, negate_product=False)
 419
 420     @unittest.skipUnless(ENABLE_FMA_F16_FORMAL,
 421                          "ENABLE_FMA_F16_FORMAL not in environ")
 422     def test_fnmadd_f16_rton_formal(self):
 423         self.tst_fma_formal(sort=SmtSortFloat16(), rm=FPRoundingMode.RTON,
 424                             negate_addend=True, negate_product=True)
 425
 426     @unittest.skipUnless(ENABLE_FMA_F16_FORMAL,
 427                          "ENABLE_FMA_F16_FORMAL not in environ")
 428     def test_fnmsub_f16_rton_formal(self):
 429         self.tst_fma_formal(sort=SmtSortFloat16(), rm=FPRoundingMode.RTON,
 430                             negate_addend=False, negate_product=True)
 431
 432     @unittest.skipUnless(ENABLE_FMA_F32_FORMAL,
 433                          "ENABLE_FMA_F32_FORMAL not in environ")
 434     def test_fmadd_f32_rne_formal(self):
 435         self.tst_fma_formal(sort=SmtSortFloat32(), rm=FPRoundingMode.RNE,
 436                             negate_addend=False, negate_product=False)
 437
 438     @unittest.skipUnless(ENABLE_FMA_F32_FORMAL,
 439                          "ENABLE_FMA_F32_FORMAL not in environ")
 440     def test_fmsub_f32_rne_formal(self):
 441         self.tst_fma_formal(sort=SmtSortFloat32(), rm=FPRoundingMode.RNE,
 442                             negate_addend=True, negate_product=False)
 443
 444     @unittest.skipUnless(ENABLE_FMA_F32_FORMAL,
 445                          "ENABLE_FMA_F32_FORMAL not in environ")
 446     def test_fnmadd_f32_rne_formal(self):
 447         self.tst_fma_formal(sort=SmtSortFloat32(), rm=FPRoundingMode.RNE,
 448                             negate_addend=True, negate_product=True)
 449
 450     @unittest.skipUnless(ENABLE_FMA_F32_FORMAL,
 451                          "ENABLE_FMA_F32_FORMAL not in environ")
 452     def test_fnmsub_f32_rne_formal(self):
 453         self.tst_fma_formal(sort=SmtSortFloat32(), rm=FPRoundingMode.RNE,
 454                             negate_addend=False, negate_product=True)
 455
 456     @unittest.skipUnless(ENABLE_FMA_F32_FORMAL,
 457                          "ENABLE_FMA_F32_FORMAL not in environ")
 458     def test_fmadd_f32_rtz_formal(self):
 459         self.tst_fma_formal(sort=SmtSortFloat32(), rm=FPRoundingMode.RTZ,
 460                             negate_addend=False, negate_product=False)
 461
 462     @unittest.skipUnless(ENABLE_FMA_F32_FORMAL,
 463                          "ENABLE_FMA_F32_FORMAL not in environ")
 464     def test_fmsub_f32_rtz_formal(self):
 465         self.tst_fma_formal(sort=SmtSortFloat32(), rm=FPRoundingMode.RTZ,
 466                             negate_addend=True, negate_product=False)
 467
 468     @unittest.skipUnless(ENABLE_FMA_F32_FORMAL,
 469                          "ENABLE_FMA_F32_FORMAL not in environ")
 470     def test_fnmadd_f32_rtz_formal(self):
 471         self.tst_fma_formal(sort=SmtSortFloat32(), rm=FPRoundingMode.RTZ,
 472                             negate_addend=True, negate_product=True)
 473
 474     @unittest.skipUnless(ENABLE_FMA_F32_FORMAL,
 475                          "ENABLE_FMA_F32_FORMAL not in environ")
 476     def test_fnmsub_f32_rtz_formal(self):
 477         self.tst_fma_formal(sort=SmtSortFloat32(), rm=FPRoundingMode.RTZ,
 478                             negate_addend=False, negate_product=True)
 479
 480     @unittest.skipUnless(ENABLE_FMA_F32_FORMAL,
 481                          "ENABLE_FMA_F32_FORMAL not in environ")
 482     def test_fmadd_f32_rtp_formal(self):
 483         self.tst_fma_formal(sort=SmtSortFloat32(), rm=FPRoundingMode.RTP,
 484                             negate_addend=False, negate_product=False)
 485
 486     @unittest.skipUnless(ENABLE_FMA_F32_FORMAL,
 487                          "ENABLE_FMA_F32_FORMAL not in environ")
 488     def test_fmsub_f32_rtp_formal(self):
 489         self.tst_fma_formal(sort=SmtSortFloat32(), rm=FPRoundingMode.RTP,
 490                             negate_addend=True, negate_product=False)
 491
 492     @unittest.skipUnless(ENABLE_FMA_F32_FORMAL,
 493                          "ENABLE_FMA_F32_FORMAL not in environ")
 494     def test_fnmadd_f32_rtp_formal(self):
 495         self.tst_fma_formal(sort=SmtSortFloat32(), rm=FPRoundingMode.RTP,
 496                             negate_addend=True, negate_product=True)
 497
 498     @unittest.skipUnless(ENABLE_FMA_F32_FORMAL,
 499                          "ENABLE_FMA_F32_FORMAL not in environ")
 500     def test_fnmsub_f32_rtp_formal(self):
 501         self.tst_fma_formal(sort=SmtSortFloat32(), rm=FPRoundingMode.RTP,
 502                             negate_addend=False, negate_product=True)
 503
 504     @unittest.skipUnless(ENABLE_FMA_F32_FORMAL,
 505                          "ENABLE_FMA_F32_FORMAL not in environ")
 506     def test_fmadd_f32_rtn_formal(self):
 507         self.tst_fma_formal(sort=SmtSortFloat32(), rm=FPRoundingMode.RTN,
 508                             negate_addend=False, negate_product=False)
 509
 510     @unittest.skipUnless(ENABLE_FMA_F32_FORMAL,
 511                          "ENABLE_FMA_F32_FORMAL not in environ")
 512     def test_fmsub_f32_rtn_formal(self):
 513         self.tst_fma_formal(sort=SmtSortFloat32(), rm=FPRoundingMode.RTN,
 514                             negate_addend=True, negate_product=False)
 515
 516     @unittest.skipUnless(ENABLE_FMA_F32_FORMAL,
 517                          "ENABLE_FMA_F32_FORMAL not in environ")
 518     def test_fnmadd_f32_rtn_formal(self):
 519         self.tst_fma_formal(sort=SmtSortFloat32(), rm=FPRoundingMode.RTN,
 520                             negate_addend=True, negate_product=True)
 521
 522     @unittest.skipUnless(ENABLE_FMA_F32_FORMAL,
 523                          "ENABLE_FMA_F32_FORMAL not in environ")
 524     def test_fnmsub_f32_rtn_formal(self):
 525         self.tst_fma_formal(sort=SmtSortFloat32(), rm=FPRoundingMode.RTN,
 526                             negate_addend=False, negate_product=True)
 527
 528     @unittest.skipUnless(ENABLE_FMA_F32_FORMAL,
 529                          "ENABLE_FMA_F32_FORMAL not in environ")
 530     def test_fmadd_f32_rna_formal(self):
 531         self.tst_fma_formal(sort=SmtSortFloat32(), rm=FPRoundingMode.RNA,
 532                             negate_addend=False, negate_product=False)
 533
 534     @unittest.skipUnless(ENABLE_FMA_F32_FORMAL,
 535                          "ENABLE_FMA_F32_FORMAL not in environ")
 536     def test_fmsub_f32_rna_formal(self):
 537         self.tst_fma_formal(sort=SmtSortFloat32(), rm=FPRoundingMode.RNA,
 538                             negate_addend=True, negate_product=False)
 539
 540     @unittest.skipUnless(ENABLE_FMA_F32_FORMAL,
 541                          "ENABLE_FMA_F32_FORMAL not in environ")
 542     def test_fnmadd_f32_rna_formal(self):
 543         self.tst_fma_formal(sort=SmtSortFloat32(), rm=FPRoundingMode.RNA,
 544                             negate_addend=True, negate_product=True)
 545
 546     @unittest.skipUnless(ENABLE_FMA_F32_FORMAL,
 547                          "ENABLE_FMA_F32_FORMAL not in environ")
 548     def test_fnmsub_f32_rna_formal(self):
 549         self.tst_fma_formal(sort=SmtSortFloat32(), rm=FPRoundingMode.RNA,
 550                             negate_addend=False, negate_product=True)
 551
 552     @unittest.skipUnless(ENABLE_FMA_F32_FORMAL,
 553                          "ENABLE_FMA_F32_FORMAL not in environ")
 554     def test_fmadd_f32_rtop_formal(self):
 555         self.tst_fma_formal(sort=SmtSortFloat32(), rm=FPRoundingMode.RTOP,
 556                             negate_addend=False, negate_product=False)
 557
 558     @unittest.skipUnless(ENABLE_FMA_F32_FORMAL,
 559                          "ENABLE_FMA_F32_FORMAL not in environ")
 560     def test_fmsub_f32_rtop_formal(self):
 561         self.tst_fma_formal(sort=SmtSortFloat32(), rm=FPRoundingMode.RTOP,
 562                             negate_addend=True, negate_product=False)
 563
 564     @unittest.skipUnless(ENABLE_FMA_F32_FORMAL,
 565                          "ENABLE_FMA_F32_FORMAL not in environ")
 566     def test_fnmadd_f32_rtop_formal(self):
 567         self.tst_fma_formal(sort=SmtSortFloat32(), rm=FPRoundingMode.RTOP,
 568                             negate_addend=True, negate_product=True)
 569
 570     @unittest.skipUnless(ENABLE_FMA_F32_FORMAL,
 571                          "ENABLE_FMA_F32_FORMAL not in environ")
 572     def test_fnmsub_f32_rtop_formal(self):
 573         self.tst_fma_formal(sort=SmtSortFloat32(), rm=FPRoundingMode.RTOP,
 574                             negate_addend=False, negate_product=True)
 575
 576     @unittest.skipUnless(ENABLE_FMA_F32_FORMAL,
 577                          "ENABLE_FMA_F32_FORMAL not in environ")
 578     def test_fmadd_f32_rton_formal(self):
 579         self.tst_fma_formal(sort=SmtSortFloat32(), rm=FPRoundingMode.RTON,
 580                             negate_addend=False, negate_product=False)
 581
 582     @unittest.skipUnless(ENABLE_FMA_F32_FORMAL,
 583                          "ENABLE_FMA_F32_FORMAL not in environ")
 584     def test_fmsub_f32_rton_formal(self):
 585         self.tst_fma_formal(sort=SmtSortFloat32(), rm=FPRoundingMode.RTON,
 586                             negate_addend=True, negate_product=False)
 587
 588     @unittest.skipUnless(ENABLE_FMA_F32_FORMAL,
 589                          "ENABLE_FMA_F32_FORMAL not in environ")
 590     def test_fnmadd_f32_rton_formal(self):
 591         self.tst_fma_formal(sort=SmtSortFloat32(), rm=FPRoundingMode.RTON,
 592                             negate_addend=True, negate_product=True)
 593
 594     @unittest.skipUnless(ENABLE_FMA_F32_FORMAL,
 595                          "ENABLE_FMA_F32_FORMAL not in environ")
 596     def test_fnmsub_f32_rton_formal(self):
 597         self.tst_fma_formal(sort=SmtSortFloat32(), rm=FPRoundingMode.RTON,
 598                             negate_addend=False, negate_product=True)
 599
 600     @unittest.skip("too slow")
 601     def test_fmadd_f64_rne_formal(self):
 602         self.tst_fma_formal(sort=SmtSortFloat64(), rm=FPRoundingMode.RNE,
 603                             negate_addend=False, negate_product=False)
 604
 605     @unittest.skip("too slow")
 606     def test_fmsub_f64_rne_formal(self):
 607         self.tst_fma_formal(sort=SmtSortFloat64(), rm=FPRoundingMode.RNE,
 608                             negate_addend=True, negate_product=False)
 609
 610     @unittest.skip("too slow")
 611     def test_fnmadd_f64_rne_formal(self):
 612         self.tst_fma_formal(sort=SmtSortFloat64(), rm=FPRoundingMode.RNE,
 613                             negate_addend=True, negate_product=True)
 614
 615     @unittest.skip("too slow")
 616     def test_fnmsub_f64_rne_formal(self):
 617         self.tst_fma_formal(sort=SmtSortFloat64(), rm=FPRoundingMode.RNE,
 618                             negate_addend=False, negate_product=True)
 619
 620     @unittest.skip("too slow")
 621     def test_fmadd_f64_rtz_formal(self):
 622         self.tst_fma_formal(sort=SmtSortFloat64(), rm=FPRoundingMode.RTZ,
 623                             negate_addend=False, negate_product=False)
 624
 625     @unittest.skip("too slow")
 626     def test_fmsub_f64_rtz_formal(self):
 627         self.tst_fma_formal(sort=SmtSortFloat64(), rm=FPRoundingMode.RTZ,
 628                             negate_addend=True, negate_product=False)
 629
 630     @unittest.skip("too slow")
 631     def test_fnmadd_f64_rtz_formal(self):
 632         self.tst_fma_formal(sort=SmtSortFloat64(), rm=FPRoundingMode.RTZ,
 633                             negate_addend=True, negate_product=True)
 634
 635     @unittest.skip("too slow")
 636     def test_fnmsub_f64_rtz_formal(self):
 637         self.tst_fma_formal(sort=SmtSortFloat64(), rm=FPRoundingMode.RTZ,
 638                             negate_addend=False, negate_product=True)
 639
 640     @unittest.skip("too slow")
 641     def test_fmadd_f64_rtp_formal(self):
 642         self.tst_fma_formal(sort=SmtSortFloat64(), rm=FPRoundingMode.RTP,
 643                             negate_addend=False, negate_product=False)
 644
 645     @unittest.skip("too slow")
 646     def test_fmsub_f64_rtp_formal(self):
 647         self.tst_fma_formal(sort=SmtSortFloat64(), rm=FPRoundingMode.RTP,
 648                             negate_addend=True, negate_product=False)
 649
 650     @unittest.skip("too slow")
 651     def test_fnmadd_f64_rtp_formal(self):
 652         self.tst_fma_formal(sort=SmtSortFloat64(), rm=FPRoundingMode.RTP,
 653                             negate_addend=True, negate_product=True)
 654
 655     @unittest.skip("too slow")
 656     def test_fnmsub_f64_rtp_formal(self):
 657         self.tst_fma_formal(sort=SmtSortFloat64(), rm=FPRoundingMode.RTP,
 658                             negate_addend=False, negate_product=True)
 659
 660     @unittest.skip("too slow")
 661     def test_fmadd_f64_rtn_formal(self):
 662         self.tst_fma_formal(sort=SmtSortFloat64(), rm=FPRoundingMode.RTN,
 663                             negate_addend=False, negate_product=False)
 664
 665     @unittest.skip("too slow")
 666     def test_fmsub_f64_rtn_formal(self):
 667         self.tst_fma_formal(sort=SmtSortFloat64(), rm=FPRoundingMode.RTN,
 668                             negate_addend=True, negate_product=False)
 669
 670     @unittest.skip("too slow")
 671     def test_fnmadd_f64_rtn_formal(self):
 672         self.tst_fma_formal(sort=SmtSortFloat64(), rm=FPRoundingMode.RTN,
 673                             negate_addend=True, negate_product=True)
 674
 675     @unittest.skip("too slow")
 676     def test_fnmsub_f64_rtn_formal(self):
 677         self.tst_fma_formal(sort=SmtSortFloat64(), rm=FPRoundingMode.RTN,
 678                             negate_addend=False, negate_product=True)
 679
 680     @unittest.skip("too slow")
 681     def test_fmadd_f64_rna_formal(self):
 682         self.tst_fma_formal(sort=SmtSortFloat64(), rm=FPRoundingMode.RNA,
 683                             negate_addend=False, negate_product=False)
 684
 685     @unittest.skip("too slow")
 686     def test_fmsub_f64_rna_formal(self):
 687         self.tst_fma_formal(sort=SmtSortFloat64(), rm=FPRoundingMode.RNA,
 688                             negate_addend=True, negate_product=False)
 689
 690     @unittest.skip("too slow")
 691     def test_fnmadd_f64_rna_formal(self):
 692         self.tst_fma_formal(sort=SmtSortFloat64(), rm=FPRoundingMode.RNA,
 693                             negate_addend=True, negate_product=True)
 694
 695     @unittest.skip("too slow")
 696     def test_fnmsub_f64_rna_formal(self):
 697         self.tst_fma_formal(sort=SmtSortFloat64(), rm=FPRoundingMode.RNA,
 698                             negate_addend=False, negate_product=True)
 699
 700     @unittest.skip("too slow")
 701     def test_fmadd_f64_rtop_formal(self):
 702         self.tst_fma_formal(sort=SmtSortFloat64(), rm=FPRoundingMode.RTOP,
 703                             negate_addend=False, negate_product=False)
 704
 705     @unittest.skip("too slow")
 706     def test_fmsub_f64_rtop_formal(self):
 707         self.tst_fma_formal(sort=SmtSortFloat64(), rm=FPRoundingMode.RTOP,
 708                             negate_addend=True, negate_product=False)
 709
 710     @unittest.skip("too slow")
 711     def test_fnmadd_f64_rtop_formal(self):
 712         self.tst_fma_formal(sort=SmtSortFloat64(), rm=FPRoundingMode.RTOP,
 713                             negate_addend=True, negate_product=True)
 714
 715     @unittest.skip("too slow")
 716     def test_fnmsub_f64_rtop_formal(self):
 717         self.tst_fma_formal(sort=SmtSortFloat64(), rm=FPRoundingMode.RTOP,
 718                             negate_addend=False, negate_product=True)
 719
 720     @unittest.skip("too slow")
 721     def test_fmadd_f64_rton_formal(self):
 722         self.tst_fma_formal(sort=SmtSortFloat64(), rm=FPRoundingMode.RTON,
 723                             negate_addend=False, negate_product=False)
 724
 725     @unittest.skip("too slow")
 726     def test_fmsub_f64_rton_formal(self):
 727         self.tst_fma_formal(sort=SmtSortFloat64(), rm=FPRoundingMode.RTON,
 728                             negate_addend=True, negate_product=False)
 729
 730     @unittest.skip("too slow")
 731     def test_fnmadd_f64_rton_formal(self):
 732         self.tst_fma_formal(sort=SmtSortFloat64(), rm=FPRoundingMode.RTON,
 733                             negate_addend=True, negate_product=True)
 734
 735     @unittest.skip("too slow")
 736     def test_fnmsub_f64_rton_formal(self):
 737         self.tst_fma_formal(sort=SmtSortFloat64(), rm=FPRoundingMode.RTON,
 738                             negate_addend=False, negate_product=True)
 739
 740     def test_all_rounding_modes_covered(self):
 741         for width in 8, 16, 32, 64:
 742             for rm in FPRoundingMode:
 743                 rm_s = rm.name.lower()
 744                 name = f"test_fmadd_f{width}_{rm_s}_formal"
 745                 assert callable(getattr(self, name))
 746                 name = f"test_fmsub_f{width}_{rm_s}_formal"
 747                 assert callable(getattr(self, name))
 748                 name = f"test_fnmadd_f{width}_{rm_s}_formal"
 749                 assert callable(getattr(self, name))
 750                 name = f"test_fnmsub_f{width}_{rm_s}_formal"
 751                 assert callable(getattr(self, name))
 752
 753
 754 if __name__ == '__main__':
 755     unittest.main()