Add aiger engine

.gitignore

@@ -1,4 +1,4 @@
 /docs/build
-/sbysrc/demo
+/sbysrc/demo[0-9]
 /sbysrc/__pycache__
 

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

sbysrc/sby.py

@@ -43,14 +43,15 @@ sby [options] <jobname>.sby
     --yosys <path_to_executable>
     --abc <path_to_executable>
     --smtbmc <path_to_executable>
-    --sprove <path_to_executable>
+    --suprove <path_to_executable>
+    --avy <path_to_executable>
         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()
 

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
 

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"

sbysrc/sby_engine_aiger.py

@@ -0,0 +1,107 @@
+#
+# SymbiYosys (sby) -- Front-end for Yosys-based formal verification flows
+#
+# Copyright (C) 2016  Clifford Wolf <clifford@clifford.at>
+#
+# 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
+

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
 

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)