From ffeee1a11fc1ebb623ca1460a60edd6502dd9ed8 Mon Sep 17 00:00:00 2001
From: Clifford Wolf <clifford@clifford.at>
Date: Mon, 30 Jan 2017 12:59:20 +0100
Subject: [PATCH] Add smtbmc prove support

---
 sbysrc/sby_core.py          |  2 +-
 sbysrc/sby_engine_smtbmc.py | 82 +++++++++++++++++++++++++++++++------
 sbysrc/sby_mode_prove.py    |  6 ++-
 3 files changed, 74 insertions(+), 16 deletions(-)

diff --git a/sbysrc/sby_core.py b/sbysrc/sby_core.py
index d4903b9..3c713f8 100644
--- a/sbysrc/sby_core.py
+++ b/sbysrc/sby_core.py
@@ -332,7 +332,7 @@ class SbyJob:
             import sby_mode_bmc
             sby_mode_bmc.run(self)
 
-        if self.options["mode"] == "prove":
+        elif self.options["mode"] == "prove":
             import sby_mode_prove
             sby_mode_prove.run(self)
 
diff --git a/sbysrc/sby_engine_smtbmc.py b/sbysrc/sby_engine_smtbmc.py
index 8b30255..65ebbc6 100644
--- a/sbysrc/sby_engine_smtbmc.py
+++ b/sbysrc/sby_engine_smtbmc.py
@@ -20,8 +20,6 @@ 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
@@ -43,11 +41,34 @@ def run(mode, job, engine_idx, engine):
     if syn_opt: model_name += "_syn"
     if nomem_opt: model_name += "_nomem"
 
-    task = SbyTask(job, "engine_%d" % engine_idx, job.model(model_name),
-            ("cd %s; yosys-smtbmc --noprogress %s -t %d --dump-vcd engine_%d/trace.vcd --dump-vlogtb engine_%d/trace_tb.v " +
-             "--dump-smtc engine_%d/trace.smtc model/design_smt2.smt2") %
-                    (job.workdir, " ".join(smtbmc_opts), job.opt_depth, engine_idx, engine_idx, engine_idx),
-            logfile=open("%s/engine_%d/logfile.txt" % (job.workdir, engine_idx), "w"))
+    if mode == "prove":
+        run("prove_basecase", job, engine_idx, engine)
+        run("prove_induction", job, engine_idx, engine)
+        return
+
+    taskname = "engine_%d" % engine_idx
+    trace_prefix = "engine_%d/trace" % engine_idx
+    logfile_prefix = "%s/engine_%d/logfile" % (job.workdir, engine_idx)
+
+    if mode == "prove_basecase":
+        taskname += ".basecase"
+
+    if mode == "prove_induction":
+        taskname += ".induction"
+        trace_prefix += "_induct"
+        logfile_prefix += "_induct"
+        smtbmc_opts.append("-i")
+
+    task = SbyTask(job, taskname, job.model(model_name),
+            ("cd %s; yosys-smtbmc --noprogress %s -t %d --dump-vcd %s.vcd --dump-vlogtb %s_tb.v --dump-smtc %s.smtc model/design_smt2.smt2") %
+                    (job.workdir, " ".join(smtbmc_opts), job.opt_depth, trace_prefix, trace_prefix, trace_prefix),
+            logfile=open(logfile_prefix + ".txt", "w"))
+
+    if mode == "prove_basecase":
+        job.basecase_tasks.append(task)
+
+    if mode == "prove_induction":
+        job.induction_tasks.append(task)
 
     task_status = None
 
@@ -63,14 +84,49 @@ def run(mode, job, engine_idx, engine):
     def exit_callback(retcode):
         assert task_status is not None
 
-        job.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), job.status))
+        if mode == "bmc":
+            job.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), job.status))
+
+            if job.status == "FAIL":
+                job.summary.append("counterexample trace: %s/engine_%d/trace.vcd" % (job.workdir, engine_idx))
+
+            job.terminate()
 
-        if job.status == "FAIL":
-            job.summary.append("counterexample trace: %s/engine_%d/trace.vcd" % (job.workdir, engine_idx))
+        elif mode in ["prove_basecase", "prove_induction"]:
+            job.log("engine_%d: Status returned by engine for %s: %s" % (engine_idx, mode.split("_")[1], task_status))
+            job.summary.append("engine_%d (%s) returned %s for %s" % (engine_idx, " ".join(engine), task_status, mode.split("_")[1]))
 
-        job.terminate()
+            if mode == "prove_basecase":
+                for task in job.basecase_tasks:
+                    task.terminate()
+
+                if task_status == "PASS":
+                    job.basecase_pass = True
+
+                else:
+                    job.status = task_status
+                    job.summary.append("counterexample trace: %s/engine_%d/trace.vcd" % (job.workdir, engine_idx))
+                    job.terminate()
+
+            elif mode == "prove_induction":
+                for task in job.induction_tasks:
+                    task.terminate()
+
+                if task_status == "PASS":
+                    job.induction_pass = True
+
+            else:
+                assert False
+
+            if job.basecase_pass and job.induction_pass:
+                job.status = "PASS"
+                job.summary.append("successful proof by k-induction.")
+                job.terminate()
+
+        else:
+            assert False
 
     task.output_callback = output_callback
     task.exit_callback = exit_callback
diff --git a/sbysrc/sby_mode_prove.py b/sbysrc/sby_mode_prove.py
index 45b05e7..2491404 100644
--- a/sbysrc/sby_mode_prove.py
+++ b/sbysrc/sby_mode_prove.py
@@ -25,8 +25,10 @@ def run(job):
     if "depth" in job.options:
         job.opt_depth = int(job.options["depth"])
 
-    job.basecase_done = False
-    job.induction_done = False
+    job.status = "UNKNOWN"
+
+    job.basecase_pass = False
+    job.induction_pass = False
     job.basecase_tasks = list()
     job.induction_tasks = list()
 
-- 
2.30.2