nmigen/test/utils.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 ..hdl.ir import *
  13 from ..back import rtlil
  14 from .._toolchain import require_tool
  15
  16
  17 warnings.warn("nmigen.test.utils is an internal utility module that has several design flaws "
  18               "and was never intended as a public API; it will be removed in nmigen 0.4. "
  19               "if you are using FHDLTestCase, include its implementation in your codebase. "
  20               "see also nmigen/nmigen#487",
  21               DeprecationWarning, stacklevel=2)
  22
  23
  24 __all__ = ["FHDLTestCase"]
  25
  26
  27 class FHDLTestCase(unittest.TestCase):
  28     def assertRepr(self, obj, repr_str):
  29         if isinstance(obj, list):
  30             obj = Statement.cast(obj)
  31         def prepare_repr(repr_str):
  32             repr_str = re.sub(r"\s+",   " ",  repr_str)
  33             repr_str = re.sub(r"\( (?=\()", "(", repr_str)
  34             repr_str = re.sub(r"\) (?=\))", ")", repr_str)
  35             return repr_str.strip()
  36         self.assertEqual(prepare_repr(repr(obj)), prepare_repr(repr_str))
  37
  38     def assertFormal(self, spec, mode="bmc", depth=1):
  39         caller, *_ = traceback.extract_stack(limit=2)
  40         spec_root, _ = os.path.splitext(caller.filename)
  41         spec_dir = os.path.dirname(spec_root)
  42         spec_name = "{}_{}".format(
  43             os.path.basename(spec_root).replace("test_", "spec_"),
  44             caller.name.replace("test_", "")
  45         )
  46
  47         # The sby -f switch seems not fully functional when sby is reading from stdin.
  48         if os.path.exists(os.path.join(spec_dir, spec_name)):
  49             shutil.rmtree(os.path.join(spec_dir, spec_name))
  50
  51         if mode == "hybrid":
  52             # A mix of BMC and k-induction, as per personal communication with Claire Wolf.
  53             script = "setattr -unset init w:* a:nmigen.sample_reg %d"
  54             mode   = "bmc"
  55         else:
  56             script = ""
  57
  58         config = textwrap.dedent("""\
  59         [options]
  60         mode {mode}
  61         depth {depth}
  62         wait on
  63
  64         [engines]
  65         smtbmc
  66
  67         [script]
  68         read_ilang top.il
  69         prep
  70         {script}
  71
  72         [file top.il]
  73         {rtlil}
  74         """).format(
  75             mode=mode,
  76             depth=depth,
  77             script=script,
  78             rtlil=rtlil.convert(Fragment.get(spec, platform="formal"))
  79         )
  80         with subprocess.Popen([require_tool("sby"), "-f", "-d", spec_name], cwd=spec_dir,
  81                               universal_newlines=True,
  82                               stdin=subprocess.PIPE, stdout=subprocess.PIPE) as proc:
  83             stdout, stderr = proc.communicate(config)
  84             if proc.returncode != 0:
  85                 self.fail("Formal verification failed:\n" + stdout)