diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index ebb11f5..c83fa1d 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -11,10 +11,10 @@ jobs: steps: - name: Checkout SBY - uses: actions/checkout@v4 + uses: actions/checkout@v7 - name: Install oss-cad-suite - uses: YosysHQ/setup-oss-cad-suite@v3 + uses: YosysHQ/setup-oss-cad-suite@v4 with: github-token: ${{ secrets.GITHUB_TOKEN }} - name: Run SBY tests @@ -24,10 +24,10 @@ jobs: runs-on: [self-hosted, linux, x64, fast] steps: - name: Checkout SBY - uses: actions/checkout@v4 + uses: actions/checkout@v7 - name: Checkout Yosys - uses: actions/checkout@v4 + uses: actions/checkout@v7 with: repository: 'YosysHQ/yosys' path: 'yosys' @@ -40,14 +40,16 @@ jobs: - name: Build Yosys run: | cd yosys - make config-clang - echo "ENABLE_VERIFIC := 1" >> Makefile.conf - echo "ENABLE_VERIFIC_EDIF := 1" >> Makefile.conf - echo "ENABLE_VERIFIC_LIBERTY := 1" >> Makefile.conf - echo "ENABLE_VERIFIC_YOSYSHQ_EXTENSIONS := 1" >> Makefile.conf - echo "ENABLE_CCACHE := 1" >> Makefile.conf - make -j${{ env.procs }} - make install DESTDIR=${GITHUB_WORKSPACE}/.local PREFIX= + rm -rf build Configuration.cmake + echo 'set(CMAKE_C_COMPILER clang CACHE STRING "")' >> Configuration.cmake + echo 'set(CMAKE_CXX_COMPILER clang++ CACHE STRING "")' >> Configuration.cmake + echo 'set(YOSYS_COMPILER_LAUNCHER ccache CACHE STRING "")' >> Configuration.cmake + echo 'set(YOSYS_VERIFIC_DIR "/usr/local/src/verific_lib" CACHE STRING "")' >> Configuration.cmake + + cmake -C Configuration.cmake -B build . -DCMAKE_INSTALL_PREFIX=${GITHUB_WORKSPACE}/.local -DCMAKE_BUILD_TYPE=Debug + + cmake --build build -j${{ env.procs }} + cmake --build build --target install - name: Build SBY run: | diff --git a/.github/workflows/codeql.yml b/.github/workflows/codeql.yml index 888cbb3..10125a8 100644 --- a/.github/workflows/codeql.yml +++ b/.github/workflows/codeql.yml @@ -16,13 +16,13 @@ jobs: steps: - name: Checkout repository - uses: actions/checkout@v4 + uses: actions/checkout@v7 - name: Initialize CodeQL - uses: github/codeql-action/init@v3 + uses: github/codeql-action/init@v4 with: languages: python queries: security-extended,security-and-quality - name: Perform CodeQL Analysis - uses: github/codeql-action/analyze@v3 + uses: github/codeql-action/analyze@v4 diff --git a/docs/source/appnotes.rst b/docs/source/appnotes.rst new file mode 100644 index 0000000..ae675e5 --- /dev/null +++ b/docs/source/appnotes.rst @@ -0,0 +1,9 @@ +Application Notes +================= + +Formal Basics and Methods +-------------------------- + +- `109 Property Checking with SVA `_ +- `120 Weak precondition cover and witness for SVA properties `_ +- `130 Multi-Stage Verification `_ diff --git a/docs/source/index.rst b/docs/source/index.rst index ab67043..e40120f 100644 --- a/docs/source/index.rst +++ b/docs/source/index.rst @@ -21,5 +21,6 @@ formal tasks: autotune.rst verilog.rst verific.rst + appnotes.rst license.rst diff --git a/docs/source/install.rst b/docs/source/install.rst index 2e8e3ab..cc41dac 100644 --- a/docs/source/install.rst +++ b/docs/source/install.rst @@ -138,7 +138,7 @@ 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. itp-bmc ^^^^^^^ diff --git a/docs/source/reference.rst b/docs/source/reference.rst index b880ec3..8beefaa 100644 --- a/docs/source/reference.rst +++ b/docs/source/reference.rst @@ -111,6 +111,10 @@ The :sby:`[tasks]` section must appear in the ``.sby`` file before the first The command ``sby --dumptasks `` prints the list of all tasks defined in a given ``.sby`` file. +Note that there is currently no way to specify dependencies on other tasks. For complex flows where such dependencies are needed, consider using separate ``.sby`` files, or a single file with external scripting. For an advanced example which uses tasks and external scripting to implement a multi-stage verification +flow, see `AppNote 130: Multi-Stage Verification +`_. + Options section --------------- @@ -124,6 +128,7 @@ Mode Description ``prove`` Unbounded model check to verify safety properties (``assert(...)`` statements) ``live`` Unbounded model check to verify liveness properties (``assert(s_eventually ...)`` statements) ``cover`` Generate set of shortest traces required to reach all cover() statements +``prep`` Prepare the design and write the preprocessed model without running solver engines ========= =========== .. @@ -176,6 +181,12 @@ options are: | | | ``model/design_.*`` files within the working | | | | directory, even when not required to run the task. | +-------------------+------------+---------------------------------------------------------+ +| ``skip_prep`` | All | Skip SBY's internal preparation step. Values: ``on``, | +| | | ``off``. Default: ``off``. For an example of how it can | +| | | be useful to disable the preparation step in complex | +| | | flows, see `AppNote 130: Multi-Stage Verification | +| | | `_. | ++-------------------+------------+---------------------------------------------------------+ | ``smtc`` | ``bmc``, | Pass this ``.smtc`` file to the smtbmc engine. All | | | ``prove``, | other engines are disabled when this option is used. | | | ``cover`` | Default: None | @@ -293,11 +304,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 +320,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 +402,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 +421,7 @@ solvers: +-------------------------------+---------------------------------+ | ``avy`` | ``prove`` | +-------------------------------+---------------------------------+ -| ``rIC3`` | ``prove`` | +| ``rIC3`` | ``bmc``, ``prove`` | +-------------------------------+---------------------------------+ | ``aigbmc`` | ``bmc`` | +-------------------------------+---------------------------------+ diff --git a/sbysrc/sby.py b/sbysrc/sby.py index 2d5a1da..315aa55 100644 --- a/sbysrc/sby.py +++ b/sbysrc/sby.py @@ -215,7 +215,7 @@ def read_sbyconfig(sbydata, taskname): tasks_section = False if task_skiping_blocks: - if line == "--": + if line.strip() == "--": task_skip_block = False task_skiping_blocks = False return @@ -365,7 +365,7 @@ if dump_files: find_files(taskname) else: find_files(None) - print("\n".join(file_set)) + print("\n".join(str(f) for f in file_set)) sys.exit(0) if dump_tags: diff --git a/sbysrc/sby_core.py b/sbysrc/sby_core.py index 1ffa2c8..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, @@ -1270,7 +1275,7 @@ class SbyTask(SbyConfig): print("formalff -clk2ff -ff2anyinit", file=f) print("simplemap", file=f) print("dffunmap", file=f) - print("abc -g AND -fast", file=f) + print("aigmap", file=f) print("opt_clean", file=f) print("stat", file=f) print(f"write_aiger -I -B -zinit -no-startoffset {'-vmap' if self.opt_aigvmap else '-map'} design_aiger.aim" + @@ -1374,7 +1379,9 @@ class SbyTask(SbyConfig): self.handle_str_option("mode", None) - if self.opt_mode not in ["bmc", "prove", "cover", "live", "prep"]: + if self.opt_mode is None: + self.error("Missing mode. Please specify a `mode` in the [options] section.") + elif self.opt_mode not in ["bmc", "prove", "cover", "live", "prep"]: self.error(f"Invalid mode: {self.opt_mode}") self.expect = ["PASS"] 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/parser/.gitignore b/tests/parser/.gitignore deleted file mode 100644 index b87b190..0000000 --- a/tests/parser/.gitignore +++ /dev/null @@ -1,4 +0,0 @@ -* -!Makefile -!.gitignore -!*.sby diff --git a/tests/parser/Makefile b/tests/parser/Makefile deleted file mode 100644 index 7827c43..0000000 --- a/tests/parser/Makefile +++ /dev/null @@ -1,2 +0,0 @@ -SUBDIR=parser -include ../make/subdir.mk 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 diff --git a/tests/regression/yosys_5892_memname.sby b/tests/regression/yosys_5892_memname.sby new file mode 100644 index 0000000..412712f --- /dev/null +++ b/tests/regression/yosys_5892_memname.sby @@ -0,0 +1,55 @@ +[options] +mode bmc +depth 3 +expect fail + +[engines] +smtbmc bitwuzla + +[script] +read_verilog -sv top.sv +prep -top top -flatten + +[file top.sv] +module top(input logic clk, input logic [1:0] addr, input logic [7:0] data); + logic [7:0] value; + + wrapper wrapper ( + .clk(clk), + .addr(addr), + .data(data), + .value(value) + ); + + always_ff @(posedge clk) begin + assert (value != 8'hff); + end +endmodule + +module wrapper( + input logic clk, + input logic [1:0] addr, + input logic [7:0] data, + output logic [7:0] value +); + uut uut ( + .clk(clk), + .addr(addr), + .data(data), + .value(value) + ); +endmodule + +module uut( + input logic clk, + input logic [1:0] addr, + input logic [7:0] data, + output logic [7:0] value +); + logic [7:0] \mem\with\backslash [0:3]; + + always_ff @(posedge clk) begin + \mem\with\backslash [addr] <= data; + value <= \mem\with\backslash [addr]; + end +endmodule diff --git a/tools/cexenum/cexenum.py b/tools/cexenum/cexenum.py index d180835..40a571d 100755 --- a/tools/cexenum/cexenum.py +++ b/tools/cexenum/cexenum.py @@ -289,7 +289,7 @@ class AigModel(tl.process.Process): "formalff -clk2ff -ff2anyinit", "simplemap", "dffunmap", - "abc -g AND -fast", + "aigmap", "opt_clean", "stat", "write_rtlil design_aiger.il",