Add "append" option

diff --git a/sbysrc/sby_engine_abc.py b/sbysrc/sby_engine_abc.py
index 90f399ad474eff212f8eb253d2f5c5773cbbcc0d..c1d130c1e652e4586209f84d312a6f26614e4c98 100644 (file)
--- a/sbysrc/sby_engine_abc.py
+++ b/sbysrc/sby_engine_abc.py
@@ -81,9 +81,9 @@ def run(mode, job, engine_idx, engine):
 
         if task_status == "FAIL":
             task2 = SbyTask(job, "engine_%d" % engine_idx, job.model("smt2"),
-                    ("cd %s; %s -s %s --noprogress --dump-vcd engine_%d/trace.vcd --dump-vlogtb engine_%d/trace_tb.v " +
+                    ("cd %s; %s -s %s --noprogress --append %d --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.exe_paths["smtbmc"], job.opt_aigsmt, engine_idx, engine_idx, engine_idx, engine_idx),
+                            (job.workdir, job.exe_paths["smtbmc"], job.opt_aigsmt, job.opt_append, 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_aiger.py b/sbysrc/sby_engine_aiger.py
index 545f727fa6ad31148bff9291cdab7abdc8b2d257..3a7e87dba7a02820670640183bf82c743834badd 100644 (file)
--- a/sbysrc/sby_engine_aiger.py
+++ b/sbysrc/sby_engine_aiger.py
@@ -78,9 +78,9 @@ def run(mode, job, engine_idx, engine):
 
         if task_status == "FAIL":
             task2 = SbyTask(job, "engine_%d" % engine_idx, job.model("smt2"),
-                    ("cd %s; %s -s %s --noprogress --dump-vcd engine_%d/trace.vcd --dump-vlogtb engine_%d/trace_tb.v " +
+                    ("cd %s; %s -s %s --noprogress --append %d --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"], job.opt_aigsmt, engine_idx, engine_idx, engine_idx, engine_idx),
+                            (job.workdir, job.exe_paths["smtbmc"], job.opt_aigsmt, job,opt_append, 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 7cb37cd639d85fa9a1ab27039110afc4f7f99208..392fbea1f61589807630928370a49fd3fe742837 100644 (file)
--- a/sbysrc/sby_engine_smtbmc.py
+++ b/sbysrc/sby_engine_smtbmc.py
@@ -69,8 +69,8 @@ def run(mode, job, engine_idx, engine):
         trace_prefix += "%"
 
     task = SbyTask(job, taskname, job.model(model_name),
-            "cd %s; %s --noprogress %s -t %d --dump-vcd %s.vcd --dump-vlogtb %s_tb.v --dump-smtc %s.smtc model/design_%s.smt2" %
-                    (job.workdir, job.exe_paths["smtbmc"], " ".join(smtbmc_opts), job.opt_depth, trace_prefix, trace_prefix, trace_prefix, model_name),
+            "cd %s; %s --noprogress %s -t %d --append %d --dump-vcd %s.vcd --dump-vlogtb %s_tb.v --dump-smtc %s.smtc model/design_%s.smt2" %
+                    (job.workdir, job.exe_paths["smtbmc"], " ".join(smtbmc_opts), job.opt_depth, job.opt_append, trace_prefix, trace_prefix, trace_prefix, model_name),
             logfile=open(logfile_prefix + ".txt", "w"))
 
     if mode == "prove_basecase":

diff --git a/sbysrc/sby_mode_bmc.py b/sbysrc/sby_mode_bmc.py
index 2daa299eded3587a454935ad5e4f98976e66096e..33a03a0e31e396609f2f9af2e9db8d7d2e35e5ba 100644 (file)
--- a/sbysrc/sby_mode_bmc.py
+++ b/sbysrc/sby_mode_bmc.py
@@ -21,11 +21,15 @@ from sby_core import SbyTask
 
 def run(job):
     job.opt_depth = 20
+    job.opt_append = 0
     job.opt_aigsmt = "z3"
 
     if "depth" in job.options:
         job.opt_depth = int(job.options["depth"])
 
+    if "append" in job.options:
+        job.opt_append = int(job.options["append"])
+
     if "aigsmt" in job.options:
         job.opt_aigsmt = job.options["aigsmt"]
 

diff --git a/sbysrc/sby_mode_cover.py b/sbysrc/sby_mode_cover.py
index 78a59f9207cc5c97f5ba55bbffef48fa38705543..90ef93b48c8b179d29dbc158935207b154d907d9 100644 (file)
--- a/sbysrc/sby_mode_cover.py
+++ b/sbysrc/sby_mode_cover.py
@@ -21,10 +21,14 @@ from sby_core import SbyTask
 
 def run(job):
     job.opt_depth = 20
+    job.opt_append = 0
 
     if "depth" in job.options:
         job.opt_depth = int(job.options["depth"])
 
+    if "append" in job.options:
+        job.opt_append = int(job.options["append"])
+
     for engine_idx in range(len(job.engines)):
         engine = job.engines[engine_idx]
         assert len(engine) > 0

diff --git a/sbysrc/sby_mode_prove.py b/sbysrc/sby_mode_prove.py
index 26eb80d71d59f8fd943948c064651a063baa06ef..214f010abbd8532870027f8dea063b512560366f 100644 (file)
--- a/sbysrc/sby_mode_prove.py
+++ b/sbysrc/sby_mode_prove.py
@@ -21,11 +21,15 @@ from sby_core import SbyTask
 
 def run(job):
     job.opt_depth = 20
+    job.opt_append = 0
     job.opt_aigsmt = "z3"
 
     if "depth" in job.options:
         job.opt_depth = int(job.options["depth"])
 
+    if "append" in job.options:
+        job.opt_append = int(job.options["append"])
+
     if "aigsmt" in job.options:
         job.opt_aigsmt = job.options["aigsmt"]