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

Add support for cosa2 BTOR solver

Browse source 
Signed-off-by: Claire Wolf <claire@symbioticeda.com>
This commit is contained in:
Claire Wolf 2020-05-18 15:13:56 +02:00
parent 9fdece3dab
commit c7668de077
3 changed files with 47 additions and 24 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
sbysrc/sby.py
View file

@ -58,6 +58,8 @@ parser.add_argument("--aigbmc", metavar="<path_to_executable>",
parser.add_argument("--avy", metavar="<path_to_executable>",
action=DictAction, dest="exe_paths")
parser.add_argument("--btormc", metavar="<path_to_executable>",
action=DictAction, dest="exe_paths")
parser.add_argument("--cosa2", metavar="<path_to_executable>",
action=DictAction, dest="exe_paths",
help="configure which executable to use for the respective tool")
parser.add_argument("--dumpcfg", action="store_true", dest="dump_cfg",

12
sbysrc/sby_core.py
View file

@ -90,15 +90,18 @@ class SbyTask:
else:
self.notify.append(next_task)
def log(self, line):
if line is not None and (self.noprintregex is None or not self.noprintregex.match(line)):
if self.logfile is not None:
print(line, file=self.logfile)
self.job.log("{}: {}".format(self.info, line))
def handle_output(self, line):
if self.terminated or len(line) == 0:
return
if self.output_callback is not None:
line = self.output_callback(line)
if line is not None and (self.noprintregex is None or not self.noprintregex.match(line)):
if self.logfile is not None:
print(line, file=self.logfile)
self.job.log("{}: {}".format(self.info, line))
self.log(line)
def handle_exit(self, retcode):
if self.terminated:
@ -222,6 +225,7 @@ class SbyJob:
"aigbmc": "aigbmc",
"avy": "avy",
"btormc": "btormc",
"cosa2": "cosa2",
}
self.tasks_running = []

57
sbysrc/sby_engine_btor.py
View file

@ -35,6 +35,9 @@ def run(mode, job, engine_idx, engine):
solver_cmd += " -kmin {}".format(job.opt_skip)
solver_cmd += " ".join([""] + solver_args[1:])
elif solver_args[0] == "cosa2":
solver_cmd = job.exe_paths["cosa2"] + " -v 1 -e bmc -k {}".format(job.opt_depth - 1)
else:
job.error("Invalid solver command {}.".format(solver_args[0]))
@ -111,10 +114,14 @@ def run(mode, job, engine_idx, engine):
def output_callback(line):
if mode == "cover":
match = re.search(r"calling BMC on ([0-9]+) properties", line)
if match:
common_state.expected_cex = int(match[1])
assert common_state.produced_cex == 0
if solver_args[0] == "btormc":
match = re.search(r"calling BMC on ([0-9]+) properties", line)
if match:
common_state.expected_cex = int(match[1])
assert common_state.produced_cex == 0
else:
job.error("engine_{}: BTOR solver '{}' is currently not supported in cover mode.".format(solver_args[0]))
if (common_state.produced_cex < common_state.expected_cex) and line == "sat":
assert common_state.wit_file == None
@ -122,6 +129,8 @@ def run(mode, job, engine_idx, engine):
common_state.wit_file = open("{}/engine_{}/trace.wit".format(job.workdir, engine_idx), "w")
else:
common_state.wit_file = open("{}/engine_{}/trace{}.wit".format(job.workdir, engine_idx, common_state.produced_cex), "w")
if solver_args[0] != "btormc":
task.log("Found satisfiability witness.")
if common_state.wit_file:
print(line, file=common_state.wit_file)
@ -130,7 +139,7 @@ def run(mode, job, engine_idx, engine):
suffix = ""
else:
suffix = common_state.produced_cex
task2 = SbyTask(job, "engine_{}".format(engine_idx), job.model("btor"),
task2 = SbyTask(job, "engine_{}_{}".format(engine_idx, common_state.produced_cex), job.model("btor"),
"cd {dir} ; btorsim -c --vcd engine_{idx}/trace{i}.vcd --hierarchical-symbols --info model/design_btor.info model/design_btor.btor engine_{idx}/trace{i}.wit".format(dir=job.workdir, idx=engine_idx, i=suffix),
logfile=open("{dir}/engine_{idx}/logfile2.txt".format(dir=job.workdir, idx=engine_idx), "w"))
task2.output_callback = output_callback2
@ -144,28 +153,36 @@ def run(mode, job, engine_idx, engine):
if common_state.produced_cex == common_state.expected_cex:
common_state.solver_status = "sat"
if line.startswith("u"):
return "No CEX up to depth {}.".format(int(line[1:])-1)
else:
if solver_args[0] == "btormc":
if "calling BMC on" in line:
return line
if "SATISFIABLE" in line:
return line
if "bad state properties at bound" in line:
return line
if "deleting model checker:" in line:
if common_state.solver_status is None:
common_state.solver_status = "unsat"
return line
if solver_args[0] == "btormc":
if "calling BMC on" in line:
return line
if "SATISFIABLE" in line:
return line
if "bad state properties at bound" in line:
return line
if "deleting model checker:" in line:
if common_state.solver_status is None:
common_state.solver_status = "unsat"
return line
elif solver_args[0] == "cosa2":
if line == "unknown":
if common_state.solver_status is None:
common_state.solver_status = "unsat"
return "No CEX found."
if line not in ["b0"]:
return line
if not common_state.wit_file:
print(line, file=task.logfile)
return None
def exit_callback(retcode):
assert retcode == 0
if solver_args[0] == "cosa2":
assert retcode in [1, 2]
else:
assert retcode == 0
if common_state.expected_cex != 0:
assert common_state.solver_status is not None