From 79634d5016051add0fed4e670c81f80a931f38ff Mon Sep 17 00:00:00 2001
From: George Rennie <georgerennie@gmail.com>
Date: Tue, 16 Nov 2021 15:16:32 +0000
Subject: [PATCH] Add --anybase option to smtbmc engine

This uses the smtbmc -g flag to generate an arbitrary trace for the
basecase in prove mode, instead of one starting with the initial
conditions. This behaves similarly to the basecase assertions in yosys'
equiv_induct.
---
 sbysrc/sby_engine_smtbmc.py | 30 +++++++++++++++++++++++-------
 1 file changed, 23 insertions(+), 7 deletions(-)

diff --git a/sbysrc/sby_engine_smtbmc.py b/sbysrc/sby_engine_smtbmc.py
index c21a3f7..3f964ff 100644
--- a/sbysrc/sby_engine_smtbmc.py
+++ b/sbysrc/sby_engine_smtbmc.py
@@ -29,12 +29,14 @@ def run(mode, job, engine_idx, engine):
     stdt_opt = False
     dumpsmt2 = False
     progress = False
+    anybase = False
     basecase_only = False
     induction_only = False
     random_seed = None
 
     opts, args = getopt.getopt(engine[1:], "", ["nomem", "syn", "stbv", "stdt", "presat",
-            "nopresat", "unroll", "nounroll", "dumpsmt2", "progress", "basecase", "induction", "seed="])
+            "nopresat", "unroll", "nounroll", "dumpsmt2", "progress", "anybase",
+            "basecase", "induction", "seed="])
 
     for o, a in opts:
         if o == "--nomem":
@@ -57,6 +59,8 @@ def run(mode, job, engine_idx, engine):
             dumpsmt2 = True
         elif o == "--progress":
             progress = True
+        elif o == "--anybase":
+            anybase = True
         elif o == "--basecase":
             if induction_only:
                 job.error("smtbmc options --basecase and --induction are exclusive.")
@@ -114,6 +118,8 @@ def run(mode, job, engine_idx, engine):
     if mode == "prove_basecase":
         taskname += ".basecase"
         logfile_prefix += "_basecase"
+        if anybase:
+            smtbmc_opts.append("-g")
 
     if mode == "prove_induction":
         taskname += ".induction"
@@ -218,14 +224,24 @@ def run(mode, job, engine_idx, engine):
                 for task in job.basecase_tasks:
                     task.terminate()
 
-                if task_status == "PASS":
-                    job.basecase_pass = True
+                if not anybase:
+                    if task_status == "PASS":
+                        job.basecase_pass = True
 
+                    else:
+                        job.update_status(task_status)
+                        if os.path.exists(f"{job.workdir}/engine_{engine_idx}/trace.vcd"):
+                            job.summary.append(f"counterexample trace: {job.workdir}/engine_{engine_idx}/trace.vcd")
+                        job.terminate()
                 else:
-                    job.update_status(task_status)
-                    if os.path.exists(f"{job.workdir}/engine_{engine_idx}/trace.vcd"):
-                        job.summary.append(f"counterexample trace: {job.workdir}/engine_{engine_idx}/trace.vcd")
-                    job.terminate()
+                    if task_status == "PASS":
+                        job.basecase_pass = True
+                        if os.path.exists(f"{job.workdir}/engine_{engine_idx}/trace.vcd"):
+                            job.summary.append(f"basecase trace: {job.workdir}/engine_{engine_idx}/trace.vcd")
+
+                    else:
+                        job.update_status(task_status)
+                        job.terminate()
 
             elif mode == "prove_induction":
                 for task in job.induction_tasks: