From 180e07f9c4db7c23f17773b05251fc9cc5b68093 Mon Sep 17 00:00:00 2001 From: "N. Engelhardt" Date: Wed, 25 Mar 2020 15:53:55 +0100 Subject: [PATCH] add btor cover mode; use btorsim for vcd generation Signed-off-by: N. Engelhardt --- sbysrc/sby_core.py | 4 +- sbysrc/sby_engine_btor.py | 139 +++++++++++++++++++------------------- sbysrc/sby_mode_cover.py | 4 ++ 3 files changed, 76 insertions(+), 71 deletions(-) diff --git a/sbysrc/sby_core.py b/sbysrc/sby_core.py index e27a5c2..d3b0b1e 100644 --- a/sbysrc/sby_core.py +++ b/sbysrc/sby_core.py @@ -409,15 +409,15 @@ class SbyJob: print("flatten", file=f) print("setundef -undriven -anyseq", file=f) print("setattr -unset keep", file=f) - print("delete -output", file=f) print("opt -full", file=f) if "_syn" in model_name: print("techmap", file=f) print("opt -fast", file=f) print("abc", file=f) print("opt_clean", file=f) + print("delete -output", file=f) print("stat", file=f) - print("write_btor design_{}.btor".format(model_name), file=f) + print("write_btor {}-i design_{m}.info design_{m}.btor".format("-c " if self.opt_mode == "cover" else "", m=model_name), file=f) task = SbyTask(self, model_name, self.model("nomem" if "_nomem" in model_name else "base"), "cd {}/model; {} -ql design_{s}.log design_{s}.ys".format(self.workdir, self.exe_paths["yosys"], s=model_name)) diff --git a/sbysrc/sby_engine_btor.py b/sbysrc/sby_engine_btor.py index 1130a3a..e3a7247 100644 --- a/sbysrc/sby_engine_btor.py +++ b/sbysrc/sby_engine_btor.py @@ -29,7 +29,7 @@ def run(mode, job, engine_idx, engine): job.error("Unexpected BTOR engine options.") if solver_args[0] == "btormc": - solver_cmd = job.exe_paths["btormc"] + " --stop-first -v 1 -kmax {}".format(job.opt_depth - 1) + solver_cmd = job.exe_paths["btormc"] + " --stop-first {} -v 1 -kmax {}".format(0 if mode == "cover" else 1, job.opt_depth - 1) if job.opt_skip is not None: solver_cmd += " -kmin {}".format(job.opt_skip) solver_cmd += " ".join([""] + solver_args[1:]) @@ -41,24 +41,39 @@ def run(mode, job, engine_idx, engine): "cd {}; {} model/design_btor.btor".format(job.workdir, solver_cmd), logfile=open("{}/engine_{}/logfile.txt".format(job.workdir, engine_idx), "w")) - task_status = None - produced_cex = False - end_of_cex = False - wit_file = open("{}/engine_{}/trace.wit".format(job.workdir, engine_idx), "w") + solver_status = None + produced_cex = 0 + expected_cex = 1 + wit_file = None def output_callback(line): - nonlocal task_status + nonlocal solver_status nonlocal produced_cex - nonlocal end_of_cex - - if not end_of_cex and not produced_cex and line == "sat": - produced_cex = True - task_status = "FAIL" + nonlocal expected_cex + nonlocal wit_file + + if mode == "cover": + match = re.search(r"calling BMC on ([0-9]+) properties", line) + if match: + expected_cex = int(match[1]) + assert expected_cex > 0 + assert produced_cex == 0 + + if (produced_cex < expected_cex) and line == "sat": + assert wit_file == None + if expected_cex == 1: + wit_file = open("{}/engine_{}/trace.wit".format(job.workdir, engine_idx), "w") + else: + wit_file = open("{}/engine_{}/trace{}.wit".format(job.workdir, engine_idx, produced_cex), "w") - if produced_cex and not end_of_cex: + if wit_file: print(line, file=wit_file) if line == ".": - end_of_cex = True + produced_cex += 1 + wit_file.close() + wit_file = None + if produced_cex == expected_cex: + solver_status = "sat" if line.startswith("u"): return "No CEX up to depth {}.".format(int(line[1:])-1) @@ -71,22 +86,32 @@ def run(mode, job, engine_idx, engine): if "bad state properties at bound" in line: return line if "deleting model checker:" in line: - if task_status is None: - task_status = "PASS" + if solver_status is None: + solver_status = "unsat" return line - if not produced_cex or end_of_cex: + if not wit_file: print(line, file=task.logfile) return None def exit_callback(retcode): assert retcode == 0 - assert task_status is not None + assert solver_status is not None + + if solver_status == "unsat": + if expected_cex == 1: + with open("{}/engine_{}/trace.wit".format(job.workdir, engine_idx), "w") as wit_file: + print("unsat", file=wit_file) + else: + for i in range(produced_cex, expected_cex): + with open("{}/engine_{}/trace{}.wit".format(job.workdir, engine_idx, i), "w") as wit_file: + print("unsat", file=wit_file) - if task_status == "PASS": - print("unsat", file=wit_file) - wit_file.close() + if mode == "cover": + task_status = "PASS" if solver_status == "sat" else "FAIL" + else: + task_status = "FAIL" if solver_status == "sat" else "PASS" job.update_status(task_status) job.log("engine_{}: Status returned by engine: {}".format(engine_idx, task_status)) @@ -94,66 +119,42 @@ def run(mode, job, engine_idx, engine): job.terminate() - if task_status == "FAIL" and job.opt_aigsmt != "none": - if produced_cex: - has_arrays = False - - with open("{}/model/design_btor.btor".format(job.workdir), "r") as f: - for line in f: - line = line.split() - if len(line) == 5 and line[1] == "sort" and line[2] == "array": - has_arrays = True - break - - if has_arrays: - setupcmd = "cd {};".format(job.workdir) - finalwit = "engine_{}/trace.wit".format(engine_idx) - else: - setupcmd = "cd {}; { echo sat; btorsim --states model/design_btor.btor engine_{i}/trace.wit; } > engine_{i}/simtrace.wit &&".format(job.workdir, i=engine_idx) - finalwit = "engine_{}/simtrace.wit".format(engine_idx) - - if mode == "live": - task2 = SbyTask(job, "engine_{}".format(engine_idx), job.model("smt2"), - ("{} {} -g -s {}{} --noprogress --dump-vcd engine_{i}/trace.vcd --dump-vlogtb engine_{i}/trace_tb.v " + - "--dump-smtc engine_{i}/trace.smtc --btorwit {} model/design_smt2.smt2").format(setupcmd, job.exe_paths["smtbmc"], job.opt_aigsmt, "" if job.opt_tbtop is None else " --vlogtb-top {}".format(job.opt_tbtop), finalwit, i=engine_idx), - logfile=open("{}/engine_{}/logfile2.txt".format(job.workdir, engine_idx), "w")) - else: - task2 = SbyTask(job, "engine_{}".format(engine_idx), job.model("smt2"), - ("{} {} -s {}{} --noprogress --append {} --dump-vcd engine_{i}/trace.vcd --dump-vlogtb engine_{i}/trace_tb.v " + - "--dump-smtc engine_{i}/trace.smtc --btorwit {} model/design_smt2.smt2").format - (setupcmd, job.exe_paths["smtbmc"], job.opt_aigsmt, - "" if job.opt_tbtop is None else " --vlogtb-top {}".format(job.opt_tbtop), - job.opt_append, finalwit, i=engine_idx), - logfile=open("{}/engine_{}/logfile2.txt".format(job.workdir, engine_idx), "w")) - - task2_status = None + if produced_cex == 0: + job.log("engine_{}: Engine did not produce a counter example.".format(engine_idx)) + elif produced_cex == 1: + task2 = SbyTask(job, "engine_{}".format(engine_idx), job.model("btor"), + "cd {dir}; btorsim -c --vcd engine_{idx}/trace.vcd --hierarchical-symbols model/design_btor.btor engine_{idx}/trace.wit".format(dir=job.workdir, idx=engine_idx), + logfile=open("{dir}/engine_{idx}/logfile2.txt".format(dir=job.workdir, idx=engine_idx), "w")) - def output_callback2(line): - nonlocal task2_status + def output_callback2(line): + return line - match = re.match(r"^## [0-9: ]+ Status: FAILED", line) - if match: task2_status = "FAIL" + def exit_callback2(line): + assert retcode == 0 - match = re.match(r"^## [0-9: ]+ Status: PASSED", line) - if match: task2_status = "PASS" + if os.path.exists("{}/engine_{}/trace.vcd".format(job.workdir, engine_idx)): + job.summary.append("counterexample trace: {}/engine_{}/trace.vcd".format(job.workdir, engine_idx)) + task2.output_callback = output_callback2 + task2.exit_callback = exit_callback2 + + else: + for i in range(produced_cex): + task2 = SbyTask(job, "engine_{}".format(engine_idx), job.model("btor"), + "cd {dir}; btorsim -c --vcd engine_{idx}/trace{i}.vcd --hierarchical-symbols model/design_btor.btor engine_{idx}/trace{i}.wit".format(dir=job.workdir, idx=engine_idx, i=i), + logfile=open("{dir}/engine_{idx}/logfile{}.txt".format(i+2, dir=job.workdir, idx=engine_idx), "w")) + + def output_callback2(line): return line def exit_callback2(line): - assert task2_status is not None - if mode == "live": - assert task2_status == "PASS" - else: - assert task2_status == "FAIL" + assert retcode == 0 - if os.path.exists("{}/engine_{}/trace.vcd".format(job.workdir, engine_idx)): - job.summary.append("counterexample trace: {}/engine_{}/trace.vcd".format(job.workdir, engine_idx)) + if os.path.exists("{}/engine_{}/trace{}.vcd".format(job.workdir, engine_idx, i)): + job.summary.append("counterexample trace: {}/engine_{}/trace{}.vcd".format(job.workdir, engine_idx, i)) task2.output_callback = output_callback2 task2.exit_callback = exit_callback2 - else: - job.log("engine_{}: Engine did not produce a counter example.".format(engine_idx)) - task.output_callback = output_callback task.exit_callback = exit_callback diff --git a/sbysrc/sby_mode_cover.py b/sbysrc/sby_mode_cover.py index b5dc022..dbefac2 100644 --- a/sbysrc/sby_mode_cover.py +++ b/sbysrc/sby_mode_cover.py @@ -34,5 +34,9 @@ def run(job): import sby_engine_smtbmc sby_engine_smtbmc.run("cover", job, engine_idx, engine) + elif engine[0] == "btor": + import sby_engine_btor + sby_engine_btor.run("cover", job, engine_idx, engine) + else: job.error("Invalid engine '{}' for cover mode.".format(engine[0])) -- 2.30.2