Support rIC3 as backend

Signed-off-by: Yuheng Su <[email protected]>

docs/examples/demos/up_down_counter.sby

@@ -1,13 +1,15 @@
 [tasks]
 suprove
 avy
+rIC3
 
 [options]
 mode prove
 
 [engines]
 suprove: aiger suprove
 avy: aiger avy
+rIC3: aiger rIC3
 
 [script]
 read_verilog -formal demo.v

docs/source/install.rst

@@ -133,3 +133,7 @@ super_prove
 Avy
 ^^^
   https://arieg.bitbucket.io/avy/
+
+rIC3
+^^^
+  https://github.com/gipsyh/rIC3/

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``                       |
 +-------------------------------+---------------------------------+
 

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

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

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