mirrors/sby
3
0
Fork 0
mirror of https://github.com/YosysHQ/sby.git synced 2025-04-05 22:14:08 +00:00
Code Activity

Add "smtbmc ... -- ..." feature (for "raw" smtbmc options)

Browse source 
Signed-off-by: Clifford Wolf <clifford@clifford.at>
This commit is contained in:
Clifford Wolf 2018-11-22 17:08:28 +01:00
parent b50f4f3d10
commit 4eb91d5b88
2 changed files with 10 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
docs/source/reference.rst
View file

@ -241,6 +241,8 @@ The following solvers are currently supported by ``yosys-smtbmc``:
* mathsat * mathsat
* cvc4 * cvc4
Any additional options after ``--`` are passed to ``yosys-smtbmc`` as-is.
``aiger`` engine ``aiger`` engine
~~~~~~~~~~~~~~~~ ~~~~~~~~~~~~~~~~

9
sbysrc/sby_engine_smtbmc.py
View file

@ -67,10 +67,17 @@ def run(mode, job, engine_idx, engine):
else: else:
job.error("Invalid smtbmc options %s." % o) job.error("Invalid smtbmc options %s." % o)
xtra_opts = False
for i, a in enumerate(args): for i, a in enumerate(args):
if i == 0 and a == "z3" and unroll_opt is None: if i == 0 and a == "z3" and unroll_opt is None:
unroll_opt = False unroll_opt = False
smtbmc_opts += ["-s" if i == 0 else "-S", a] if a == "--":
xtra_opts = True
continue
if xtra_opts:
smtbmc_opts.append(a)
else:
smtbmc_opts += ["-s" if i == 0 else "-S", a]
if presat_opt: if presat_opt:
smtbmc_opts += ["--presat"] smtbmc_opts += ["--presat"]