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 "append" option

Browse source
This commit is contained in:
Clifford Wolf 2017-02-26 11:08:14 +01:00
parent 94260e01b8
commit 7be08218cb
6 changed files with 18 additions and 6 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
sbysrc/sby_engine_abc.py
View file

@ -81,9 +81,9 @@ def run(mode, job, engine_idx, engine):
if task_status == "FAIL": if task_status == "FAIL":
task2 = SbyTask(job, "engine_%d" % engine_idx, job.model("smt2"), task2 = SbyTask(job, "engine_%d" % engine_idx, job.model("smt2"),
("cd %s; %s -s %s --noprogress --dump-vcd engine_%d/trace.vcd --dump-vlogtb engine_%d/trace_tb.v " + ("cd %s; %s -s %s --noprogress --append %d --dump-vcd engine_%d/trace.vcd --dump-vlogtb engine_%d/trace_tb.v " +
"--dump-smtc engine_%d/trace.smtc --aig model/design_aiger.aim:engine_%d/trace.aiw --aig-noheader model/design_smt2.smt2") % "--dump-smtc engine_%d/trace.smtc --aig model/design_aiger.aim:engine_%d/trace.aiw --aig-noheader model/design_smt2.smt2") %
(job.workdir, job.exe_paths["smtbmc"], job.opt_aigsmt, engine_idx, engine_idx, engine_idx, engine_idx), (job.workdir, job.exe_paths["smtbmc"], job.opt_aigsmt, job.opt_append, engine_idx, engine_idx, engine_idx, engine_idx),
logfile=open("%s/engine_%d/logfile2.txt" % (job.workdir, engine_idx), "w")) logfile=open("%s/engine_%d/logfile2.txt" % (job.workdir, engine_idx), "w"))
task2_status = None task2_status = None

4
sbysrc/sby_engine_aiger.py
View file

@ -78,9 +78,9 @@ def run(mode, job, engine_idx, engine):
if task_status == "FAIL": if task_status == "FAIL":
task2 = SbyTask(job, "engine_%d" % engine_idx, job.model("smt2"), task2 = SbyTask(job, "engine_%d" % engine_idx, job.model("smt2"),
("cd %s; %s -s %s --noprogress --dump-vcd engine_%d/trace.vcd --dump-vlogtb engine_%d/trace_tb.v " + ("cd %s; %s -s %s --noprogress --append %d --dump-vcd engine_%d/trace.vcd --dump-vlogtb engine_%d/trace_tb.v " +
"--dump-smtc engine_%d/trace.smtc --aig model/design_aiger.aim:engine_%d/trace.aiw model/design_smt2.smt2") % "--dump-smtc engine_%d/trace.smtc --aig model/design_aiger.aim:engine_%d/trace.aiw model/design_smt2.smt2") %
(job.workdir, job.exe_paths["smtbmc"], job.opt_aigsmt, engine_idx, engine_idx, engine_idx, engine_idx), (job.workdir, job.exe_paths["smtbmc"], job.opt_aigsmt, job,opt_append, engine_idx, engine_idx, engine_idx, engine_idx),
logfile=open("%s/engine_%d/logfile2.txt" % (job.workdir, engine_idx), "w")) logfile=open("%s/engine_%d/logfile2.txt" % (job.workdir, engine_idx), "w"))
task2_status = None task2_status = None

4
sbysrc/sby_engine_smtbmc.py
View file

@ -69,8 +69,8 @@ def run(mode, job, engine_idx, engine):
trace_prefix += "%" trace_prefix += "%"
task = SbyTask(job, taskname, job.model(model_name), task = SbyTask(job, taskname, job.model(model_name),
"cd %s; %s --noprogress %s -t %d --dump-vcd %s.vcd --dump-vlogtb %s_tb.v --dump-smtc %s.smtc model/design_%s.smt2" % "cd %s; %s --noprogress %s -t %d --append %d --dump-vcd %s.vcd --dump-vlogtb %s_tb.v --dump-smtc %s.smtc model/design_%s.smt2" %
(job.workdir, job.exe_paths["smtbmc"], " ".join(smtbmc_opts), job.opt_depth, trace_prefix, trace_prefix, trace_prefix, model_name), (job.workdir, job.exe_paths["smtbmc"], " ".join(smtbmc_opts), job.opt_depth, job.opt_append, trace_prefix, trace_prefix, trace_prefix, model_name),
logfile=open(logfile_prefix + ".txt", "w")) logfile=open(logfile_prefix + ".txt", "w"))
if mode == "prove_basecase": if mode == "prove_basecase":

4
sbysrc/sby_mode_bmc.py
View file

@ -21,11 +21,15 @@ from sby_core import SbyTask
def run(job): def run(job):
job.opt_depth = 20 job.opt_depth = 20
job.opt_append = 0
job.opt_aigsmt = "z3" job.opt_aigsmt = "z3"
if "depth" in job.options: if "depth" in job.options:
job.opt_depth = int(job.options["depth"]) job.opt_depth = int(job.options["depth"])
if "append" in job.options:
job.opt_append = int(job.options["append"])
if "aigsmt" in job.options: if "aigsmt" in job.options:
job.opt_aigsmt = job.options["aigsmt"] job.opt_aigsmt = job.options["aigsmt"]

4
sbysrc/sby_mode_cover.py
View file

@ -21,10 +21,14 @@ from sby_core import SbyTask
def run(job): def run(job):
job.opt_depth = 20 job.opt_depth = 20
job.opt_append = 0
if "depth" in job.options: if "depth" in job.options:
job.opt_depth = int(job.options["depth"]) job.opt_depth = int(job.options["depth"])
if "append" in job.options:
job.opt_append = int(job.options["append"])
for engine_idx in range(len(job.engines)): for engine_idx in range(len(job.engines)):
engine = job.engines[engine_idx] engine = job.engines[engine_idx]
assert len(engine) > 0 assert len(engine) > 0

4
sbysrc/sby_mode_prove.py
View file

@ -21,11 +21,15 @@ from sby_core import SbyTask
def run(job): def run(job):
job.opt_depth = 20 job.opt_depth = 20
job.opt_append = 0
job.opt_aigsmt = "z3" job.opt_aigsmt = "z3"
if "depth" in job.options: if "depth" in job.options:
job.opt_depth = int(job.options["depth"]) job.opt_depth = int(job.options["depth"])
if "append" in job.options:
job.opt_append = int(job.options["append"])
if "aigsmt" in job.options: if "aigsmt" in job.options:
job.opt_aigsmt = job.options["aigsmt"] job.opt_aigsmt = job.options["aigsmt"]