9 from contextlib
import contextmanager
12 from nmigen
.back
.pysim
import *
13 from nmigen
.hdl
.ir
import Fragment
14 from nmigen
.back
import rtlil
15 from nmigen
._toolchain
import require_tool
18 __all__
= ["FHDLTestCase", "runSimulation", "wb_read", "wb_write"]
20 def runSimulation(module
, process
, vcd_filename
="anonymous.vcd", clock
=1e-6):
21 sim
= Simulator(module
)
22 with sim
.write_vcd(vcd_filename
):
24 sim
.add_sync_process(process
)
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
))
39 def assertRaises(self
, exception
, msg
=None):
40 with
super().assertRaises(exception
) as cm
:
43 # WTF? unittest.assertRaises is completely broken.
44 self
.assertEqual(str(cm
.exception
), msg
)
47 def assertRaisesRegex(self
, exception
, regex
=None):
48 with
super().assertRaises(exception
) as cm
:
51 # unittest.assertRaisesRegex also seems broken...
52 self
.assertRegex(str(cm
.exception
), regex
)
55 def assertWarns(self
, category
, msg
=None):
56 with warnings
.catch_warnings(record
=True) as warns
:
58 self
.assertEqual(len(warns
), 1)
59 self
.assertEqual(warns
[0].category
, category
)
61 self
.assertEqual(str(warns
[0].message
), msg
)
63 def assertFormal(self
, spec
, mode
="bmc", depth
=1):
64 caller
, *_
= traceback
.extract_stack(limit
=2)
65 spec_root
, _
= os
.path
.splitext(caller
.filename
)
66 spec_dir
= os
.path
.dirname(spec_root
)
67 spec_name
= "{}_{}".format(
68 os
.path
.basename(spec_root
).replace("test_", "spec_"),
69 caller
.name
.replace("test_", "")
72 # The sby -f switch seems not fully functional when sby is
74 if os
.path
.exists(os
.path
.join(spec_dir
, spec_name
)):
75 shutil
.rmtree(os
.path
.join(spec_dir
, spec_name
))
77 config
= textwrap
.dedent("""\
96 rtlil
=rtlil
.convert(Fragment
.get(spec
, platform
="formal"))
98 with subprocess
.Popen([require_tool("sby"), "-f", "-d", spec_name
],
100 universal_newlines
=True,
101 stdin
=subprocess
.PIPE
,
102 stdout
=subprocess
.PIPE
) as proc
:
103 stdout
, stderr
= proc
.communicate(config
)
104 if proc
.returncode
!= 0:
105 self
.fail("Formal verification failed:\n" + stdout
)
107 def wb_read(bus
, addr
, sel
, timeout
=32):
110 yield bus
.adr
.eq(addr
)
111 yield bus
.sel
.eq(sel
)
114 while not (yield bus
.ack
):
116 if cycles
>= timeout
:
117 raise RuntimeError("Wishbone transaction timed out")
119 data
= (yield bus
.dat_r
)
124 def wb_write(bus
, addr
, data
, sel
, timeout
=32):
127 yield bus
.adr
.eq(addr
)
129 yield bus
.sel
.eq(sel
)
130 yield bus
.dat_w
.eq(data
)
133 while not (yield bus
.ack
):
135 if cycles
>= timeout
:
136 raise RuntimeError("Wishbone transaction timed out")