67b957d4f4
Compared to tests in the repository root, tests in the package have
many downsides:
* Unless explicitly excluded in find_packages(), tests and their
support code effectively become a part of public API.
This, unfortunately, happened with FHDLTestCase, which was never
intended for downstream use.
* Even if explicitly excluded from the setuptools package, using
an editable install, or setting PYTHONPATH still allows accessing
the tests.
* Having a sub-package that is present in the source tree but not
exported (or, worse, exported only sometimes) is confusing.
* The name `nmigen.test` cannot be used for anything else, such as
testing utilities that *are* intended for downstream use.
78 lines
2.4 KiB
Python
78 lines
2.4 KiB
Python
import os
|
|
import re
|
|
import shutil
|
|
import subprocess
|
|
import textwrap
|
|
import traceback
|
|
import unittest
|
|
from contextlib import contextmanager
|
|
|
|
from nmigen.hdl.ast import *
|
|
from nmigen.hdl.ir import *
|
|
from nmigen.back import rtlil
|
|
from nmigen._toolchain import require_tool
|
|
|
|
|
|
__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)
|