riscv
/
yosys
mirror of https://github.com/YosysHQ/yosys.git
1
0
Fork 0
Code Issues Projects Releases Wiki Activity

Add "yosys-smtbmc -S <opt>"

This commit is contained in:
Clifford Wolf 2017-02-19 22:51:29 +01:00
parent cf25dc9ce7
commit 242c5f01de
1 changed files with 18 additions and 7 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

25
backends/smt2/smtio.py
View File

@ -60,6 +60,7 @@ class SmtIo:
if opts is not None: if opts is not None:
self.logic = opts.logic self.logic = opts.logic
self.solver = opts.solver self.solver = opts.solver
self.solver_opts = opts.solver_opts
self.debug_print = opts.debug_print self.debug_print = opts.debug_print
self.debug_file = opts.debug_file self.debug_file = opts.debug_file
self.dummy_file = opts.dummy_file self.dummy_file = opts.dummy_file
@ -71,6 +72,7 @@ class SmtIo:
else: else:
self.solver = "z3" self.solver = "z3"
self.solver_opts = list()
self.debug_print = False self.debug_print = False
self.debug_file = None self.debug_file = None
self.dummy_file = None self.dummy_file = None
@ -81,23 +83,26 @@ class SmtIo:
self.nocomments = False self.nocomments = False
if self.solver == "yices": if self.solver == "yices":
self.popen_vargs = ['yices-smt2', '--incremental'] self.popen_vargs = ['yices-smt2', '--incremental'] + self.solver_opts
if self.solver == "z3": if self.solver == "z3":
self.popen_vargs = ['z3', '-smt2', '-in'] self.popen_vargs = ['z3', '-smt2', '-in'] + self.solver_opts
if self.solver == "cvc4": if self.solver == "cvc4":
self.popen_vargs = ['cvc4', '--incremental', '--lang', 'smt2'] self.popen_vargs = ['cvc4', '--incremental', '--lang', 'smt2'] + self.solver_opts
if self.solver == "mathsat": if self.solver == "mathsat":
self.popen_vargs = ['mathsat'] self.popen_vargs = ['mathsat'] + self.solver_opts
if self.solver == "boolector": if self.solver == "boolector":
self.popen_vargs = ['boolector', '--smt2', '-i'] self.popen_vargs = ['boolector', '--smt2', '-i'] + self.solver_opts
self.unroll = True self.unroll = True
if self.solver == "abc": if self.solver == "abc":
self.popen_vargs = ['yosys-abc', '-S', '%blast; &sweep -C 5000; &syn4; &cec -s -m -C 2000'] if len(self.solver_opts) > 0:
self.popen_vargs = ['yosys-abc', '-S', '; '.join(self.solver_opts)]
else:
self.popen_vargs = ['yosys-abc', '-S', '%blast; &sweep -C 5000; &syn4; &cec -s -m -C 2000']
self.logic_ax = False self.logic_ax = False
self.unroll = True self.unroll = True
self.noincr = True self.noincr = True
@ -634,9 +639,10 @@ class SmtIo:
class SmtOpts: class SmtOpts:
def __init__(self): def __init__(self):
self.shortopts = "s:v" self.shortopts = "s:S:v"
self.longopts = ["unroll", "noincr", "noprogress", "dump-smt2=", "logic=", "dummy=", "info=", "nocomments"] self.longopts = ["unroll", "noincr", "noprogress", "dump-smt2=", "logic=", "dummy=", "info=", "nocomments"]
self.solver = "z3" self.solver = "z3"
self.solver_opts = list()
self.debug_print = False self.debug_print = False
self.debug_file = None self.debug_file = None
self.dummy_file = None self.dummy_file = None
@ -650,6 +656,8 @@ class SmtOpts:
def handle(self, o, a): def handle(self, o, a):
if o == "-s": if o == "-s":
self.solver = a self.solver = a
elif o == "-S":
self.solver_opts.append(a)
elif o == "-v": elif o == "-v":
self.debug_print = True self.debug_print = True
elif o == "--unroll": elif o == "--unroll":
@ -678,6 +686,9 @@ class SmtOpts:
set SMT solver: z3, cvc4, yices, mathsat, boolector, dummy set SMT solver: z3, cvc4, yices, mathsat, boolector, dummy
default: z3 default: z3
-S <opt>
pass <opt> as command line argument to the solver
--logic <smt2_logic> --logic <smt2_logic>
use the specified SMT2 logic (e.g. QF_AUFBV) use the specified SMT2 logic (e.g. QF_AUFBV)