nmigen.test.utils: restore FHDLTestCase to gracefully deprecate it.
Fixes #484.
This commit is contained in:
parent
67b957d4f4
commit
5b01499901
1
nmigen/test/__init__.py
Normal file
1
nmigen/test/__init__.py
Normal file
|
@ -0,0 +1 @@
|
|||
# TODO(nmigen-0.4): remove the entire package
|
85
nmigen/test/utils.py
Normal file
85
nmigen/test/utils.py
Normal file
|
@ -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)
|
Loading…
Reference in a new issue