src/ieee754/fpadd/test/test_add_formal.py

   1 import unittest
   2 from nmutil.formaltest import FHDLTestCase
   3 from ieee754.fpadd.pipeline import FPADDBasePipe
   4 from nmigen.hdl.dsl import Module
   5 from nmigen.hdl.ast import AnySeq, Assert, AnyConst, Signal, Assume
   6 from nmigen.hdl.smtlib2 import (SmtFloatingPoint, SmtSortFloat16,
   7                                 ROUND_NEAREST_TIES_TO_EVEN)
   8 from ieee754.pipeline import PipelineSpec
   9
  10
  11 class TestFAdd16Formal(FHDLTestCase):
  12     def test_fadd16_rne_formal(self):
  13         dut = FPADDBasePipe(PipelineSpec(width=16, id_width=4))
  14         m = Module()
  15         m.submodules.dut = dut
  16         m.d.comb += dut.n.i_ready.eq(AnySeq(1))
  17         m.d.comb += dut.p.i_valid.eq(AnySeq(1))
  18         a = dut.p.i_data.a
  19         b = dut.p.i_data.b
  20         z = dut.n.o_data.z
  21         f16 = SmtSortFloat16()
  22         rm = ROUND_NEAREST_TIES_TO_EVEN
  23         a_fp = SmtFloatingPoint.from_bits(a, sort=f16)
  24         b_fp = SmtFloatingPoint.from_bits(b, sort=f16)
  25         z_fp = SmtFloatingPoint.from_bits(z, sort=f16)
  26         expected_fp = a_fp.add(b_fp, rm=rm)
  27         expected = Signal(16)
  28         m.d.comb += expected.eq(AnySeq(16))
  29         # Important Note: expected and z won't necessarily match bit-exactly
  30         # if it's a NaN, all this checks for is z is also any NaN
  31         m.d.comb += Assume((SmtFloatingPoint.from_bits(expected, sort=f16)
  32                             == expected_fp).as_value())
  33         # FIXME: check that it produces the correct NaNs
  34         m.d.comb += a.eq(AnyConst(16))
  35         m.d.comb += b.eq(AnyConst(16))
  36         with m.If(dut.n.trigger):
  37             m.d.sync += Assert((z_fp == expected_fp).as_value())
  38         self.assertFormal(m, depth=5, solver="z3")
  39
  40     # FIXME: check other rounding modes
  41     # FIXME: check exception flags
  42
  43
  44 if __name__ == '__main__':
  45     unittest.main()