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