mirrors/sby
3
0
Fork 0
mirror of https://github.com/YosysHQ/sby.git synced 2025-04-12 08:28:16 +00:00
Code Activity

update rIC3 backend

Browse source 
Signed-off-by: Yuheng Su <gipsyh.icu@gmail.com>
This commit is contained in:
Yuheng Su 2024-12-17 04:41:58 +00:00
parent daf4e4cb39
commit 8da7174b16
3 changed files with 5 additions and 3 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
docs/examples/demos/up_down_counter.sby
View file

@ -1,7 +1,6 @@
[tasks] [tasks]
suprove suprove
avy avy
rIC3
[options] [options]
mode prove mode prove
@ -9,7 +8,6 @@ mode prove
[engines] [engines]
suprove: aiger suprove suprove: aiger suprove
avy: aiger avy avy: aiger avy
rIC3: aiger rIC3
[script] [script]
read_verilog -formal demo.v read_verilog -formal demo.v

4
docs/source/install.rst
View file

@ -137,3 +137,7 @@ Avy
rIC3 rIC3
^^^^ ^^^^
https://github.com/gipsyh/rIC3/ https://github.com/gipsyh/rIC3/
The minimum required version is 1.3.0
rIC3 is not allowed to be used for any commercial purposes without authorization.

2
sbysrc/sby_engine_aiger.py
View file

@ -50,7 +50,7 @@ def run(mode, task, engine_idx, engine):
elif solver_args[0] == "rIC3": elif solver_args[0] == "rIC3":
if mode != "prove": if mode != "prove":
task.error("The aiger solver 'rIC3' is only supported in prove mode.") task.error("The aiger solver 'rIC3' is only supported in prove mode.")
solver_cmd = " ".join([task.exe_paths["rIC3"], "-v0", "--sby"] + solver_args[1:]) solver_cmd = " ".join([task.exe_paths["rIC3"], "--witness"] + solver_args[1:])
elif solver_args[0] == "aigbmc": elif solver_args[0] == "aigbmc":
if mode != "bmc": if mode != "bmc":