From: Cesar Strauss <cestrauss@gmail.com>
Date: Sat, 23 Jan 2021 09:43:43 +0000 (-0300)
Subject: Allow choosing a non-default solver in assertFormal
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=268b22e9dad1df913d86ebc631c69dc218c63242;p=nmutil.git

Allow choosing a non-default solver in assertFormal

It seems that small changes can dramatically affect the speed of the
default solver (yices2), while z3 is unaffected.

Let's use the one that gives the best results.
---

diff --git a/src/nmutil/formaltest.py b/src/nmutil/formaltest.py
index dca64ca..4b9b174 100644
--- a/src/nmutil/formaltest.py
+++ b/src/nmutil/formaltest.py
@@ -52,7 +52,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, solver=""):
         caller, *_ = traceback.extract_stack(limit=2)
         spec_root, _ = os.path.splitext(caller.filename)
         spec_dir = os.path.dirname(spec_root)
@@ -81,7 +81,7 @@ class FHDLTestCase(unittest.TestCase):
         wait on
 
         [engines]
-        smtbmc
+        smtbmc {solver}
 
         [script]
         read_ilang top.il
@@ -93,6 +93,7 @@ class FHDLTestCase(unittest.TestCase):
         """).format(
             mode=mode,
             depth=depth,
+            solver=solver,
             script=script,
             rtlil=rtlil.convert(Fragment.get(spec, platform="formal"))
         )