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

Working BTOR BMC engine

Browse source 
Signed-off-by: Clifford Wolf <clifford@clifford.at>
This commit is contained in:
Clifford Wolf 2018-12-08 07:01:21 +01:00
parent 4c485766e2
commit 150f30ae08
2 changed files with 26 additions and 18 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
sbysrc/sby_core.py
View file

@ -338,6 +338,10 @@ class SbyJob:
with open("%s/model/design_%s.ys" % (self.workdir, model_name), "w") as f: with open("%s/model/design_%s.ys" % (self.workdir, model_name), "w") as f:
print("# running in %s/model/" % (self.workdir), file=f) print("# running in %s/model/" % (self.workdir), file=f)
print("read_ilang design%s.il" % ("_nomem" if "_nomem" in model_name else ""), file=f) print("read_ilang design%s.il" % ("_nomem" if "_nomem" in model_name else ""), file=f)
print("flatten", file=f)
print("setattr -unset keep", file=f)
print("delete -output", file=f)
print("opt -full", file=f)
if "_syn" in model_name: if "_syn" in model_name:
print("techmap", file=f) print("techmap", file=f)
print("opt -fast", file=f) print("opt -fast", file=f)

40
sbysrc/sby_engine_btor.py
View file

@ -29,7 +29,7 @@ def run(mode, job, engine_idx, engine):
job.error("Unexpected BTOR engine options.") job.error("Unexpected BTOR engine options.")
if solver_args[0] == "btormc": if solver_args[0] == "btormc":
solver_cmd = job.exe_paths["btormc"] + " --stop-first -kmax %d" % job.opt_depth solver_cmd = job.exe_paths["btormc"] + " --stop-first -v 1 -kmax %d" % job.opt_depth
if job.opt_skip is not None: if job.opt_skip is not None:
solver_cmd += " -kmin %d" % job.opt_skip solver_cmd += " -kmin %d" % job.opt_skip
solver_cmd += " ".join([""] + solver_args[1:]) solver_cmd += " ".join([""] + solver_args[1:])
@ -44,39 +44,43 @@ def run(mode, job, engine_idx, engine):
task_status = None task_status = None
produced_cex = False produced_cex = False
end_of_cex = False end_of_cex = False
aiw_file = open("%s/engine_%d/trace.aiw" % (job.workdir, engine_idx), "w") wit_file = open("%s/engine_%d/trace.wit" % (job.workdir, engine_idx), "w")
def output_callback(line): def output_callback(line):
nonlocal task_status nonlocal task_status
nonlocal produced_cex nonlocal produced_cex
nonlocal end_of_cex nonlocal end_of_cex
if task_status is not None: if not end_of_cex and not produced_cex and line == "sat":
if not end_of_cex and not produced_cex and line.isdigit(): produced_cex = True
produced_cex = True task_status = "FAIL"
if not end_of_cex:
print(line, file=aiw_file) if produced_cex and not end_of_cex:
print(line, file=wit_file)
if line == ".": if line == ".":
end_of_cex = True end_of_cex = True
return None
if line.startswith("u"): if line.startswith("u"):
return "No CEX up to depth %d." % (int(line[1:])-1) return "No CEX up to depth %d." % (int(line[1:])-1)
if line in ["0", "1", "2"]: if solver_args[0] == "btormc":
print(line, file=aiw_file) if "bad state properties at bound" in line:
if line == "0": task_status = "PASS" return line
if line == "1": task_status = "FAIL" if "deleting model checker:" in line:
if line == "2": task_status = "UNKNOWN" if task_status is None:
task_status = "PASS"
return line
if not produced_cex or end_of_cex:
print(line, file=task.logfile)
return None return None
def exit_callback(retcode): def exit_callback(retcode):
if solver_args[0] not in ["avy"]: assert retcode == 0
assert retcode == 0
assert task_status is not None assert task_status is not None
aiw_file.close() wit_file.close()
job.update_status(task_status) job.update_status(task_status)
job.log("engine_%d: Status returned by engine: %s" % (engine_idx, task_status)) job.log("engine_%d: Status returned by engine: %s" % (engine_idx, task_status))
@ -89,7 +93,7 @@ def run(mode, job, engine_idx, engine):
if mode == "live": if mode == "live":
task2 = SbyTask(job, "engine_%d" % engine_idx, job.model("smt2"), task2 = SbyTask(job, "engine_%d" % engine_idx, job.model("smt2"),
("cd %s; %s -g -s %s%s --noprogress --dump-vcd engine_%d/trace.vcd --dump-vlogtb engine_%d/trace_tb.v " + ("cd %s; %s -g -s %s%s --noprogress --dump-vcd engine_%d/trace.vcd --dump-vlogtb engine_%d/trace_tb.v " +
"--dump-smtc engine_%d/trace.smtc --aig model/design_btor.aim:engine_%d/trace.aiw model/design_smt2.smt2") % "--dump-smtc engine_%d/trace.smtc --btorwit model/design_btor.btor:engine_%d/trace.wit model/design_smt2.smt2") %
(job.workdir, job.exe_paths["smtbmc"], job.opt_aigsmt, (job.workdir, job.exe_paths["smtbmc"], job.opt_aigsmt,
"" if job.opt_tbtop is None else " --vlogtb-top %s" % job.opt_tbtop, "" if job.opt_tbtop is None else " --vlogtb-top %s" % job.opt_tbtop,
engine_idx, engine_idx, engine_idx, engine_idx), engine_idx, engine_idx, engine_idx, engine_idx),
@ -97,7 +101,7 @@ def run(mode, job, engine_idx, engine):
else: else:
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%s --noprogress --append %d --dump-vcd engine_%d/trace.vcd --dump-vlogtb engine_%d/trace_tb.v " + ("cd %s; %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_btor.aim:engine_%d/trace.aiw model/design_smt2.smt2") % "--dump-smtc engine_%d/trace.smtc --btorwit model/design_btor.btor:engine_%d/trace.wit model/design_smt2.smt2") %
(job.workdir, job.exe_paths["smtbmc"], job.opt_aigsmt, (job.workdir, job.exe_paths["smtbmc"], job.opt_aigsmt,
"" if job.opt_tbtop is None else " --vlogtb-top %s" % job.opt_tbtop, "" if job.opt_tbtop is None else " --vlogtb-top %s" % job.opt_tbtop,
job.opt_append, engine_idx, engine_idx, engine_idx, engine_idx), job.opt_append, engine_idx, engine_idx, engine_idx, engine_idx),