From: Jannis Harder <me@jix.one>
Date: Mon, 21 Mar 2022 17:36:09 +0000 (+0100)
Subject: Initial support for the new smtbmc --keep-going option
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=7824460e27eb65cf240ab92e306b4be57eb0b161;p=SymbiYosys.git

Initial support for the new smtbmc --keep-going option

So far this only passes on the option and adjusts the trace_prefix to
support multiple numbered traces. Further changes are needed to
correctly associate individual traces with the assertions failing in
that trace.
---

diff --git a/sbysrc/sby_engine_smtbmc.py b/sbysrc/sby_engine_smtbmc.py
index 492e2a5..9b7ff2b 100644
--- a/sbysrc/sby_engine_smtbmc.py
+++ b/sbysrc/sby_engine_smtbmc.py
@@ -31,11 +31,12 @@ def run(mode, task, engine_idx, engine):
     progress = False
     basecase_only = False
     induction_only = False
+    keep_going = False
     random_seed = None
     task.precise_prop_status = True
 
     opts, args = getopt.getopt(engine[1:], "", ["nomem", "syn", "stbv", "stdt", "presat",
-            "nopresat", "unroll", "nounroll", "dumpsmt2", "progress", "basecase", "induction", "seed="])
+            "nopresat", "unroll", "nounroll", "dumpsmt2", "progress", "basecase", "induction", "keep-going", "seed="])
 
     for o, a in opts:
         if o == "--nomem":
@@ -66,6 +67,10 @@ def run(mode, task, engine_idx, engine):
             if basecase_only:
                 task.error("smtbmc options --basecase and --induction are exclusive.")
             induction_only = True
+        elif o == "--keep-going":
+            if mode not in ("bmc", "prove", "prove_basecase", "prove_induction"):
+                task.error("smtbmc option --keep-going is only supported in bmc and prove mode.")
+            keep_going = True
         elif o == "--seed":
             random_seed = a
         else:
@@ -126,6 +131,10 @@ def run(mode, task, engine_idx, engine):
         smtbmc_opts.append("-c")
         trace_prefix += "%"
 
+    if keep_going:
+        smtbmc_opts.append("--keep-going")
+        trace_prefix += "%"
+
     if dumpsmt2:
         smtbmc_opts += ["--dump-smt2", trace_prefix.replace("%", "") + ".smt2"]