From a12b9c7b96d2cfe77863ab98680a98acddc61d32 Mon Sep 17 00:00:00 2001 From: Jean THOMAS Date: Fri, 19 Jun 2020 14:27:22 +0200 Subject: [PATCH] Remove tests from gram.compat --- gram/compat.py | 104 ----------------------------------- gram/test/.gitignore | 1 + gram/test/__init__.py | 0 gram/test/test_common.py | 2 + gram/test/test_compat.py | 51 +++++++++++++++++ gram/test/utils/__init__.py | 0 gram/test/utils/formal.py | 106 ++++++++++++++++++++++++++++++++++++ 7 files changed, 160 insertions(+), 104 deletions(-) create mode 100644 gram/test/.gitignore create mode 100644 gram/test/__init__.py create mode 100644 gram/test/test_common.py create mode 100644 gram/test/utils/__init__.py create mode 100644 gram/test/utils/formal.py diff --git a/gram/compat.py b/gram/compat.py index 5bda031..e049dcd 100644 --- a/gram/compat.py +++ b/gram/compat.py @@ -27,49 +27,6 @@ def delayed_enter(m, src, dst, delay): with m.State(statename): m.next = deststate -class DelayedEnterTestCase(unittest.TestCase): - def test_sequence(self): - def sequence(expected_delay): - m = Module() - - before = Signal() - end = Signal() - - with m.FSM(): - with m.State("Before-Delayed-Enter"): - m.d.comb += before.eq(1) - m.next = "Delayed-Enter" - - delayed_enter(m, "Delayed-Enter", "End-Delayed-Enter", expected_delay) - - with m.State("End-Delayed-Enter"): - m.d.comb += end.eq(1) - - def process(): - while (yield before): - yield - - delay = 0 - while not (yield end): - yield - delay += 1 - - self.assertEqual(delay, expected_delay) - - sim = Simulator(m) - with sim.write_vcd("test_compat.vcd"): - sim.add_clock(1e-6) - sim.add_sync_process(process) - sim.run() - - with self.assertRaises(AssertionError): - sequence(0) - sequence(1) - sequence(2) - sequence(10) - sequence(100) - sequence(1000) - class RoundRobin(Elaboratable): """A round-robin scheduler. (HarryHo90sHK) Parameters @@ -146,67 +103,6 @@ class Timeline(Elaboratable): return m -class TimelineTestCase(unittest.TestCase): - def test_sequence(self): - sigA = Signal() - sigB = Signal() - sigC = Signal() - timeline = Timeline([ - (1, sigA.eq(1)), - (5, sigA.eq(1)), - (7, sigA.eq(0)), - (10, sigB.eq(1)), - (11, sigB.eq(0)), - ]) - m = Module() - m.submodules.timeline = timeline - - def process(): - # Test default value for unset signals - self.assertFalse((yield sigA)) - self.assertFalse((yield sigB)) - - # Ensure that the sequence isn't triggered without the trigger signal - for i in range(100): - yield - self.assertFalse((yield sigA)) - self.assertFalse((yield sigB)) - - yield timeline.trigger.eq(1) - yield - yield timeline.trigger.eq(0) - - for i in range(11+1): - yield - - if i == 1: - self.assertTrue((yield sigA)) - self.assertFalse((yield sigB)) - elif i == 5: - self.assertTrue((yield sigA)) - self.assertFalse((yield sigB)) - elif i == 7: - self.assertFalse((yield sigA)) - self.assertFalse((yield sigB)) - elif i == 10: - self.assertFalse((yield sigA)) - self.assertTrue((yield sigB)) - elif i == 11: - self.assertFalse((yield sigA)) - self.assertFalse((yield sigB)) - - # Ensure no changes happen once the sequence is done - for i in range(100): - yield - self.assertFalse((yield sigA)) - self.assertFalse((yield sigB)) - - sim = Simulator(m) - with sim.write_vcd("test_compat.vcd"): - sim.add_clock(1e-6) - sim.add_sync_process(process) - sim.run() - class CSRPrefixProxy: def __init__(self, bank, prefix): diff --git a/gram/test/.gitignore b/gram/test/.gitignore new file mode 100644 index 0000000..9adb764 --- /dev/null +++ b/gram/test/.gitignore @@ -0,0 +1 @@ +spec_* diff --git a/gram/test/__init__.py b/gram/test/__init__.py new file mode 100644 index 0000000..e69de29 diff --git a/gram/test/test_common.py b/gram/test/test_common.py new file mode 100644 index 0000000..d1676d4 --- /dev/null +++ b/gram/test/test_common.py @@ -0,0 +1,2 @@ +import unittest +from .utils.formal import FHDLTestCase diff --git a/gram/test/test_compat.py b/gram/test/test_compat.py index 041bb0b..a1d4b3f 100644 --- a/gram/test/test_compat.py +++ b/gram/test/test_compat.py @@ -1,6 +1,9 @@ import unittest +from gram.test.utils.formal import FHDLTestCase from nmigen import * +from nmigen.hdl.ast import Past +from nmigen.asserts import Assert, Assume from gram.compat import * @@ -107,3 +110,51 @@ class TimelineTestCase(unittest.TestCase): sim.add_clock(1e-6) sim.add_sync_process(process) sim.run() + +class RoundRobinOutputMatchSpec(Elaboratable): + def __init__(self, dut): + self.dut = dut + + def elaborate(self, platform): + m = Module() + + m.d.comb += Assume(Rose(self.dut.stb).implies(self.dut.request == Past(self.dut.request))) + + m.d.sync += Assert(((Past(self.dut.request) != 0) & Past(self.dut.stb)).implies(Past(self.dut.request) & (1 << self.dut.grant))) + + return m + +class RoundRobinTestCase(FHDLTestCase): + def test_sequence(self): + m = Module() + m.submodules.rb = roundrobin = RoundRobin(8) + + def process(): + yield roundrobin.request.eq(0b10001000) + yield roundrobin.stb.eq(1) + yield + yield + + self.assertEqual((yield roundrobin.grant), 3) + yield + + self.assertEqual((yield roundrobin.grant), 7) + yield + + self.assertEqual((yield roundrobin.grant), 3) + yield roundrobin.request.eq(0b00000001) + yield + yield + + self.assertEqual((yield roundrobin.grant), 0) + + sim = Simulator(m) + with sim.write_vcd("test_compat.vcd"): + sim.add_clock(1e-6) + sim.add_sync_process(process) + sim.run() + + # def test_output_match(self): + # roundrobin = RoundRobin(32) + # spec = RoundRobinOutputMatchSpec(roundrobin) + # self.assertFormal(spec, mode="bmc", depth=10) \ No newline at end of file diff --git a/gram/test/utils/__init__.py b/gram/test/utils/__init__.py new file mode 100644 index 0000000..e69de29 diff --git a/gram/test/utils/formal.py b/gram/test/utils/formal.py new file mode 100644 index 0000000..dfbd63e --- /dev/null +++ b/gram/test/utils/formal.py @@ -0,0 +1,106 @@ +import os +import re +import shutil +import subprocess +import textwrap +import traceback +import unittest +import warnings +from contextlib import contextmanager + +from nmigen.hdl.ir import Fragment +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)) + + @contextmanager + def assertRaises(self, exception, msg=None): + with super().assertRaises(exception) as cm: + yield + if msg is not None: + # WTF? unittest.assertRaises is completely broken. + self.assertEqual(str(cm.exception), msg) + + @contextmanager + def assertRaisesRegex(self, exception, regex=None): + with super().assertRaises(exception) as cm: + yield + if regex is not None: + # unittest.assertRaisesRegex also seems broken... + self.assertRegex(str(cm.exception), regex) + + @contextmanager + def assertWarns(self, category, msg=None): + with warnings.catch_warnings(record=True) as warns: + yield + self.assertEqual(len(warns), 1) + self.assertEqual(warns[0].category, category) + if msg is not None: + self.assertEqual(str(warns[0].message), msg) + + 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) -- 2.30.2