src/ieee754/test/tools.py

   1 import os
   2 import re
   3 import shutil
   4 import subprocess
   5 import textwrap
   6 import traceback
   7 import unittest
   8 import warnings
   9 from contextlib import contextmanager
  10
  11 from nmigen.hdl.ast import Statement
  12 from nmigen.hdl.ir import Fragment
  13 from nmigen.back import rtlil
  14
  15
  16 __all__ = ["FHDLTestCase"]
  17
  18
  19 class FHDLTestCase(unittest.TestCase):
  20     def assertRepr(self, obj, repr_str):
  21         obj = Statement.wrap(obj)
  22         def prepare_repr(repr_str):
  23             repr_str = re.sub(r"\s+",   " ",  repr_str)
  24             repr_str = re.sub(r"\( (?=\()", "(", repr_str)
  25             repr_str = re.sub(r"\) (?=\))", ")", repr_str)
  26             return repr_str.strip()
  27         self.assertEqual(prepare_repr(repr(obj)), prepare_repr(repr_str))
  28
  29     @contextmanager
  30     def assertRaises(self, exception, msg=None):
  31         with super().assertRaises(exception) as cm:
  32             yield
  33         if msg is not None:
  34             # WTF? unittest.assertRaises is completely broken.
  35             self.assertEqual(str(cm.exception), msg)
  36
  37     @contextmanager
  38     def assertRaisesRegex(self, exception, regex=None):
  39         with super().assertRaises(exception) as cm:
  40             yield
  41         if regex is not None:
  42             # unittest.assertRaisesRegex also seems broken...
  43             self.assertRegex(str(cm.exception), regex)
  44
  45     @contextmanager
  46     def assertWarns(self, category, msg=None):
  47         with warnings.catch_warnings(record=True) as warns:
  48             yield
  49         self.assertEqual(len(warns), 1)
  50         self.assertEqual(warns[0].category, category)
  51         if msg is not None:
  52             self.assertEqual(str(warns[0].message), msg)
  53
  54     def assertFormal(self, spec, mode="bmc", depth=1):
  55         caller, *_ = traceback.extract_stack(limit=2)
  56         spec_root, _ = os.path.splitext(caller.filename)
  57         spec_dir = os.path.dirname(spec_root)
  58         spec_name = "{}_{}".format(
  59             os.path.basename(spec_root).replace("test_", "spec_"),
  60             caller.name.replace("test_", "")
  61         )
  62
  63         # The sby -f switch seems not fully functional when sby is reading from stdin.
  64         if os.path.exists(os.path.join(spec_dir, spec_name)):
  65             shutil.rmtree(os.path.join(spec_dir, spec_name))
  66
  67         if mode == "hybrid":
  68             # A mix of BMC and k-induction, as per personal communication with Clifford Wolf.
  69             script = "setattr -unset init w:* a:nmigen.sample_reg %d"
  70             mode   = "bmc"
  71         else:
  72             script = ""
  73
  74         config = textwrap.dedent("""\
  75         [options]
  76         mode {mode}
  77         depth {depth}
  78         wait on
  79
  80         [engines]
  81         smtbmc
  82
  83         [script]
  84         read_ilang top.il
  85         prep
  86         {script}
  87
  88         [file top.il]
  89         {rtlil}
  90         """).format(
  91             mode=mode,
  92             depth=depth,
  93             script=script,
  94             rtlil=rtlil.convert(Fragment.get(spec, platform="formal"))
  95         )
  96         with subprocess.Popen(["sby", "-f", "-d", spec_name], cwd=spec_dir,
  97                               universal_newlines=True,
  98                               stdin=subprocess.PIPE,
  99                               stdout=subprocess.PIPE) as proc:
 100             stdout, stderr = proc.communicate(config)
 101             if proc.returncode != 0:
 102                 self.fail("Formal verification failed:\n" + stdout)