From: Luke Kenneth Casson Leighton <lkcl@lkcl.net>
Date: Thu, 4 Jun 2020 12:45:56 +0000 (+0100)
Subject: add copy of FHDLTestCase from nmigen
X-Git-Tag: 24jan2021_ls180~54
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=35be9017fd75f4e5a9d608546b0ead39c639d858;p=nmutil.git

add copy of FHDLTestCase from nmigen
---

diff --git a/src/nmutil/formal/proof_clz.py b/src/nmutil/formal/proof_clz.py
index 209658e..aac25d3 100644
--- a/src/nmutil/formal/proof_clz.py
+++ b/src/nmutil/formal/proof_clz.py
@@ -1,6 +1,6 @@
 from nmigen import Module, Signal, Elaboratable, Mux, Const
 from nmigen.asserts import Assert, AnyConst, Assume
-from nmigen.test.utils import FHDLTestCase
+from nmutil.formaltest import FHDLTestCase
 from nmigen.cli import rtlil
 
 from nmutil.clz import CLZ
diff --git a/src/nmutil/formaltest.py b/src/nmutil/formaltest.py
new file mode 100644
index 0000000..dca64ca
--- /dev/null
+++ b/src/nmutil/formaltest.py
@@ -0,0 +1,107 @@
+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)
+