projects
/
nmutil.git
/ commitdiff
commit
grep
author
committer
pickaxe
?
search:
re
summary
|
shortlog
|
log
|
commit
| commitdiff |
tree
raw
|
patch
|
inline
| side by side (parent:
7d5a0ec
)
add smtbmc_opts argument to assertFormal to allow passing more solver flags
author
Jacob Lifshay
<programmerjake@gmail.com>
Tue, 28 Jun 2022 04:53:04 +0000
(21:53 -0700)
committer
Jacob Lifshay
<programmerjake@gmail.com>
Tue, 28 Jun 2022 04:53:04 +0000
(21:53 -0700)
src/nmutil/formaltest.py
patch
|
blob
|
history
diff --git
a/src/nmutil/formaltest.py
b/src/nmutil/formaltest.py
index dd2b4ae45029db82ad53b6e69c8060cd09471836..db89f9e342ad63117a4313a601803d6effae860a 100644
(file)
--- 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="",
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
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]
wait on
[engines]
- smtbmc {solver} -- --
--logic=ALL
+ smtbmc {solver} -- --
{smtbmc_opts}
[script]
read_ilang top.il
[script]
read_ilang top.il
@@
-63,6
+63,7
@@
class FHDLTestCase(unittest.TestCase):
depth=depth,
solver=solver,
script=script,
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"],
rtlil=rtlil.convert(Fragment.get(spec, platform="formal"))
)
with subprocess.Popen([require_tool("sby"), "-d", "job"],