From b5be4a575907b07156e9f4a15a12fea780085e86 Mon Sep 17 00:00:00 2001 From: Clifford Wolf Date: Sun, 19 Feb 2017 23:53:01 +0100 Subject: [PATCH] Add aiger engine --- .gitignore | 2 +- sbysrc/{demo.sby => demo1.sby} | 0 sbysrc/demo2.sby | 21 +++++++ sbysrc/sby.py | 9 +-- sbysrc/sby_core.py | 19 +++--- sbysrc/sby_engine_abc.py | 4 ++ sbysrc/sby_engine_aiger.py | 107 +++++++++++++++++++++++++++++++++ sbysrc/sby_engine_smtbmc.py | 2 + sbysrc/sby_mode_prove.py | 4 ++ 9 files changed, 153 insertions(+), 15 deletions(-) rename sbysrc/{demo.sby => demo1.sby} (100%) create mode 100644 sbysrc/demo2.sby create mode 100644 sbysrc/sby_engine_aiger.py diff --git a/.gitignore b/.gitignore index b0f28e2..e374fdc 100644 --- a/.gitignore +++ b/.gitignore @@ -1,4 +1,4 @@ /docs/build -/sbysrc/demo +/sbysrc/demo[0-9] /sbysrc/__pycache__ diff --git a/sbysrc/demo.sby b/sbysrc/demo1.sby similarity index 100% rename from sbysrc/demo.sby rename to sbysrc/demo1.sby diff --git a/sbysrc/demo2.sby b/sbysrc/demo2.sby new file mode 100644 index 0000000..1d5639c --- /dev/null +++ b/sbysrc/demo2.sby @@ -0,0 +1,21 @@ +[options] +mode prove +wait on + +[engines] +aiger suprove +aiger avy + +[script] +read_verilog -formal demo.v +prep -top top + +[file demo.v] +module top(input clk, input up, down); + reg [4:0] counter = 0; + always @(posedge clk) begin + if (up && counter != 10) counter <= counter + 1; + if (down && counter != 0) counter <= counter - 1; + end + assert property (counter != 15); +endmodule diff --git a/sbysrc/sby.py b/sbysrc/sby.py index 94ec952..e960240 100644 --- a/sbysrc/sby.py +++ b/sbysrc/sby.py @@ -43,14 +43,15 @@ sby [options] .sby --yosys --abc --smtbmc - --sprove + --suprove + --avy configure which executable to use for the respective tool """) sys.exit(1) try: opts, args = getopt.getopt(sys.argv[1:], "d:bf", ["yosys=", - "abc=", "smtbmc=", "sprove="]) + "abc=", "smtbmc=", "suprove="]) except: usage() @@ -67,8 +68,8 @@ for o, a in opts: exe_paths["abc"] = a elif o == "--smtbmc": exe_paths["smtbmc"] = a - elif o == "--sprove": - exe_paths["sprove"] = a + elif o == "--suprove": + exe_paths["suprove"] = a else: usage() diff --git a/sbysrc/sby_core.py b/sbysrc/sby_core.py index a1aaec3..dd1e380 100644 --- a/sbysrc/sby_core.py +++ b/sbysrc/sby_core.py @@ -52,12 +52,14 @@ class SbyTask: self.notify.append(next_task) def handle_output(self, line): - if self.terminated: + if self.terminated or len(line) == 0: return - if self.logfile is not None: - print(line, file=self.logfile) if self.output_callback is not None: - self.output_callback(line) + 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("%s: %s" % (self.info, line)) def handle_exit(self, retcode): if self.terminated: @@ -101,9 +103,6 @@ class SbyTask: break outs = (self.linebuffer + outs).strip() self.linebuffer = "" - if len(outs) == 0: continue - if self.noprintregex is None or not self.noprintregex.match(outs): - self.job.log("%s: %s" % (self.info, outs)) self.handle_output(outs) if self.p.poll() is not None: @@ -141,7 +140,8 @@ class SbyJob: "yosys": "yosys", "abc": "yosys-abc", "smtbmc": "yosys-smtbmc", - "sprove": "super_prove", + "suprove": "super_prove", + "avy": "avy", } self.tasks_running = [] @@ -254,8 +254,7 @@ class SbyJob: fds.append(task.p.stdout) try: - while select(fds, [], [], 1.0) == ([], [], []): - pass + select(fds, [], [], 1.0) == ([], [], []) except: pass diff --git a/sbysrc/sby_engine_abc.py b/sbysrc/sby_engine_abc.py index 4230620..092a176 100644 --- a/sbysrc/sby_engine_abc.py +++ b/sbysrc/sby_engine_abc.py @@ -67,6 +67,8 @@ def run(mode, job, engine_idx, engine): match = re.match(r"^Property proved.", line) if match: task_status = "PASS" + return line + def exit_callback(retcode): assert retcode == 0 assert task_status is not None @@ -95,6 +97,8 @@ def run(mode, job, engine_idx, engine): match = re.match(r"^## [0-9: ]+ Status: PASSED", line) if match: task2_status = "PASS" + return line + def exit_callback2(line): assert task2_status is not None assert task2_status == "FAIL" diff --git a/sbysrc/sby_engine_aiger.py b/sbysrc/sby_engine_aiger.py new file mode 100644 index 0000000..c1feebd --- /dev/null +++ b/sbysrc/sby_engine_aiger.py @@ -0,0 +1,107 @@ +# +# SymbiYosys (sby) -- Front-end for Yosys-based formal verification flows +# +# Copyright (C) 2016 Clifford Wolf +# +# Permission to use, copy, modify, and/or distribute this software for any +# purpose with or without fee is hereby granted, provided that the above +# copyright notice and this permission notice appear in all copies. +# +# THE SOFTWARE IS PROVIDED "AS IS" AND THE AUTHOR DISCLAIMS ALL WARRANTIES +# WITH REGARD TO THIS SOFTWARE INCLUDING ALL IMPLIED WARRANTIES OF +# MERCHANTABILITY AND FITNESS. IN NO EVENT SHALL THE AUTHOR BE LIABLE FOR +# ANY SPECIAL, DIRECT, INDIRECT, OR CONSEQUENTIAL DAMAGES OR ANY DAMAGES +# WHATSOEVER RESULTING FROM LOSS OF USE, DATA OR PROFITS, WHETHER IN AN +# ACTION OF CONTRACT, NEGLIGENCE OR OTHER TORTIOUS ACTION, ARISING OUT OF +# OR IN CONNECTION WITH THE USE OR PERFORMANCE OF THIS SOFTWARE. +# + +import re, os, getopt +from sby_core import SbyTask + +def run(mode, job, engine_idx, engine): + opts, solver_args = getopt.getopt(engine[1:], "", []) + assert len(solver_args) > 0 + + for o, a in opts: + assert False + + if solver_args[0] == "suprove": + solver_cmd = " ".join([job.exe_paths["suprove"]] + solver_args[1:]) + + elif solver_args[0] == "avy": + solver_cmd = " ".join([job.exe_paths["avy"], "--cex", "-"] + solver_args[1:]) + + else: + assert False + + task = SbyTask(job, "engine_%d" % engine_idx, job.model("aig"), + "cd %s; %s model/design_aiger.aig" % (job.workdir, solver_cmd), + logfile=open("%s/engine_%d/logfile.txt" % (job.workdir, engine_idx), "w")) + + task_status = None + aiw_file = open("%s/engine_%d/trace.aiw" % (job.workdir, engine_idx), "w") + + def output_callback(line): + nonlocal task_status + + if task_status is not None: + print(line, file=aiw_file) + return None + + if line.startswith("u"): + return "No CEX up to depth %d." % (int(line[1:])-1) + + if line in ["0", "1", "2"]: + print(line, file=aiw_file) + if line == "0": task_status = "PASS" + if line == "1": task_status = "FAIL" + if line == "2": task_status = "UNKNOWN" + + return None + + def exit_callback(retcode): + if solver_args[0] not in ["avy"]: + assert retcode == 0 + assert task_status is not None + + aiw_file.close() + + job.update_status(task_status) + job.log("engine_%d: Status returned by engine: %s" % (engine_idx, task_status)) + job.summary.append("engine_%d (%s) returned %s" % (engine_idx, " ".join(engine), task_status)) + + job.terminate() + + if task_status == "FAIL": + task2 = SbyTask(job, "engine_%d" % engine_idx, job.model("smt2"), + ("cd %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_aiger.aim:engine_%d/trace.aiw model/design_smt2.smt2") % + (job.workdir, job.exe_paths["smtbmc"], engine_idx, engine_idx, engine_idx, engine_idx), + logfile=open("%s/engine_%d/logfile2.txt" % (job.workdir, engine_idx), "w")) + + task2_status = None + + def output_callback2(line): + nonlocal task2_status + + match = re.match(r"^## [0-9: ]+ Status: FAILED", line) + if match: task2_status = "FAIL" + + match = re.match(r"^## [0-9: ]+ Status: PASSED", line) + if match: task2_status = "PASS" + + return line + + def exit_callback2(line): + assert task2_status is not None + assert task2_status == "FAIL" + + job.summary.append("counterexample trace: %s/engine_%d/trace.vcd" % (job.workdir, engine_idx)) + + task2.output_callback = output_callback2 + task2.exit_callback = exit_callback2 + + task.output_callback = output_callback + task.exit_callback = exit_callback + diff --git a/sbysrc/sby_engine_smtbmc.py b/sbysrc/sby_engine_smtbmc.py index 3977f2c..52ccb9c 100644 --- a/sbysrc/sby_engine_smtbmc.py +++ b/sbysrc/sby_engine_smtbmc.py @@ -86,6 +86,8 @@ def run(mode, job, engine_idx, engine): match = re.match(r"^## [0-9: ]+ Status: PASSED", line) if match: task_status = "PASS" + return line + def exit_callback(retcode): assert task_status is not None diff --git a/sbysrc/sby_mode_prove.py b/sbysrc/sby_mode_prove.py index 2491404..67cb7f2 100644 --- a/sbysrc/sby_mode_prove.py +++ b/sbysrc/sby_mode_prove.py @@ -43,6 +43,10 @@ def run(job): import sby_engine_smtbmc sby_engine_smtbmc.run("prove", job, engine_idx, engine) + elif engine[0] == "aiger": + import sby_engine_aiger + sby_engine_aiger.run("prove", job, engine_idx, engine) + elif engine[0] == "abc": import sby_engine_abc sby_engine_abc.run("prove", job, engine_idx, engine) -- 2.30.2