86 lines
2.7 KiB
Python
86 lines
2.7 KiB
Python
|
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)
|