7 from contextlib
import contextmanager
8 from nmigen
.hdl
.ast
import Statement
9 from nmigen
.hdl
.ir
import Fragment
10 from nmigen
.back
import rtlil
11 from nmigen
._toolchain
import require_tool
12 from nmutil
.get_test_path
import get_test_path
15 __all__
= ["FHDLTestCase"]
18 class FHDLTestCase(unittest
.TestCase
):
19 def assertRepr(self
, obj
, repr_str
):
20 if isinstance(obj
, list):
21 obj
= Statement
.cast(obj
)
23 def prepare_repr(repr_str
):
24 repr_str
= re
.sub(r
"\s+", " ", repr_str
)
25 repr_str
= re
.sub(r
"\( (?=\()", "(", repr_str
)
26 repr_str
= re
.sub(r
"\) (?=\))", ")", repr_str
)
27 return repr_str
.strip()
28 self
.assertEqual(prepare_repr(repr(obj
)), prepare_repr(repr_str
))
31 def assertRaises(self
, exception
, msg
=None):
32 with
super().assertRaises(exception
) as cm
:
35 # WTF? unittest.assertRaises is completely broken.
36 self
.assertEqual(str(cm
.exception
), msg
)
39 def assertRaisesRegex(self
, exception
, regex
=None):
40 with
super().assertRaises(exception
) as cm
:
43 # unittest.assertRaisesRegex also seems broken...
44 self
.assertRegex(str(cm
.exception
), regex
)
47 def assertWarns(self
, category
, msg
=None):
48 with warnings
.catch_warnings(record
=True) as warns
:
50 self
.assertEqual(len(warns
), 1)
51 self
.assertEqual(warns
[0].category
, category
)
53 self
.assertEqual(str(warns
[0].message
), msg
)
55 def assertFormal(self
, spec
, mode
="bmc", depth
=1, solver
="",
56 base_path
="formal_test_temp"):
57 path
= get_test_path(self
, base_path
)
59 # The sby -f switch seems not fully functional when sby is
61 shutil
.rmtree(path
, ignore_errors
=True)
62 path
.mkdir(parents
=True)
65 # A mix of BMC and k-induction, as per personal
66 # communication with Clifford Wolf.
67 script
= "setattr -unset init w:* a:nmigen.sample_reg %d"
72 config
= textwrap
.dedent("""\
93 rtlil
=rtlil
.convert(Fragment
.get(spec
, platform
="formal"))
95 with subprocess
.Popen([require_tool("sby"), "-d", "job"],
97 universal_newlines
=True,
98 stdin
=subprocess
.PIPE
,
99 stdout
=subprocess
.PIPE
) as proc
:
100 stdout
, stderr
= proc
.communicate(config
)
101 if proc
.returncode
!= 0:
102 self
.fail("Formal verification failed:\n" + stdout
)