From: Jacob Lifshay <programmerjake@gmail.com>
Date: Tue, 28 Jun 2022 04:53:04 +0000 (-0700)
Subject: add smtbmc_opts argument to assertFormal to allow passing more solver flags
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=4f38a53d353e54cce7cff7a6b58dd1b477d5fbd5;p=nmutil.git

add smtbmc_opts argument to assertFormal to allow passing more solver flags
---

diff --git a/src/nmutil/formaltest.py b/src/nmutil/formaltest.py
index dd2b4ae..db89f9e 100644
--- a/src/nmutil/formaltest.py
+++ b/src/nmutil/formaltest.py
@@ -26,7 +26,7 @@ class FHDLTestCase(unittest.TestCase):
         self.assertEqual(prepare_repr(repr(obj)), prepare_repr(repr_str))
 
     def assertFormal(self, spec, mode="bmc", depth=1, solver="",
-                     base_path="formal_test_temp"):
+                     base_path="formal_test_temp", smtbmc_opts="--logic=ALL"):
         path = get_test_path(self, base_path)
 
         # The sby -f switch seems not fully functional when sby is
@@ -49,7 +49,7 @@ class FHDLTestCase(unittest.TestCase):
         wait on
 
         [engines]
-        smtbmc {solver} -- -- --logic=ALL
+        smtbmc {solver} -- -- {smtbmc_opts}
 
         [script]
         read_ilang top.il
@@ -63,6 +63,7 @@ class FHDLTestCase(unittest.TestCase):
             depth=depth,
             solver=solver,
             script=script,
+            smtbmc_opts=smtbmc_opts,
             rtlil=rtlil.convert(Fragment.get(spec, platform="formal"))
         )
         with subprocess.Popen([require_tool("sby"), "-d", "job"],