Add vcd option to make VCD writing optional

docs/source/reference.rst

@@ -146,6 +146,9 @@ options are:
 |                  |            | wait for all engines to return and check for            |
 |                  |            | consistency. Values: ``on``, ``off``. Default: ``off``  |
 +------------------+------------+---------------------------------------------------------+
+| ``vcd``          |   All      | Write VCD traces for counter-example or cover traces.   |
+|                  |            | Values: ``on``, ``off``. Default: ``on``                |
++------------------+------------+---------------------------------------------------------+
 | ``aigsmt``       |   All      | Which SMT2 solver to use for converting AIGER witnesses |
 |                  |            | to counter example traces. Use ``none`` to disable      |
 |                  |            | conversion of AIGER witnesses. Default: ``yices``       |

sbysrc/sby_core.py

@@ -986,6 +986,8 @@ class SbyTask(SbyConfig):
         self.handle_bool_option("wait", False)
         self.handle_int_option("timeout", None)
 
+        self.handle_bool_option("vcd", True)
+
         self.handle_str_option("smtc", None)
         self.handle_int_option("skip", None)
         self.handle_str_option("tbtop", None)

sbysrc/sby_engine_abc.py

@@ -89,15 +89,20 @@ def run(mode, task, engine_idx, engine):
         task.terminate()
 
         if proc_status == "FAIL" and task.opt_aigsmt != "none":
+            trace_prefix = f"engine_{engine_idx}/trace"
+            dump_flags = f"--dump-vcd {trace_prefix}.vcd " if task.opt_vcd else ""
+            dump_flags += f"--dump-yw {trace_prefix}.yw --dump-vlogtb {trace_prefix}_tb.v --dump-smtc {trace_prefix}.smtc"
+
             proc2 = SbyProc(
                 task,
                 f"engine_{engine_idx}",
                 task.model("smt2"),
-                ("cd {}; {} -s {}{} --noprogress --append {} --dump-vcd engine_{i}/trace.vcd --dump-vlogtb engine_{i}/trace_tb.v " +
+                ("cd {}; {} -s {}{} --noprogress --append {} {dump_flags} --aig model/design_aiger.aim:engine_{i}/trace.aiw --aig-noheader model/design_smt2.smt2").format
-                     "--dump-smtc engine_{i}/trace.smtc --aig model/design_aiger.aim:engine_{i}/trace.aiw --aig-noheader model/design_smt2.smt2").format
                             (task.workdir, task.exe_paths["smtbmc"], task.opt_aigsmt,
                             "" if task.opt_tbtop is None else f" --vlogtb-top {task.opt_tbtop}",
-                            task.opt_append, i=engine_idx),
+                            task.opt_append,
+                            dump_flags=dump_flags,
+                            i=engine_idx),
                 logfile=open(f"{task.workdir}/engine_{engine_idx}/logfile2.txt", "w")
             )
 

sbysrc/sby_engine_aiger.py

@@ -105,15 +105,19 @@ def run(mode, task, engine_idx, engine):
 
         if proc_status == "FAIL" and task.opt_aigsmt != "none":
             if produced_cex:
+                trace_prefix = f"engine_{engine_idx}/trace"
+                dump_flags = f"--dump-vcd {trace_prefix}.vcd " if task.opt_vcd else ""
+                dump_flags += f"--dump-yw {trace_prefix}.yw --dump-vlogtb {trace_prefix}_tb.v --dump-smtc {trace_prefix}.smtc"
+
                 if mode == "live":
                     proc2 = SbyProc(
                         task,
                         f"engine_{engine_idx}",
                         task.model("smt2"),
-                        ("cd {}; {} -g -s {}{} --noprogress --dump-vcd engine_{i}/trace.vcd --dump-vlogtb engine_{i}/trace_tb.v " +
+                        ("cd {}; {} -g -s {}{} --noprogress {dump_flags} --aig model/design_aiger.aim:engine_{i}/trace.aiw model/design_smt2.smt2").format
-                             "--dump-smtc engine_{i}/trace.smtc --dump-yw engine_{i}/trace.yw --aig model/design_aiger.aim:engine_{i}/trace.aiw model/design_smt2.smt2").format
                                     (task.workdir, task.exe_paths["smtbmc"], task.opt_aigsmt,
                                     "" if task.opt_tbtop is None else f" --vlogtb-top {task.opt_tbtop}",
+                                    dump_flags=dump_flags,
                                     i=engine_idx),
                         logfile=open(f"{task.workdir}/engine_{engine_idx}/logfile2.txt", "w")
                     )
@@ -122,11 +126,12 @@ def run(mode, task, engine_idx, engine):
                         task,
                         f"engine_{engine_idx}",
                         task.model("smt2"),
-                        ("cd {}; {} -s {}{} --noprogress --append {} --dump-vcd engine_{i}/trace.vcd --dump-vlogtb engine_{i}/trace_tb.v " +
+                        ("cd {}; {} -s {}{} --noprogress --append {} {dump_flags} --aig model/design_aiger.aim:engine_{i}/trace.aiw model/design_smt2.smt2").format
-                             "--dump-smtc engine_{i}/trace.smtc --dump-yw engine_{i}/trace.yw --aig model/design_aiger.aim:engine_{i}/trace.aiw model/design_smt2.smt2").format
                                     (task.workdir, task.exe_paths["smtbmc"], task.opt_aigsmt,
                                     "" if task.opt_tbtop is None else f" --vlogtb-top {task.opt_tbtop}",
-                                    task.opt_append, i=engine_idx),
+                                    task.opt_append,
+                                    dump_flags=dump_flags,
+                                    i=engine_idx),
                         logfile=open(f"{task.workdir}/engine_{engine_idx}/logfile2.txt", "w")
                     )
 

sbysrc/sby_engine_btor.py

@@ -152,17 +152,20 @@ def run(mode, task, engine_idx, engine):
                     suffix = ""
                 else:
                     suffix = common_state.produced_cex
-                proc2 = SbyProc(
+
-                    task,
+                if mode == "cover" or task.opt_vcd:
-                    f"engine_{engine_idx}_{common_state.produced_cex}",
+                    # TODO cover runs btorsim not only for trace generation, can we run it without VCD generation in that case?
-                    task.model("btor"),
+                    proc2 = SbyProc(
-                    "cd {dir} ; btorsim -c --vcd engine_{idx}/trace{i}.vcd --hierarchical-symbols --info model/design_btor{s}.info model/design_btor{s}.btor engine_{idx}/trace{i}.wit".format(dir=task.workdir, idx=engine_idx, i=suffix, s='_single' if solver_args[0] == 'pono' else ''),
+                        task,
-                    logfile=open(f"{task.workdir}/engine_{engine_idx}/logfile2.txt", "w")
+                        f"engine_{engine_idx}_{common_state.produced_cex}",
-                )
+                        task.model("btor"),
-                proc2.output_callback = output_callback2
+                        "cd {dir} ; btorsim -c --vcd engine_{idx}/trace{i}.vcd --hierarchical-symbols --info model/design_btor{s}.info model/design_btor{s}.btor engine_{idx}/trace{i}.wit".format(dir=task.workdir, idx=engine_idx, i=suffix, s='_single' if solver_args[0] == 'pono' else ''),
-                proc2.exit_callback = make_exit_callback(suffix)
+                        logfile=open(f"{task.workdir}/engine_{engine_idx}/logfile2.txt", "w")
-                proc2.checkretcode = True
+                    )
-                common_state.running_procs += 1
+                    proc2.output_callback = output_callback2
+                    proc2.exit_callback = make_exit_callback(suffix)
+                    proc2.checkretcode = True
+                    common_state.running_procs += 1
 
                 common_state.produced_cex += 1
                 common_state.wit_file.close()

sbysrc/sby_engine_smtbmc.py

@@ -148,11 +148,13 @@ def run(mode, task, engine_idx, engine):
         t_opt = "{}".format(task.opt_depth)
 
     random_seed = f"--info \"(set-option :random-seed {random_seed})\"" if random_seed else ""
+    dump_flags = f"--dump-vcd {trace_prefix}.vcd " if task.opt_vcd else ""
+    dump_flags += f"--dump-yw {trace_prefix}.yw --dump-vlogtb {trace_prefix}_tb.v --dump-smtc {trace_prefix}.smtc"
     proc = SbyProc(
         task,
         procname,
         task.model(model_name),
-        f"""cd {task.workdir}; {task.exe_paths["smtbmc"]} {" ".join(smtbmc_opts)} -t {t_opt} {random_seed} --append {task.opt_append} --dump-vcd {trace_prefix}.vcd --dump-yw {trace_prefix}.yw --dump-vlogtb {trace_prefix}_tb.v --dump-smtc {trace_prefix}.smtc model/design_{model_name}.smt2""",
+        f"""cd {task.workdir}; {task.exe_paths["smtbmc"]} {" ".join(smtbmc_opts)} -t {t_opt} {random_seed} --append {task.opt_append} {dump_flags} model/design_{model_name}.smt2""",
         logfile=open(logfile_prefix + ".txt", "w"),
         logstderr=(not progress)
     )

tests/unsorted/no_vcd.sby

@@ -0,0 +1,37 @@
+[tasks]
+smtbmc mode_bmc
+btor_bmc engine_btor mode_bmc
+btor_cover engine_btor mode_cover
+abc mode_bmc
+aiger engine_aiger mode_prove
+
+[options]
+mode_bmc: mode bmc
+mode_prove: mode prove
+mode_cover: mode cover
+vcd off
+~mode_cover: expect fail
+
+[engines]
+smtbmc: smtbmc
+engine_btor: btor btormc
+abc: abc bmc3
+aiger: aiger suprove
+
+[script]
+read_verilog -formal no_vcd.sv
+prep -top top
+
+[file no_vcd.sv]
+module top(input clk, input force);
+
+reg [4:0] counter = 0;
+
+always @(posedge clk) begin
+    if (!counter[4] || force)
+        counter <= counter + 1;
+    assert (counter < 10);
+    cover (counter == 4);
+end
+
+endmodule