tests/utils.py

   1 import os
   2 import re
   3 import shutil
   4 import subprocess
   5 import textwrap
   6 import traceback
   7 import unittest
   8 from contextlib import contextmanager
   9
  10 from nmigen.hdl.ast import *
  11 from nmigen.hdl.ir import *
  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     def assertFormal(self, spec, mode="bmc", depth=1):
  31         stack = traceback.extract_stack()
  32         for frame in reversed(stack):
  33             if os.path.dirname(__file__) not in frame.filename:
  34                 break
  35             caller = frame
  36
  37         spec_root, _ = os.path.splitext(caller.filename)
  38         spec_dir = os.path.dirname(spec_root)
  39         spec_name = "{}_{}".format(
  40             os.path.basename(spec_root).replace("test_", "spec_"),
  41             caller.name.replace("test_", "")
  42         )
  43
  44         # The sby -f switch seems not fully functional when sby is reading from stdin.
  45         if os.path.exists(os.path.join(spec_dir, spec_name)):
  46             shutil.rmtree(os.path.join(spec_dir, spec_name))
  47
  48         if mode == "hybrid":
  49             # A mix of BMC and k-induction, as per personal communication with Claire Wolf.
  50             script = "setattr -unset init w:* a:nmigen.sample_reg %d"
  51             mode   = "bmc"
  52         else:
  53             script = ""
  54
  55         config = textwrap.dedent("""\
  56         [options]
  57         mode {mode}
  58         depth {depth}
  59         wait on
  60
  61         [engines]
  62         smtbmc
  63
  64         [script]
  65         read_ilang top.il
  66         prep
  67         {script}
  68
  69         [file top.il]
  70         {rtlil}
  71         """).format(
  72             mode=mode,
  73             depth=depth,
  74             script=script,
  75             rtlil=rtlil.convert(Fragment.get(spec, platform="formal"))
  76         )
  77         with subprocess.Popen(
  78                 [require_tool("sby"), "-f", "-d", spec_name],
  79                 cwd=spec_dir, env={**os.environ, "PYTHONWARNINGS":"ignore"},
  80                 universal_newlines=True, stdin=subprocess.PIPE, stdout=subprocess.PIPE) as proc:
  81             stdout, stderr = proc.communicate(config)
  82             if proc.returncode != 0:
  83                 self.fail("Formal verification failed:\n" + stdout)