From daf4e4cb39a367a48655f72542c3ba4fa6bbbd20 Mon Sep 17 00:00:00 2001 From: Yuheng Su Date: Mon, 16 Dec 2024 11:02:45 +0000 Subject: [PATCH 1/2] Support rIC3 as backend Signed-off-by: Yuheng Su --- 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 cb922eb3..4ad57349 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 ba578d20..ddd8eb57 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 7b92d7c2..6f9c09ce 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 2c676daf..812c0c5e 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="", action=DictAction, dest="exe_paths") + parser.add_argument("--rIC3", metavar="", + action=DictAction, dest="exe_paths") parser.add_argument("--btormc", metavar="", action=DictAction, dest="exe_paths") parser.add_argument("--pono", metavar="", diff --git a/sbysrc/sby_core.py b/sbysrc/sby_core.py index c0444d73..c181c187 100644 --- a/sbysrc/sby_core.py +++ b/sbysrc/sby_core.py @@ -849,6 +849,7 @@ def __init__(self, sbyconfig, workdir, early_logs, reusedir, taskloop=None, logf "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 f18e35d8..d8c78536 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 Date: Tue, 17 Dec 2024 04:41:58 +0000 Subject: [PATCH 2/2] update rIC3 backend Signed-off-by: Yuheng Su --- 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 4ad57349..cb922eb3 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 ddd8eb57..1f9c81a8 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 d8c78536..07fc965a 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":