From 268b22e9dad1df913d86ebc631c69dc218c63242 Mon Sep 17 00:00:00 2001 From: Cesar Strauss Date: Sat, 23 Jan 2021 06:43:43 -0300 Subject: [PATCH] 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. --- src/nmutil/formaltest.py | 5 +++-- 1 file changed, 3 insertions(+), 2 deletions(-) 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")) ) -- 2.30.2