From daf4e4cb39a367a48655f72542c3ba4fa6bbbd20 Mon Sep 17 00:00:00 2001
From: Yuheng Su <gipsyh.icu@gmail.com>
Date: Mon, 16 Dec 2024 11:02:45 +0000
Subject: [PATCH 1/3] Support rIC3 as backend
Signed-off-by: Yuheng Su <gipsyh.icu@gmail.com>
---
docs/examples/demos/up_down_counter.sby | 2 ++
docs/source/install.rst | 4 ++++
docs/source/reference.rst | 4 ++++
sbysrc/sby_cmdline.py | 2 ++
sbysrc/sby_core.py | 1 +
sbysrc/sby_engine_aiger.py | 7 ++++++-
6 files changed, 19 insertions(+), 1 deletion(-)
diff --git a/docs/examples/demos/up_down_counter.sby b/docs/examples/demos/up_down_counter.sby
index cb922eb..4ad5734 100644
--- a/docs/examples/demos/up_down_counter.sby
+++ b/docs/examples/demos/up_down_counter.sby
@@ -1,6 +1,7 @@
[tasks]
suprove
avy
+rIC3
[options]
mode prove
@@ -8,6 +9,7 @@ mode prove
[engines]
suprove: aiger suprove
avy: aiger avy
+rIC3: aiger rIC3
[script]
read_verilog -formal demo.v
diff --git a/docs/source/install.rst b/docs/source/install.rst
index ba578d2..ddd8eb5 100644
--- a/docs/source/install.rst
+++ b/docs/source/install.rst
@@ -133,3 +133,7 @@ super_prove
Avy
^^^
https://arieg.bitbucket.io/avy/
+
+rIC3
+^^^^
+ https://github.com/gipsyh/rIC3/
diff --git a/docs/source/reference.rst b/docs/source/reference.rst
index 7b92d7c..6f9c09c 100644
--- a/docs/source/reference.rst
+++ b/docs/source/reference.rst
@@ -248,6 +248,8 @@ The following mode/engine/solver combinations are currently supported:
| | |
| | ``aiger avy`` |
| | |
+| | ``aiger rIC3`` |
+| | |
| | ``aiger suprove`` |
+-----------+--------------------------+
| ``cover`` | ``smtbmc [all solvers]`` |
@@ -341,6 +343,8 @@ solvers:
+-------------------------------+---------------------------------+
| ``avy`` | ``prove`` |
+-------------------------------+---------------------------------+
+| ``rIC3`` | ``prove`` |
++-------------------------------+---------------------------------+
| ``aigbmc`` | ``bmc`` |
+-------------------------------+---------------------------------+
diff --git a/sbysrc/sby_cmdline.py b/sbysrc/sby_cmdline.py
index 2c676da..812c0c5 100644
--- a/sbysrc/sby_cmdline.py
+++ b/sbysrc/sby_cmdline.py
@@ -49,6 +49,8 @@ def parser_func(release_version='unknown SBY version'):
action=DictAction, dest="exe_paths")
parser.add_argument("--avy", metavar="<path_to_executable>",
action=DictAction, dest="exe_paths")
+ parser.add_argument("--rIC3", metavar="<path_to_executable>",
+ action=DictAction, dest="exe_paths")
parser.add_argument("--btormc", metavar="<path_to_executable>",
action=DictAction, dest="exe_paths")
parser.add_argument("--pono", metavar="<path_to_executable>",
diff --git a/sbysrc/sby_core.py b/sbysrc/sby_core.py
index c0444d7..c181c18 100644
--- a/sbysrc/sby_core.py
+++ b/sbysrc/sby_core.py
@@ -849,6 +849,7 @@ class SbyTask(SbyConfig):
"suprove": os.getenv("SUPROVE", "suprove"),
"aigbmc": os.getenv("AIGBMC", "aigbmc"),
"avy": os.getenv("AVY", "avy"),
+ "rIC3": os.getenv("RIC3", "rIC3"),
"btormc": os.getenv("BTORMC", "btormc"),
"pono": os.getenv("PONO", "pono"),
"imctk-eqy-engine": os.getenv("IMCTK_EQY_ENGINE", "imctk-eqy-engine"),
diff --git a/sbysrc/sby_engine_aiger.py b/sbysrc/sby_engine_aiger.py
index f18e35d..d8c7853 100644
--- a/sbysrc/sby_engine_aiger.py
+++ b/sbysrc/sby_engine_aiger.py
@@ -46,6 +46,11 @@ def run(mode, task, engine_idx, engine):
if mode != "prove":
task.error("The aiger solver 'avy' is only supported in prove mode.")
solver_cmd = " ".join([task.exe_paths["avy"], "--cex", "-"] + solver_args[1:])
+
+ elif solver_args[0] == "rIC3":
+ if mode != "prove":
+ task.error("The aiger solver 'rIC3' is only supported in prove mode.")
+ solver_cmd = " ".join([task.exe_paths["rIC3"], "-v0", "--sby"] + solver_args[1:])
elif solver_args[0] == "aigbmc":
if mode != "bmc":
@@ -87,7 +92,7 @@ def run(mode, task, engine_idx, engine):
f"cd {task.workdir}; {solver_cmd} model/design_aiger{model_variant}.aig",
logfile=open(f"{task.workdir}/engine_{engine_idx}/logfile.txt", "w")
)
- if solver_args[0] not in ["avy"]:
+ if solver_args[0] not in ["avy", "rIC3"]:
proc.checkretcode = True
proc_status = None
From 8da7174b169b6969fa97b7dbc4e7a359d7cd7aa5 Mon Sep 17 00:00:00 2001
From: Yuheng Su <gipsyh.icu@gmail.com>
Date: Tue, 17 Dec 2024 04:41:58 +0000
Subject: [PATCH 2/3] update rIC3 backend
Signed-off-by: Yuheng Su <gipsyh.icu@gmail.com>
---
docs/examples/demos/up_down_counter.sby | 2 --
docs/source/install.rst | 4 ++++
sbysrc/sby_engine_aiger.py | 2 +-
3 files changed, 5 insertions(+), 3 deletions(-)
diff --git a/docs/examples/demos/up_down_counter.sby b/docs/examples/demos/up_down_counter.sby
index 4ad5734..cb922eb 100644
--- a/docs/examples/demos/up_down_counter.sby
+++ b/docs/examples/demos/up_down_counter.sby
@@ -1,7 +1,6 @@
[tasks]
suprove
avy
-rIC3
[options]
mode prove
@@ -9,7 +8,6 @@ mode prove
[engines]
suprove: aiger suprove
avy: aiger avy
-rIC3: aiger rIC3
[script]
read_verilog -formal demo.v
diff --git a/docs/source/install.rst b/docs/source/install.rst
index ddd8eb5..1f9c81a 100644
--- a/docs/source/install.rst
+++ b/docs/source/install.rst
@@ -137,3 +137,7 @@ Avy
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.
diff --git a/sbysrc/sby_engine_aiger.py b/sbysrc/sby_engine_aiger.py
index d8c7853..07fc965 100644
--- a/sbysrc/sby_engine_aiger.py
+++ b/sbysrc/sby_engine_aiger.py
@@ -50,7 +50,7 @@ def run(mode, task, engine_idx, engine):
elif solver_args[0] == "rIC3":
if mode != "prove":
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":
if mode != "bmc":
From fc0afb04c55413bf0d12aae57a0f580c99219a12 Mon Sep 17 00:00:00 2001
From: Yuheng Su <gipsyh.icu@gmail.com>
Date: Fri, 14 Mar 2025 22:00:09 +0800
Subject: [PATCH 3/3] Set minimum rIC3 version to 1.35
---
docs/source/install.rst | 4 +---
1 file changed, 1 insertion(+), 3 deletions(-)
diff --git a/docs/source/install.rst b/docs/source/install.rst
index 1f9c81a..27e5ec6 100644
--- a/docs/source/install.rst
+++ b/docs/source/install.rst
@@ -138,6 +138,4 @@ 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.
+The minimum required version is 1.3.5