From 5a04ac3fccc91b86e8b66e7fab31ff5c261e1c51 Mon Sep 17 00:00:00 2001 From: "N. Engelhardt" Date: Wed, 12 Jan 2022 10:48:32 +0100 Subject: [PATCH 1/3] use --witness option when calling pono --- sbysrc/sby_engine_btor.py | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/sbysrc/sby_engine_btor.py b/sbysrc/sby_engine_btor.py index 15344d8..bf9216b 100644 --- a/sbysrc/sby_engine_btor.py +++ b/sbysrc/sby_engine_btor.py @@ -46,7 +46,7 @@ def run(mode, task, engine_idx, engine): elif solver_args[0] == "pono": if random_seed: task.error("Setting the random seed is not available for the pono solver.") - solver_cmd = task.exe_paths["pono"] + f" -v 1 -e bmc -k {task.opt_depth - 1}" + solver_cmd = task.exe_paths["pono"] + f" --witness -v 1 -e bmc -k {task.opt_depth - 1}" else: task.error(f"Invalid solver command {solver_args[0]}.") From ad07ea0e8590fb8fba523701c9e72b521fe0cf0c Mon Sep 17 00:00:00 2001 From: "N. Engelhardt" Date: Wed, 12 Jan 2022 11:06:05 +0100 Subject: [PATCH 2/3] add testcase exposing #137 --- tests/multi_assert.sby | 24 ++++++++++++++++++++++++ 1 file changed, 24 insertions(+) create mode 100644 tests/multi_assert.sby diff --git a/tests/multi_assert.sby b/tests/multi_assert.sby new file mode 100644 index 0000000..818195f --- /dev/null +++ b/tests/multi_assert.sby @@ -0,0 +1,24 @@ +[tasks] +btormc +pono + +[options] +mode bmc +depth 5 +expect fail + +[engines] +btormc: btor btormc +pono: btor pono + +[script] +read_verilog -sv multi_assert.v +prep -top test + +[file multi_assert.v] +module test(); +always @* begin +assert (1); +assert (0); +end +endmodule From 257a57d8ed173538ea75e417b4474f69e93c3454 Mon Sep 17 00:00:00 2001 From: "N. Engelhardt" Date: Wed, 12 Jan 2022 13:18:54 +0100 Subject: [PATCH 3/3] create only a single bad when using pono solver; workaround for #137 --- sbysrc/sby_core.py | 1 + sbysrc/sby_engine_btor.py | 4 ++-- 2 files changed, 3 insertions(+), 2 deletions(-) diff --git a/sbysrc/sby_core.py b/sbysrc/sby_core.py index 372cc9b..f05b31d 100644 --- a/sbysrc/sby_core.py +++ b/sbysrc/sby_core.py @@ -449,6 +449,7 @@ class SbyTask: print("dffunmap", file=f) print("stat", file=f) print("write_btor {}-i design_{m}.info design_{m}.btor".format("-c " if self.opt_mode == "cover" else "", m=model_name), file=f) + print("write_btor -s {}-i design_{m}_single.info design_{m}_single.btor".format("-c " if self.opt_mode == "cover" else "", m=model_name), file=f) proc = SbyProc( self, diff --git a/sbysrc/sby_engine_btor.py b/sbysrc/sby_engine_btor.py index bf9216b..7985b32 100644 --- a/sbysrc/sby_engine_btor.py +++ b/sbysrc/sby_engine_btor.py @@ -153,7 +153,7 @@ def run(mode, task, engine_idx, engine): task, f"engine_{engine_idx}_{common_state.produced_cex}", task.model("btor"), - "cd {dir} ; btorsim -c --vcd engine_{idx}/trace{i}.vcd --hierarchical-symbols --info model/design_btor.info model/design_btor.btor engine_{idx}/trace{i}.wit".format(dir=task.workdir, idx=engine_idx, i=suffix), + "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 ''), logfile=open(f"{task.workdir}/engine_{engine_idx}/logfile2.txt", "w") ) proc2.output_callback = output_callback2 @@ -216,7 +216,7 @@ def run(mode, task, engine_idx, engine): proc = SbyProc( task, f"engine_{engine_idx}", task.model("btor"), - f"cd {task.workdir}; {solver_cmd} model/design_btor.btor", + f"cd {task.workdir}; {solver_cmd} model/design_btor{'_single' if solver_args[0]=='pono' else ''}.btor", logfile=open(f"{task.workdir}/engine_{engine_idx}/logfile.txt", "w") )