diff --git a/docs/source/install.rst b/docs/source/install.rst index ad2075b..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 is 1.3.5 +SBY currently supports the release version 1.5.2 of rIC3 only. diff --git a/docs/source/reference.rst b/docs/source/reference.rst index a50e31e..c06d6c0 100644 --- a/docs/source/reference.rst +++ b/docs/source/reference.rst @@ -293,11 +293,15 @@ The following mode/engine/solver combinations are currently supported: | | | | | ``btor pono`` | | | | +| | ``btor rIC3`` | +| | | | | ``abc bmc3`` | | | | | | ``abc sim3`` | | | | | | ``aiger aigbmc`` | +| | | +| | ``aiger rIC3`` | +-----------+--------------------------+ | ``prove`` | ``smtbmc [all solvers]`` | | | | @@ -305,9 +309,11 @@ The following mode/engine/solver combinations are currently supported: | | | | | ``aiger avy`` | | | | +| | ``aiger suprove`` | +| | | | | ``aiger rIC3`` | | | | -| | ``aiger suprove`` | +| | ``btor rIC3`` | +-----------+--------------------------+ | ``cover`` | ``smtbmc [all solvers]`` | | | | @@ -385,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. @@ -402,7 +410,7 @@ solvers: +-------------------------------+---------------------------------+ | ``avy`` | ``prove`` | +-------------------------------+---------------------------------+ -| ``rIC3`` | ``prove`` | +| ``rIC3`` | ``bmc``, ``prove`` | +-------------------------------+---------------------------------+ | ``aigbmc`` | ``bmc`` | +-------------------------------+---------------------------------+ diff --git a/sbysrc/sby_core.py b/sbysrc/sby_core.py index af9a064..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) @@ -1239,8 +1244,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_aiger.py b/sbysrc/sby_engine_aiger.py index 72add92..c17f6bf 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": @@ -98,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 @@ -130,6 +140,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 @@ -166,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) @@ -179,6 +197,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 b938397..f619bb9 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,10 +34,21 @@ def run(mode, task, engine_idx, engine): for o, a in opts: if o == "--seed": random_seed = a + elif 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 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} " @@ -45,6 +58,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 +67,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 modes.") else: task.error(f"Invalid solver command {solver_args[0]}.") @@ -92,13 +126,29 @@ 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": + # 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.") + 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.") @@ -167,12 +217,13 @@ 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}", [], 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) @@ -183,8 +234,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 @@ -233,6 +284,24 @@ 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]) + 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" + 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 @@ -257,13 +326,15 @@ 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 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, UNKNOWN = 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) 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 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_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 diff --git a/tests/regression/aiger_options.sby b/tests/regression/aiger_options.sby new file mode 100644 index 0000000..4514f60 --- /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 + +mode_bmc: 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