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

Merge pull request #88 from YosysHQ/claire/cosa2

Browse source 
Add support for cosa2 BTOR solver
This commit is contained in:
clairexen 2020-05-18 17:01:19 +02:00 committed by GitHub
parent 9fdece3dab c7668de077
commit 13fef4a710
No known key found for this signature in database
GPG key ID: 4AEE18F83AFDEB23
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 = []

27
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,17 +114,23 @@ def run(mode, job, engine_idx, engine):
def output_callback(line):
if mode == "cover":
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
if common_state.expected_cex == 1:
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,9 +153,7 @@ 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
@ -159,12 +166,22 @@ def run(mode, job, engine_idx, engine):
common_state.solver_status = "unsat"
return line
if not common_state.wit_file:
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
print(line, file=task.logfile)
return None
def exit_callback(retcode):
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