From 4f38a53d353e54cce7cff7a6b58dd1b477d5fbd5 Mon Sep 17 00:00:00 2001 From: Jacob Lifshay Date: Mon, 27 Jun 2022 21:53:04 -0700 Subject: [PATCH] add smtbmc_opts argument to assertFormal to allow passing more solver flags --- 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 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"], -- 2.30.2