From 5125128bbdd1246bd5aa6dc51781168b6c590c3d Mon Sep 17 00:00:00 2001
From: Clifford Wolf <clifford@clifford.at>
Date: Mon, 30 Jan 2017 12:32:49 +0100
Subject: [PATCH] Added prove mode support via "abc pdr"

---
 sbysrc/sby_core.py          |  4 +++
 sbysrc/sby_engine_abc.py    | 22 ++++++++++++----
 sbysrc/sby_engine_smtbmc.py |  2 ++
 sbysrc/sby_mode_prove.py    | 52 +++++++++++++++++++++++++++++++++++++
 4 files changed, 75 insertions(+), 5 deletions(-)
 create mode 100644 sbysrc/sby_mode_prove.py

diff --git a/sbysrc/sby_core.py b/sbysrc/sby_core.py
index f18138a..d4903b9 100644
--- a/sbysrc/sby_core.py
+++ b/sbysrc/sby_core.py
@@ -332,6 +332,10 @@ class SbyJob:
             import sby_mode_bmc
             sby_mode_bmc.run(self)
 
+        if self.options["mode"] == "prove":
+            import sby_mode_prove
+            sby_mode_prove.run(self)
+
         else:
             assert False
 
diff --git a/sbysrc/sby_engine_abc.py b/sbysrc/sby_engine_abc.py
index 42a8d58..1b122ea 100644
--- a/sbysrc/sby_engine_abc.py
+++ b/sbysrc/sby_engine_abc.py
@@ -20,11 +20,20 @@ import re, os, getopt
 from sby_core import SbyTask
 
 def run(mode, job, engine_idx, engine):
-    assert engine == ["abc", "bmc3"]
+    if mode == "bmc":
+        assert engine == ["abc", "bmc3"]
+        abc_command = "bmc3 -F %d -v" % job.opt_depth
+
+    elif mode == "prove":
+        assert engine == ["abc", "pdr"]
+        abc_command = "pdr"
+
+    else:
+        assert False
 
     task = SbyTask(job, "engine_%d" % engine_idx, job.model("aig"),
-            ("cd %s; yosys-abc -c 'read_aiger model/design_aiger.aig; fold; strash; bmc3 -F %d -v; " +
-             "undc -c; write_cex -a engine_%d/trace.aiw'") % (job.workdir, job.opt_depth, engine_idx),
+            ("cd %s; yosys-abc -c 'read_aiger model/design_aiger.aig; fold; strash; %s; " +
+             "write_cex -a engine_%d/trace.aiw'") % (job.workdir, abc_command, engine_idx),
             logfile=open("%s/engine_%d/logfile.txt" % (job.workdir, engine_idx), "w"))
 
     task_status = None
@@ -41,6 +50,9 @@ def run(mode, job, engine_idx, engine):
         match = re.match(r"^No output asserted in [0-9]+ frames.", line)
         if match: task_status = "PASS"
 
+        match = re.match(r"^Property proved.", line)
+        if match: task_status = "PASS"
+
     def exit_callback(retcode):
         assert retcode == 0
         assert task_status is not None
@@ -53,9 +65,9 @@ def run(mode, job, engine_idx, engine):
 
         if job.status == "FAIL":
             task2 = SbyTask(job, "engine_%d" % engine_idx, job.model("smt2"),
-                    ("cd %s; yosys-smtbmc --noprogress -t %d --dump-vcd engine_%d/trace.vcd --dump-vlogtb engine_%d/trace_tb.v " +
+                    ("cd %s; yosys-smtbmc --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 --aig-noheader model/design_smt2.smt2") %
-                            (job.workdir, job.opt_depth, engine_idx, engine_idx, engine_idx, engine_idx),
+                            (job.workdir, engine_idx, engine_idx, engine_idx, engine_idx),
                     logfile=open("%s/engine_%d/logfile2.txt" % (job.workdir, engine_idx), "w"))
 
             task2_status = None
diff --git a/sbysrc/sby_engine_smtbmc.py b/sbysrc/sby_engine_smtbmc.py
index 8143db1..8b30255 100644
--- a/sbysrc/sby_engine_smtbmc.py
+++ b/sbysrc/sby_engine_smtbmc.py
@@ -20,6 +20,8 @@ import re, os, getopt
 from sby_core import SbyTask
 
 def run(mode, job, engine_idx, engine):
+    assert mode == "bmc"
+
     smtbmc_opts = []
     nomem_opt = False
     syn_opt = False
diff --git a/sbysrc/sby_mode_prove.py b/sbysrc/sby_mode_prove.py
new file mode 100644
index 0000000..45b05e7
--- /dev/null
+++ b/sbysrc/sby_mode_prove.py
@@ -0,0 +1,52 @@
+#
+# 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(job):
+    job.opt_depth = 20
+
+    if "depth" in job.options:
+        job.opt_depth = int(job.options["depth"])
+
+    job.basecase_done = False
+    job.induction_done = False
+    job.basecase_tasks = list()
+    job.induction_tasks = list()
+
+    for engine_idx in range(len(job.engines)):
+        engine = job.engines[engine_idx]
+        assert len(engine) > 0
+
+        job.log("engine_%d: %s" % (engine_idx, " ".join(engine)))
+        os.makedirs("%s/engine_%d" % (job.workdir, engine_idx))
+
+        if engine[0] == "smtbmc":
+            import sby_engine_smtbmc
+            sby_engine_smtbmc.run("prove", job, engine_idx, engine)
+
+        elif engine[0] == "abc":
+            import sby_engine_abc
+            sby_engine_abc.run("prove", job, engine_idx, engine)
+
+        else:
+            assert False
+
+    job.taskloop()
+
-- 
2.30.2