mirrors/sby
3
0
Fork 0
mirror of https://github.com/YosysHQ/sby.git synced 2026-07-30 16:14:01 +00:00
Code Activity

Merge branch 'main' into add-itp-engine

Browse source
This commit is contained in:
Pratik Deshmukh 2026-07-16 21:40:46 +05:30 • committed by GitHub
commit 9121eb0380
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
20 changed files with 367 additions and 41 deletions
Download patch file Download diff file Expand all files Collapse all files

26
.github/workflows/ci.yml vendored
View file

@ -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: |

6
.github/workflows/codeql.yml vendored
View file

@ -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

9
docs/source/appnotes.rst Normal file
View file

@ -0,0 +1,9 @@
Application Notes
=================
Formal Basics and Methods
--------------------------
- `109 Property Checking with SVA <https://yosyshq.readthedocs.io/projects/ap109>`_
- `120 Weak precondition cover and witness for SVA properties <https://yosyshq.readthedocs.io/projects/ap120>`_
- `130 Multi-Stage Verification <https://yosyshq.readthedocs.io/projects/ap130>`_

1
docs/source/index.rst
View file

@ -21,5 +21,6 @@ formal tasks:
autotune.rst
verilog.rst
verific.rst
appnotes.rst
license.rst

2
docs/source/install.rst
View file

@ -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
^^^^^^^

23
docs/source/reference.rst
View file

@ -111,6 +111,10 @@ The :sby:`[tasks]` section must appear in the ``.sby`` file before the first
The command ``sby --dumptasks <sby_file>`` 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
<https://yosyshq.readthedocs.io/projects/ap130>`_.
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_<name>.*`` 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 |
| | | <https://yosyshq.readthedocs.io/projects/ap130>`_. |
+-------------------+------------+---------------------------------------------------------+
| ``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`` |
+-------------------------------+---------------------------------+

4
sbysrc/sby.py
View file

@ -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:

19
sbysrc/sby_core.py
View file

@ -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"]

21
sbysrc/sby_engine_aiger.py
View file

@ -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:

85
sbysrc/sby_engine_btor.py
View file

@ -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

4
sbysrc/sby_mode_prove.py
View file

@ -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)

1
sbysrc/sby_sim.py
View file

@ -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

2
tests/make/required_tools.py
View file

@ -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"],
}

4
tests/parser/.gitignore vendored
View file

@ -1,4 +0,0 @@
*
!Makefile
!.gitignore
!*.sby

2
tests/parser/Makefile
View file

@ -1,2 +0,0 @@
SUBDIR=parser
include ../make/subdir.mk

21
tests/regression/aiger_comb_witness.sby Normal file
View file

@ -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

46
tests/regression/aiger_options.sby Normal file
View file

@ -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

75
tests/regression/btor_options.sby Normal file
View file

@ -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

55
tests/regression/yosys_5892_memname.sby Normal file
View file

@ -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

2
tools/cexenum/cexenum.py
View file

@ -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",