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