From: Donald Sebastian Leung
Date: Wed, 19 Aug 2020 03:49:55 +0000 (+0800)
Subject: Add option to specify solver in nmigen.test.utils
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=b3e088edecc2ff68736737af6ffb6b6cd777a918;p=nmigen.git
Add option to specify solver in nmigen.test.utils
---
diff --git a/nmigen/test/utils.py b/nmigen/test/utils.py
index c3907ce..4124127 100644
--- a/nmigen/test/utils.py
+++ b/nmigen/test/utils.py
@@ -53,7 +53,7 @@ class FHDLTestCase(unittest.TestCase):
if msg is not None:
self.assertEqual(str(warns[0].message), msg)
- def assertFormal(self, spec, mode="bmc", depth=1):
+ def assertFormal(self, spec, mode="bmc", depth=1, engine="smtbmc"):
caller, *_ = traceback.extract_stack(limit=2)
spec_root, _ = os.path.splitext(caller.filename)
spec_dir = os.path.dirname(spec_root)
@@ -80,7 +80,7 @@ class FHDLTestCase(unittest.TestCase):
wait on
[engines]
- smtbmc
+ {engine}
[script]
read_ilang top.il
@@ -92,6 +92,7 @@ class FHDLTestCase(unittest.TestCase):
""").format(
mode=mode,
depth=depth,
+ engine=engine,
script=script,
rtlil=rtlil.convert(Fragment.get(spec, platform="formal"))
)