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