From: whitequark <whitequark@whitequark.org>
Date: Thu, 27 Aug 2020 00:46:50 +0000 (+0000)
Subject: nmigen.test.utils: restore FHDLTestCase to gracefully deprecate it.
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=5b01499901d45400c58fba184c3ba6702d012858;p=nmigen.git

nmigen.test.utils: restore FHDLTestCase to gracefully deprecate it.

Fixes #484.
---

diff --git a/nmigen/test/__init__.py b/nmigen/test/__init__.py
new file mode 100644
index 0000000..2ec5765
--- /dev/null
+++ b/nmigen/test/__init__.py
@@ -0,0 +1 @@
+# TODO(nmigen-0.4): remove the entire package
diff --git a/nmigen/test/utils.py b/nmigen/test/utils.py
new file mode 100644
index 0000000..e00dbac
--- /dev/null
+++ b/nmigen/test/utils.py
@@ -0,0 +1,85 @@
+import os
+import re
+import shutil
+import subprocess
+import textwrap
+import traceback
+import unittest
+import warnings
+from contextlib import contextmanager
+
+from ..hdl.ast import *
+from ..hdl.ir import *
+from ..back import rtlil
+from .._toolchain import require_tool
+
+
+warnings.warn("nmigen.test.utils is an internal utility module that has several design flaws "
+              "and was never intended as a public API; it will be removed in nmigen 0.4. "
+              "if you are using FHDLTestCase, include its implementation in your codebase. "
+              "see also nmigen/nmigen#487",
+              DeprecationWarning, stacklevel=2)
+
+
+__all__ = ["FHDLTestCase"]
+
+
+class FHDLTestCase(unittest.TestCase):
+    def assertRepr(self, obj, repr_str):
+        if isinstance(obj, list):
+            obj = Statement.cast(obj)
+        def prepare_repr(repr_str):
+            repr_str = re.sub(r"\s+",   " ",  repr_str)
+            repr_str = re.sub(r"\( (?=\()", "(", repr_str)
+            repr_str = re.sub(r"\) (?=\))", ")", repr_str)
+            return repr_str.strip()
+        self.assertEqual(prepare_repr(repr(obj)), prepare_repr(repr_str))
+
+    def assertFormal(self, spec, mode="bmc", depth=1):
+        caller, *_ = traceback.extract_stack(limit=2)
+        spec_root, _ = os.path.splitext(caller.filename)
+        spec_dir = os.path.dirname(spec_root)
+        spec_name = "{}_{}".format(
+            os.path.basename(spec_root).replace("test_", "spec_"),
+            caller.name.replace("test_", "")
+        )
+
+        # The sby -f switch seems not fully functional when sby is reading from stdin.
+        if os.path.exists(os.path.join(spec_dir, spec_name)):
+            shutil.rmtree(os.path.join(spec_dir, spec_name))
+
+        if mode == "hybrid":
+            # A mix of BMC and k-induction, as per personal communication with Clifford Wolf.
+            script = "setattr -unset init w:* a:nmigen.sample_reg %d"
+            mode   = "bmc"
+        else:
+            script = ""
+
+        config = textwrap.dedent("""\
+        [options]
+        mode {mode}
+        depth {depth}
+        wait on
+
+        [engines]
+        smtbmc
+
+        [script]
+        read_ilang top.il
+        prep
+        {script}
+
+        [file top.il]
+        {rtlil}
+        """).format(
+            mode=mode,
+            depth=depth,
+            script=script,
+            rtlil=rtlil.convert(Fragment.get(spec, platform="formal"))
+        )
+        with subprocess.Popen([require_tool("sby"), "-f", "-d", spec_name], cwd=spec_dir,
+                              universal_newlines=True,
+                              stdin=subprocess.PIPE, stdout=subprocess.PIPE) as proc:
+            stdout, stderr = proc.communicate(config)
+            if proc.returncode != 0:
+                self.fail("Formal verification failed:\n" + stdout)