9 from contextlib
import contextmanager
11 from ..hdl
.ast
import *
12 from ..hdl
.ir
import *
13 from ..back
import rtlil
14 from .._toolchain
import require_tool
17 warnings
.warn("nmigen.test.utils is an internal utility module that has several design flaws "
18 "and was never intended as a public API; it will be removed in nmigen 0.4. "
19 "if you are using FHDLTestCase, include its implementation in your codebase. "
20 "see also nmigen/nmigen#487",
21 DeprecationWarning, stacklevel
=2)
24 __all__
= ["FHDLTestCase"]
27 class FHDLTestCase(unittest
.TestCase
):
28 def assertRepr(self
, obj
, repr_str
):
29 if isinstance(obj
, list):
30 obj
= Statement
.cast(obj
)
31 def prepare_repr(repr_str
):
32 repr_str
= re
.sub(r
"\s+", " ", repr_str
)
33 repr_str
= re
.sub(r
"\( (?=\()", "(", repr_str
)
34 repr_str
= re
.sub(r
"\) (?=\))", ")", repr_str
)
35 return repr_str
.strip()
36 self
.assertEqual(prepare_repr(repr(obj
)), prepare_repr(repr_str
))
38 def assertFormal(self
, spec
, mode
="bmc", depth
=1):
39 caller
, *_
= traceback
.extract_stack(limit
=2)
40 spec_root
, _
= os
.path
.splitext(caller
.filename
)
41 spec_dir
= os
.path
.dirname(spec_root
)
42 spec_name
= "{}_{}".format(
43 os
.path
.basename(spec_root
).replace("test_", "spec_"),
44 caller
.name
.replace("test_", "")
47 # The sby -f switch seems not fully functional when sby is reading from stdin.
48 if os
.path
.exists(os
.path
.join(spec_dir
, spec_name
)):
49 shutil
.rmtree(os
.path
.join(spec_dir
, spec_name
))
52 # A mix of BMC and k-induction, as per personal communication with Claire Wolf.
53 script
= "setattr -unset init w:* a:nmigen.sample_reg %d"
58 config
= textwrap
.dedent("""\
78 rtlil
=rtlil
.convert(Fragment
.get(spec
, platform
="formal"))
80 with subprocess
.Popen([require_tool("sby"), "-f", "-d", spec_name
], cwd
=spec_dir
,
81 universal_newlines
=True,
82 stdin
=subprocess
.PIPE
, stdout
=subprocess
.PIPE
) as proc
:
83 stdout
, stderr
= proc
.communicate(config
)
84 if proc
.returncode
!= 0:
85 self
.fail("Formal verification failed:\n" + stdout
)