From 6943469018a3aecbdeda77c23e150ca85ef9e115 Mon Sep 17 00:00:00 2001 From: Yuheng Su Date: Thu, 27 Nov 2025 10:09:53 +0800 Subject: [PATCH 01/18] Fix rIC3 BMC command --- sbysrc/sby_engine_aiger.py | 10 +++++++++- 1 file changed, 9 insertions(+), 1 deletion(-) diff --git a/sbysrc/sby_engine_aiger.py b/sbysrc/sby_engine_aiger.py index 72add92..3b6c7dc 100644 --- a/sbysrc/sby_engine_aiger.py +++ b/sbysrc/sby_engine_aiger.py @@ -53,7 +53,15 @@ def run(mode, task, engine_idx, engine): if mode == "prove": solver_cmd = " ".join([task.exe_paths["rIC3"], "--witness"] + solver_args[1:]) if mode == "bmc": - solver_cmd = " ".join([task.exe_paths["rIC3"], "--bmc-max-k {}".format(task.opt_depth - 1), "-e bmc", "-v 0", "--witness"] + solver_args[1:]) + solver_cmd = " ".join( + [ + task.exe_paths["rIC3"], + "-e bmc", + "--end {}".format(task.opt_depth - 1), + "--witness", + ] + + solver_args[1:] + ) status_2 = "PASS" # rIC3 outputs status 2 when BMC passes elif solver_args[0] == "aigbmc": From 222801e6877fa89e823b3c802b20ceef939829f6 Mon Sep 17 00:00:00 2001 From: Yuheng Su Date: Sun, 7 Dec 2025 14:19:23 +0800 Subject: [PATCH 02/18] Support rIC3 engine for btor --- docs/source/install.rst | 2 +- docs/source/reference.rst | 4 +++ sbysrc/sby_engine_btor.py | 57 ++++++++++++++++++++++++++++++++++++++- sbysrc/sby_mode_prove.py | 4 +++ 4 files changed, 65 insertions(+), 2 deletions(-) diff --git a/docs/source/install.rst b/docs/source/install.rst index ad2075b..1e21e4c 100644 --- a/docs/source/install.rst +++ b/docs/source/install.rst @@ -138,4 +138,4 @@ rIC3 ^^^^ https://github.com/gipsyh/rIC3/ -The minimum required version is 1.3.5 +The minimum required version of rIC3 is 1.5.2 diff --git a/docs/source/reference.rst b/docs/source/reference.rst index a50e31e..80b8f38 100644 --- a/docs/source/reference.rst +++ b/docs/source/reference.rst @@ -298,6 +298,8 @@ The following mode/engine/solver combinations are currently supported: | | ``abc sim3`` | | | | | | ``aiger aigbmc`` | +| | | +| | ``aiger rIC3`` | +-----------+--------------------------+ | ``prove`` | ``smtbmc [all solvers]`` | | | | @@ -308,6 +310,8 @@ The following mode/engine/solver combinations are currently supported: | | ``aiger rIC3`` | | | | | | ``aiger suprove`` | +| | | +| | ``btor rIC3`` | +-----------+--------------------------+ | ``cover`` | ``smtbmc [all solvers]`` | | | | diff --git a/sbysrc/sby_engine_btor.py b/sbysrc/sby_engine_btor.py index b938397..31cd6c9 100644 --- a/sbysrc/sby_engine_btor.py +++ b/sbysrc/sby_engine_btor.py @@ -36,6 +36,8 @@ def run(mode, task, engine_idx, engine): task.error("Unexpected BTOR engine options.") if solver_args[0] == "btormc": + if mode != "bmc": + task.error("The btormc solver is only supported in bmc mode.") solver_cmd = "" if random_seed: solver_cmd += f"BTORSEED={random_seed} " @@ -45,6 +47,8 @@ def run(mode, task, engine_idx, engine): solver_cmd += " ".join([""] + solver_args[1:]) elif solver_args[0] == "pono": + if mode != "bmc": + task.error("The pono solver is only supported in bmc mode.") if random_seed: task.error("Setting the random seed is not available for the pono solver.") if task.opt_skip is not None: @@ -52,6 +56,25 @@ def run(mode, task, engine_idx, engine): solver_cmd = task.exe_paths["pono"] + f" --witness -v 1 -e bmc -k {task.opt_depth - 1}" solver_cmd += " ".join([""] + solver_args[1:]) + elif solver_args[0] == "rIC3": + if random_seed: + task.error("Setting the random seed is not available for the rIC3 solver.") + if task.opt_skip is not None: + task.error("The btor engine supports the option skip only for the btormc solver.") + if mode == "prove": + solver_cmd = " ".join([task.exe_paths["rIC3"], "--witness"] + solver_args[1:]) + elif mode == "bmc": + solver_cmd = " ".join( + [ + task.exe_paths["rIC3"], + "-e bmc", + "--end {}".format(task.opt_depth - 1), + "--witness", + ] + + solver_args[1:] + ) + else: + task.error("The rIC3 solver is only supported in bmc and prove mode.") else: task.error(f"Invalid solver command {solver_args[0]}.") @@ -92,13 +115,26 @@ def run(mode, task, engine_idx, engine): else: task.error(f"engine_{engine_idx}: Engine terminated without status.") task.update_unknown_props(dict(source="btor", engine=f"engine_{engine_idx}")) - else: + elif mode == "bmc": if common_state.expected_cex == 0: proc_status = "pass" elif common_state.solver_status == "sat": proc_status = "FAIL" elif common_state.solver_status == "unsat": proc_status = "pass" + elif common_state.solver_status == "unknown": + proc_status = "pass" + else: + task.error(f"engine_{engine_idx}: Engine terminated without status.") + elif mode == "prove": + if common_state.expected_cex == 0: + proc_status = "pass" + elif common_state.solver_status == "sat": + proc_status = "FAIL" + elif common_state.solver_status == "unsat": + proc_status = "pass" + elif common_state.solver_status == "unknown": + proc_status = "UNKNOWN" else: task.error(f"engine_{engine_idx}: Engine terminated without status.") @@ -233,6 +269,23 @@ def run(mode, task, engine_idx, engine): if line not in ["b0"]: return line + elif solver_args[0] == "rIC3": + match = re.match(r".*bmc found counter-example in depth (\d+).*", line) + if match: + common_state.current_step = int(match[1]) + if line == "UNSAT": + if common_state.solver_status is None: + common_state.solver_status = "unsat" + return "No CEX found." + if line == "UNKNOWN": + if common_state.solver_status is None: + common_state.solver_status = "unknown" + if line == "SAT": + if common_state.solver_status is None: + common_state.solver_status = "sat" + return line + + print(line, file=proc.logfile) return None @@ -264,6 +317,8 @@ def run(mode, task, engine_idx, engine): proc.checkretcode = True if solver_args[0] == "pono": proc.retcodes = [0, 1, 255] # UNKNOWN = -1, FALSE = 0, TRUE = 1, ERROR = 2 + if solver_args[0] == "rIC3": + proc.retcodes = [10, 20, 30] # FALSE = 10, TRUE = 20, ERROR = 30 proc.output_callback = output_callback proc.register_exit_callback(exit_callback) common_state.running_procs += 1 diff --git a/sbysrc/sby_mode_prove.py b/sbysrc/sby_mode_prove.py index c608c6b..ac0efdb 100644 --- a/sbysrc/sby_mode_prove.py +++ b/sbysrc/sby_mode_prove.py @@ -42,6 +42,10 @@ def run(task): import sby_engine_aiger sby_engine_aiger.run("prove", task, engine_idx, engine) + elif engine[0] == "btor": + import sby_engine_btor + sby_engine_btor.run("prove", task, engine_idx, engine) + elif engine[0] == "abc": import sby_engine_abc sby_engine_abc.run("prove", task, engine_idx, engine) From a6069081c72aa16cc8a7bc6628921894ed4624da Mon Sep 17 00:00:00 2001 From: Yuheng Su Date: Tue, 2 Dec 2025 17:01:29 +0800 Subject: [PATCH 03/18] Enhance BTOR engine options with nomem and syn flags for improved model handling --- sbysrc/sby_core.py | 4 ++-- sbysrc/sby_engine_btor.py | 23 +++++++++++++++++------ 2 files changed, 19 insertions(+), 8 deletions(-) diff --git a/sbysrc/sby_core.py b/sbysrc/sby_core.py index af9a064..aeb9b21 100644 --- a/sbysrc/sby_core.py +++ b/sbysrc/sby_core.py @@ -1239,8 +1239,8 @@ class SbyTask(SbyConfig): print("delete -output", file=f) print("dffunmap", file=f) print("stat", file=f) - print("write_btor {}-i design_{m}.info -ywmap design_btor.ywb 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 -ywmap design_btor_single.ywb design_{m}_single.btor".format("-c " if self.opt_mode == "cover" else "", m=model_name), file=f) + print("write_btor {}-i design_{m}.info -ywmap design_{m}.ywb 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 -ywmap design_{m}_single.ywb 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 31cd6c9..47b1ec6 100644 --- a/sbysrc/sby_engine_btor.py +++ b/sbysrc/sby_engine_btor.py @@ -23,8 +23,10 @@ from sby_sim import sim_witness_trace def run(mode, task, engine_idx, engine): random_seed = None + nomem_opt = False + syn_opt = False - opts, solver_args = getopt.getopt(engine[1:], "", ["seed="]) + opts, solver_args = getopt.getopt(engine[1:], "", ["nomem", "syn", "seed="]) if len(solver_args) == 0: task.error("Missing solver command.") @@ -32,9 +34,18 @@ def run(mode, task, engine_idx, engine): for o, a in opts: if o == "--seed": random_seed = a + if o == "--nomem": + nomem_opt = True + elif o == "--syn": + syn_opt = True else: task.error("Unexpected BTOR engine options.") + model_name = "btor" + + if syn_opt: model_name += "_syn" + if nomem_opt: model_name += "_nomem" + if solver_args[0] == "btormc": if mode != "bmc": task.error("The btormc solver is only supported in bmc mode.") @@ -203,7 +214,7 @@ def run(mode, task, engine_idx, engine): else: suffix = common_state.produced_cex - model = f"design_btor{'_single' if solver_args[0] == 'pono' else ''}" + model = f"design_{model_name}{'_single' if solver_args[0] == 'pono' else ''}" yw_proc = SbyProc( task, f"engine_{engine_idx}.trace{suffix}", [], @@ -219,8 +230,8 @@ def run(mode, task, engine_idx, engine): proc2 = SbyProc( task, f"engine_{engine_idx}.trace{suffix}", - task.model("btor"), - "cd {dir} ; btorsim -c --vcd engine_{idx}/trace{i}{i2}.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, i2='' if btorsim_vcd else '_btorsim', s='_single' if solver_args[0] == 'pono' else ''), + task.model(model_name), + "cd {dir} ; btorsim -c --vcd engine_{idx}/trace{i}{i2}.vcd --hierarchical-symbols --info model/design_{m}{s}.info model/design_{m}{s}.btor engine_{idx}/trace{i}.wit".format(dir=task.workdir, idx=engine_idx, i=suffix, i2='' if btorsim_vcd else '_btorsim', m=model_name, s='_single' if solver_args[0] == 'pono' else ''), logfile=open(f"{task.workdir}/engine_{engine_idx}/logfile2.txt", "w") ) proc2.output_callback = output_callback2 @@ -310,8 +321,8 @@ 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{'_single' if solver_args[0]=='pono' else ''}.btor", + f"engine_{engine_idx}", task.model(model_name), + f"cd {task.workdir}; {solver_cmd} model/design_{model_name}{'_single' if solver_args[0] == 'pono' else ''}.btor", logfile=open(f"{task.workdir}/engine_{engine_idx}/logfile.txt", "w") ) proc.checkretcode = True From e57071a3769b878b7839b8913e6229b5b557e421 Mon Sep 17 00:00:00 2001 From: Yuheng Su Date: Sun, 7 Dec 2025 14:41:56 +0800 Subject: [PATCH 04/18] Add support for BTOR rIC3 engine in documentation --- docs/source/reference.rst | 10 +++++++--- 1 file changed, 7 insertions(+), 3 deletions(-) diff --git a/docs/source/reference.rst b/docs/source/reference.rst index 80b8f38..087bde2 100644 --- a/docs/source/reference.rst +++ b/docs/source/reference.rst @@ -300,6 +300,8 @@ The following mode/engine/solver combinations are currently supported: | | ``aiger aigbmc`` | | | | | | ``aiger rIC3`` | +| | | +| | ``btor rIC3`` | +-----------+--------------------------+ | ``prove`` | ``smtbmc [all solvers]`` | | | | @@ -307,10 +309,10 @@ The following mode/engine/solver combinations are currently supported: | | | | | ``aiger avy`` | | | | -| | ``aiger rIC3`` | -| | | | | ``aiger suprove`` | | | | +| | ``aiger rIC3`` | +| | | | | ``btor rIC3`` | +-----------+--------------------------+ | ``cover`` | ``smtbmc [all solvers]`` | @@ -389,6 +391,8 @@ The engine supports no engine options and supports the following solvers: +-------------------------------+---------------------------------+ | ``pono`` | ``bmc`` | +-------------------------------+---------------------------------+ +| ``rIC3`` | ``bmc``,``prove`` | ++-------------------------------+---------------------------------+ Solver options are passed to the solver as additional command line options. @@ -406,7 +410,7 @@ solvers: +-------------------------------+---------------------------------+ | ``avy`` | ``prove`` | +-------------------------------+---------------------------------+ -| ``rIC3`` | ``prove`` | +| ``rIC3`` | ``prove``,``bmc`` | +-------------------------------+---------------------------------+ | ``aigbmc`` | ``bmc`` | +-------------------------------+---------------------------------+ From a8f3f4bba21dbc12787c168c3e259c21cbe9f5ba Mon Sep 17 00:00:00 2001 From: Yuheng Su Date: Tue, 9 Dec 2025 09:34:19 +0800 Subject: [PATCH 05/18] Update sbysrc/sby_engine_btor.py Co-authored-by: Copilot <175728472+Copilot@users.noreply.github.com> --- 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 47b1ec6..446f315 100644 --- a/sbysrc/sby_engine_btor.py +++ b/sbysrc/sby_engine_btor.py @@ -85,7 +85,7 @@ def run(mode, task, engine_idx, engine): + solver_args[1:] ) else: - task.error("The rIC3 solver is only supported in bmc and prove mode.") + task.error("The rIC3 solver is only supported in bmc and prove modes.") else: task.error(f"Invalid solver command {solver_args[0]}.") From 87936dd03bf5c8d7385237e18a3ead515dc4857a Mon Sep 17 00:00:00 2001 From: Yuheng Su Date: Tue, 9 Dec 2025 09:41:17 +0800 Subject: [PATCH 06/18] Update rIC3 return codes to include UNKNOWN status --- 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 446f315..bc4c1b5 100644 --- a/sbysrc/sby_engine_btor.py +++ b/sbysrc/sby_engine_btor.py @@ -329,7 +329,7 @@ def run(mode, task, engine_idx, engine): if solver_args[0] == "pono": proc.retcodes = [0, 1, 255] # UNKNOWN = -1, FALSE = 0, TRUE = 1, ERROR = 2 if solver_args[0] == "rIC3": - proc.retcodes = [10, 20, 30] # FALSE = 10, TRUE = 20, ERROR = 30 + proc.retcodes = [10, 20, 30] # FALSE = 10, TRUE = 20, UNKNOWN = 30 proc.output_callback = output_callback proc.register_exit_callback(exit_callback) common_state.running_procs += 1 From 5b48417823c2bb9c977acc7c249a33df2413ec79 Mon Sep 17 00:00:00 2001 From: Yuheng Su Date: Tue, 9 Dec 2025 09:41:47 +0800 Subject: [PATCH 07/18] Update docs/source/reference.rst Co-authored-by: Copilot <175728472+Copilot@users.noreply.github.com> --- docs/source/reference.rst | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/docs/source/reference.rst b/docs/source/reference.rst index 087bde2..66998df 100644 --- a/docs/source/reference.rst +++ b/docs/source/reference.rst @@ -391,7 +391,7 @@ The engine supports no engine options and supports the following solvers: +-------------------------------+---------------------------------+ | ``pono`` | ``bmc`` | +-------------------------------+---------------------------------+ -| ``rIC3`` | ``bmc``,``prove`` | +| ``rIC3`` | ``bmc``, ``prove`` | +-------------------------------+---------------------------------+ Solver options are passed to the solver as additional command line options. From d17e524a1b7b03990a83f844a91958199f68e656 Mon Sep 17 00:00:00 2001 From: Yuheng Su Date: Tue, 9 Dec 2025 09:42:23 +0800 Subject: [PATCH 08/18] Update docs/source/reference.rst Co-authored-by: Copilot <175728472+Copilot@users.noreply.github.com> --- docs/source/reference.rst | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/docs/source/reference.rst b/docs/source/reference.rst index 66998df..80b71d9 100644 --- a/docs/source/reference.rst +++ b/docs/source/reference.rst @@ -410,7 +410,7 @@ solvers: +-------------------------------+---------------------------------+ | ``avy`` | ``prove`` | +-------------------------------+---------------------------------+ -| ``rIC3`` | ``prove``,``bmc`` | +| ``rIC3`` | ``prove``, ``bmc`` | +-------------------------------+---------------------------------+ | ``aigbmc`` | ``bmc`` | +-------------------------------+---------------------------------+ From 055a3b5d8b9eb40421e545de6ea56aae083c59b5 Mon Sep 17 00:00:00 2001 From: Yuheng Su Date: Tue, 9 Dec 2025 09:42:41 +0800 Subject: [PATCH 09/18] Update sbysrc/sby_engine_btor.py Co-authored-by: Copilot <175728472+Copilot@users.noreply.github.com> --- sbysrc/sby_engine_btor.py | 2 -- 1 file changed, 2 deletions(-) diff --git a/sbysrc/sby_engine_btor.py b/sbysrc/sby_engine_btor.py index bc4c1b5..a8a2aca 100644 --- a/sbysrc/sby_engine_btor.py +++ b/sbysrc/sby_engine_btor.py @@ -295,8 +295,6 @@ def run(mode, task, engine_idx, engine): if common_state.solver_status is None: common_state.solver_status = "sat" return line - - print(line, file=proc.logfile) return None From e8bf66d4f0dc92755d6a1ee0dc0f9a134e5dd60a Mon Sep 17 00:00:00 2001 From: "N. Engelhardt" Date: Thu, 18 Jun 2026 11:15:00 +0200 Subject: [PATCH 10/18] small fixes + add regression tests for aiger and btor engines exercising all options --- sbysrc/sby_engine_btor.py | 9 ++-- tests/make/required_tools.py | 2 + tests/regression/aiger_options.sby | 46 ++++++++++++++++++ tests/regression/btor_options.sby | 75 ++++++++++++++++++++++++++++++ 4 files changed, 129 insertions(+), 3 deletions(-) create mode 100644 tests/regression/aiger_options.sby create mode 100644 tests/regression/btor_options.sby diff --git a/sbysrc/sby_engine_btor.py b/sbysrc/sby_engine_btor.py index a8a2aca..3d6d177 100644 --- a/sbysrc/sby_engine_btor.py +++ b/sbysrc/sby_engine_btor.py @@ -34,7 +34,7 @@ def run(mode, task, engine_idx, engine): for o, a in opts: if o == "--seed": random_seed = a - if o == "--nomem": + elif o == "--nomem": nomem_opt = True elif o == "--syn": syn_opt = True @@ -47,8 +47,8 @@ def run(mode, task, engine_idx, engine): if nomem_opt: model_name += "_nomem" if solver_args[0] == "btormc": - if mode != "bmc": - task.error("The btormc solver is only supported in bmc mode.") + if mode not in ["bmc", "cover"]: + task.error("The btormc solver is only supported in bmc and cover modes.") solver_cmd = "" if random_seed: solver_cmd += f"BTORSEED={random_seed} " @@ -134,6 +134,9 @@ def run(mode, task, engine_idx, engine): elif common_state.solver_status == "unsat": proc_status = "pass" elif common_state.solver_status == "unknown": + # Currently only rIC3 solver can return unknown. + # rIC3 in bmc mode returns "sat" for counterexample found + # and "unknown" for no counterexample found until bound k. proc_status = "pass" else: task.error(f"engine_{engine_idx}: Engine terminated without status.") diff --git a/tests/make/required_tools.py b/tests/make/required_tools.py index 82b5f49..78f3c93 100644 --- a/tests/make/required_tools.py +++ b/tests/make/required_tools.py @@ -11,9 +11,11 @@ REQUIRED_TOOLS = { ("smtbmc", "abc"): ["yosys-abc"], ("aiger", "suprove"): ["suprove", "yices"], ("aiger", "avy"): ["avy", "yices"], + ("aiger", "rIC3"): ["rIC3", "yices"], ("aiger", "aigbmc"): ["aigbmc", "yices"], ("btor", "btormc"): ["btormc", "btorsim"], ("btor", "pono"): ["pono", "btorsim"], + ("btor", "rIC3"): ["rIC3", "btorsim"], ("abc"): ["yices"], } diff --git a/tests/regression/aiger_options.sby b/tests/regression/aiger_options.sby new file mode 100644 index 0000000..4bb659e --- /dev/null +++ b/tests/regression/aiger_options.sby @@ -0,0 +1,46 @@ +[tasks] +--pycode-begin-- +supported = { + "aigbmc": ["bmc"], + "ric3": ["bmc", "prove"], + "avy": ["prove"], + "suprove": ["prove", "live"], +} + +for solver, modes in supported.items(): + for mode in modes: + output(f"{solver}_{mode} mode_{mode} solver_{solver}") +--pycode-end-- + +[options] +mode_bmc: mode bmc +mode_prove: mode prove +mode_live: mode live + +depth 4 +mode_live: expect fail + +[engines] +solver_aigbmc: aiger aigbmc +solver_ric3: aiger rIC3 +solver_avy: aiger avy +solver_suprove: aiger suprove + +[script] +read -formal top.sv +prep -top top + +[file top.sv] +module top(input clk, input up, down); + reg [4:0] counter = 0; + + always @(posedge clk) begin + if (up && counter != 10) + counter <= counter + 1; + if (down && counter != 0) + counter <= counter - 1; + + assert property (counter != 15); + assert property (s_eventually counter == 15); + end +endmodule diff --git a/tests/regression/btor_options.sby b/tests/regression/btor_options.sby new file mode 100644 index 0000000..0e3a635 --- /dev/null +++ b/tests/regression/btor_options.sby @@ -0,0 +1,75 @@ +[tasks] +--pycode-begin-- +supported = { + "btormc": { + "modes": ["bmc", "cover"], + "opts": ["base", "seed", "nomem", "syn", "syn_nomem"], + }, + "pono": { + "modes": ["bmc"], + "opts": ["base", "nomem", "syn", "syn_nomem"], + }, + "ric3": { + "modes": ["bmc", "prove"], + "opts": ["base", "nomem", "syn", "syn_nomem"], + }, +} + +for solver, support in supported.items(): + for mode in support["modes"]: + for opt in support["opts"]: + output( + f"{solver}_{mode}_{opt} " + f"mode_{mode} solver_{solver} opt_{opt}" + ) +--pycode-end-- + +[options] +mode_bmc: mode bmc +mode_cover: mode cover +mode_prove: mode prove + +depth 4 + +expect pass + +[engines] +--pycode-begin-- +if "opt_seed" in tags: + opts = "--seed=42 " +elif "opt_nomem" in tags: + opts = "--nomem " +elif "opt_syn" in tags: + opts = "--syn " +elif "opt_syn_nomem" in tags: + opts = "--syn --nomem " +else: + opts = "" + +if "solver_btormc" in tags: + output(f"btor {opts}btormc") +elif "solver_pono" in tags: + output(f"btor {opts}pono") +elif "solver_ric3" in tags: + output(f"btor {opts}rIC3") +--pycode-end-- + +[script] +read -formal top.sv +prep -top top + +[file top.sv] +module top(input clk); + reg [1:0] counter = 0; + reg [1:0] memory [0:3]; + reg [1:0] value; + + always @(posedge clk) begin + counter <= counter + 1; + memory[counter] <= counter; + value <= memory[counter]; + + assert property (counter < 4); + cover property (counter == 2 && value == 1); + end +endmodule From ff48d2b9fd5cab298f1fdd4e14a36523cd39b280 Mon Sep 17 00:00:00 2001 From: Miodrag Milanovic Date: Tue, 23 Jun 2026 10:11:10 +0200 Subject: [PATCH 11/18] Fix aiger_options test --- tests/regression/aiger_options.sby | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/tests/regression/aiger_options.sby b/tests/regression/aiger_options.sby index 4bb659e..4514f60 100644 --- a/tests/regression/aiger_options.sby +++ b/tests/regression/aiger_options.sby @@ -17,7 +17,7 @@ mode_bmc: mode bmc mode_prove: mode prove mode_live: mode live -depth 4 +mode_bmc: depth 4 mode_live: expect fail [engines] From c4ed754ff8a87f5d4fe5e1c1300f27ddf5147c1f Mon Sep 17 00:00:00 2001 From: Miodrag Milanovic Date: Tue, 23 Jun 2026 10:51:21 +0200 Subject: [PATCH 12/18] Fix documentation --- docs/source/reference.rst | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/docs/source/reference.rst b/docs/source/reference.rst index 80b71d9..f2e6bd2 100644 --- a/docs/source/reference.rst +++ b/docs/source/reference.rst @@ -410,7 +410,7 @@ solvers: +-------------------------------+---------------------------------+ | ``avy`` | ``prove`` | +-------------------------------+---------------------------------+ -| ``rIC3`` | ``prove``, ``bmc`` | +| ``rIC3`` | ``prove``, ``bmc`` | +-------------------------------+---------------------------------+ | ``aigbmc`` | ``bmc`` | +-------------------------------+---------------------------------+ From 29650804c196a8c0bb6059decb02d08adef3d140 Mon Sep 17 00:00:00 2001 From: Miodrag Milanovic Date: Tue, 23 Jun 2026 12:21:28 +0200 Subject: [PATCH 13/18] catch subprocess crash as error --- sbysrc/sby_engine_aiger.py | 5 +++++ sbysrc/sby_engine_btor.py | 3 +++ 2 files changed, 8 insertions(+) diff --git a/sbysrc/sby_engine_aiger.py b/sbysrc/sby_engine_aiger.py index 3b6c7dc..b08195a 100644 --- a/sbysrc/sby_engine_aiger.py +++ b/sbysrc/sby_engine_aiger.py @@ -138,6 +138,11 @@ def run(mode, task, engine_idx, engine): proc_status = "FAIL" return None + if solver_args[0] == "rIC3": + match = re.match(r".*all workers unexpectedly exited.*", line) + if match: + proc_status = "ERROR" + if proc_status is not None: if not end_of_cex and not produced_cex and line.isdigit(): produced_cex = True diff --git a/sbysrc/sby_engine_btor.py b/sbysrc/sby_engine_btor.py index 3d6d177..b155763 100644 --- a/sbysrc/sby_engine_btor.py +++ b/sbysrc/sby_engine_btor.py @@ -287,6 +287,9 @@ def run(mode, task, engine_idx, engine): match = re.match(r".*bmc found counter-example in depth (\d+).*", line) if match: common_state.current_step = int(match[1]) + match = re.match(r".*all workers unexpectedly exited.*", line) + if match: + common_state.solver_status = "error" if line == "UNSAT": if common_state.solver_status is None: common_state.solver_status = "unsat" From ca8d332ccbfbdd3d353aa3cf8697db99d55d64ab Mon Sep 17 00:00:00 2001 From: "N. Engelhardt" Date: Mon, 6 Jul 2026 18:09:43 +0200 Subject: [PATCH 14/18] make engine/solver reference more consistent --- docs/source/reference.rst | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/docs/source/reference.rst b/docs/source/reference.rst index f2e6bd2..c06d6c0 100644 --- a/docs/source/reference.rst +++ b/docs/source/reference.rst @@ -293,6 +293,8 @@ The following mode/engine/solver combinations are currently supported: | | | | | ``btor pono`` | | | | +| | ``btor rIC3`` | +| | | | | ``abc bmc3`` | | | | | | ``abc sim3`` | @@ -300,8 +302,6 @@ The following mode/engine/solver combinations are currently supported: | | ``aiger aigbmc`` | | | | | | ``aiger rIC3`` | -| | | -| | ``btor rIC3`` | +-----------+--------------------------+ | ``prove`` | ``smtbmc [all solvers]`` | | | | @@ -410,7 +410,7 @@ solvers: +-------------------------------+---------------------------------+ | ``avy`` | ``prove`` | +-------------------------------+---------------------------------+ -| ``rIC3`` | ``prove``, ``bmc`` | +| ``rIC3`` | ``bmc``, ``prove`` | +-------------------------------+---------------------------------+ | ``aigbmc`` | ``bmc`` | +-------------------------------+---------------------------------+ From 97e47c471c9461e4e8e188215aefb32227957e75 Mon Sep 17 00:00:00 2001 From: "N. Engelhardt" Date: Mon, 6 Jul 2026 18:54:23 +0200 Subject: [PATCH 15/18] fix incidental finding that return codes weren't being checked properly on witness conversion subprocesses --- sbysrc/sby_engine_aiger.py | 1 + sbysrc/sby_engine_btor.py | 1 + sbysrc/sby_sim.py | 1 + 3 files changed, 3 insertions(+) diff --git a/sbysrc/sby_engine_aiger.py b/sbysrc/sby_engine_aiger.py index b08195a..703da8e 100644 --- a/sbysrc/sby_engine_aiger.py +++ b/sbysrc/sby_engine_aiger.py @@ -192,6 +192,7 @@ def aigsmt_trace_callback(task, engine_idx, proc_status, *, run_aigsmt, smtbmc_v task, f"engine_{engine_idx}", [], f"cd {task.workdir}; {task.exe_paths['witness']} aiw2yw engine_{engine_idx}/{name}.aiw model/design_aiger.ywa engine_{engine_idx}/{name}{aiw2yw_suffix}.yw", ) + witness_proc.checkretcode = True final_proc = witness_proc if run_aigsmt: diff --git a/sbysrc/sby_engine_btor.py b/sbysrc/sby_engine_btor.py index b155763..f619bb9 100644 --- a/sbysrc/sby_engine_btor.py +++ b/sbysrc/sby_engine_btor.py @@ -223,6 +223,7 @@ def run(mode, task, engine_idx, engine): task, f"engine_{engine_idx}.trace{suffix}", [], f"cd {task.workdir}; {task.exe_paths['witness']} wit2yw engine_{engine_idx}/trace{suffix}.wit model/{model}.ywb engine_{engine_idx}/trace{suffix}.yw", ) + yw_proc.checkretcode = True common_state.running_procs += 1 yw_proc.register_exit_callback(simple_exit_callback) diff --git a/sbysrc/sby_sim.py b/sbysrc/sby_sim.py index 32789fb..2e9b471 100644 --- a/sbysrc/sby_sim.py +++ b/sbysrc/sby_sim.py @@ -99,6 +99,7 @@ def sim_witness_trace(prefix, task, engine_idx, witness_file, *, append, inducti deps, f"""cd {task.workdir}/engine_{engine_idx}; {task.exe_paths["yosys"]} -ql {trace_name}.log {trace_name}.ys""", ) + proc.checkretcode = True proc.noprintregex = re.compile(r"Warning: Assert .* failed.*") proc.register_exit_callback(exit_callback) return proc From d11cc34cb3c619962229bb6a31cbe1160e1f41e0 Mon Sep 17 00:00:00 2001 From: "N. Engelhardt" Date: Mon, 6 Jul 2026 19:58:52 +0200 Subject: [PATCH 16/18] fix aiger witness handling for combinational designs (empty newlines are semantically important for aiw output parsed from log) --- sbysrc/sby_core.py | 9 +++++++-- sbysrc/sby_engine_aiger.py | 2 ++ tests/regression/aiger_comb_witness.sby | 21 +++++++++++++++++++++ 3 files changed, 30 insertions(+), 2 deletions(-) create mode 100644 tests/regression/aiger_comb_witness.sby diff --git a/sbysrc/sby_core.py b/sbysrc/sby_core.py index aeb9b21..d97599c 100644 --- a/sbysrc/sby_core.py +++ b/sbysrc/sby_core.py @@ -91,6 +91,7 @@ class SbyProc: self.noprintregex = None self.notify = [] self.linebuffer = "" + self.preserve_whitespace = False self.logstderr = logstderr self.silent = silent self.wait = False @@ -125,7 +126,7 @@ class SbyProc: self.task.log(f"{click.style(self.info, fg='magenta')}: {line}") def handle_output(self, line): - if self.terminated or len(line) == 0: + if self.terminated or (len(line) == 0 and not self.preserve_whitespace): return if self.output_callback is not None: line = self.output_callback(line) @@ -296,7 +297,11 @@ class SbyProc: if outs[-1] != '\n': self.linebuffer += outs break - outs = (self.linebuffer + outs).strip() + outs = self.linebuffer + outs + if self.preserve_whitespace: + outs = outs.rstrip("\r\n") + else: + outs = outs.strip() self.linebuffer = "" self.handle_output(outs) diff --git a/sbysrc/sby_engine_aiger.py b/sbysrc/sby_engine_aiger.py index 703da8e..ce9d169 100644 --- a/sbysrc/sby_engine_aiger.py +++ b/sbysrc/sby_engine_aiger.py @@ -106,6 +106,8 @@ def run(mode, task, engine_idx, engine): ) if solver_args[0] not in ["avy", "rIC3"]: proc.checkretcode = True + if not json_output: + proc.preserve_whitespace = True proc_status = None produced_cex = False diff --git a/tests/regression/aiger_comb_witness.sby b/tests/regression/aiger_comb_witness.sby new file mode 100644 index 0000000..3458673 --- /dev/null +++ b/tests/regression/aiger_comb_witness.sby @@ -0,0 +1,21 @@ +[tasks] +aigbmc +ric3 + +[options] +mode bmc +depth 1 +expect fail + +[engines] +aigbmc: aiger aigbmc +ric3: aiger rIC3 + +[script] +read -formal top.sv +prep -top top + +[file top.sv] +module top(input a); + always @* assert (!a); +endmodule From b2b067757ef1187d640022a9b5ab54f98f0e2467 Mon Sep 17 00:00:00 2001 From: "N. Engelhardt" Date: Tue, 7 Jul 2026 12:50:02 +0200 Subject: [PATCH 17/18] don't call yosys-witness on (unsupported) justice witnesses --- sbysrc/sby_engine_aiger.py | 3 +++ 1 file changed, 3 insertions(+) diff --git a/sbysrc/sby_engine_aiger.py b/sbysrc/sby_engine_aiger.py index ce9d169..c17f6bf 100644 --- a/sbysrc/sby_engine_aiger.py +++ b/sbysrc/sby_engine_aiger.py @@ -181,6 +181,9 @@ def aigsmt_exit_callback(task, engine_idx, proc_status, *, run_aigsmt, smtbmc_vc task.update_status(proc_status) task.summary.set_engine_status(engine_idx, proc_status) task.terminate() + if task.opt_mode == "live": + # we don't have any tools to process or visualize justice (lasso) witnesses + return if proc_status == "FAIL" and (not run_aigsmt or task.opt_aigsmt != "none"): aigsmt_trace_callback(task, engine_idx, proc_status, run_aigsmt=run_aigsmt, smtbmc_vcd=smtbmc_vcd, smtbmc_append=smtbmc_append, sim_append=sim_append) From 39d17d1a2b97c5a6d793704efba23d0348c8fdd9 Mon Sep 17 00:00:00 2001 From: "N. Engelhardt" Date: Tue, 7 Jul 2026 17:33:17 +0200 Subject: [PATCH 18/18] be more precise on supported rIC3 version --- docs/source/install.rst | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/docs/source/install.rst b/docs/source/install.rst index 1e21e4c..31049e2 100644 --- a/docs/source/install.rst +++ b/docs/source/install.rst @@ -138,4 +138,4 @@ rIC3 ^^^^ https://github.com/gipsyh/rIC3/ -The minimum required version of rIC3 is 1.5.2 +SBY currently supports the release version 1.5.2 of rIC3 only.