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
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):
--- /dev/null
+import unittest
+from .utils.formal import FHDLTestCase
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 *
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
--- /dev/null
+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)
projects / gram.git / commitdiff