From 21acf64132844a543f0f5ba5059ead8a56066c10 Mon Sep 17 00:00:00 2001 From: whitequark Date: Thu, 27 Aug 2020 00:46:50 +0000 Subject: [PATCH] nmigen.test.utils: restore FHDLTestCase to gracefully deprecate it. Fixes #484. --- nmigen/test/__init__.py | 1 + nmigen/test/utils.py | 85 +++++++++++++++++++++++++++++++++++++++++ 2 files changed, 86 insertions(+) create mode 100644 nmigen/test/__init__.py create mode 100644 nmigen/test/utils.py 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) -- 2.30.2