Merge pull request #367 from YosysHQ/ric3

Support rIC3 solver with btor engine

docs/source/install.rst

@@ -138,4 +138,4 @@ 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.

docs/source/reference.rst

@@ -293,11 +293,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 +309,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 +391,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 +410,7 @@ solvers:
 +-------------------------------+---------------------------------+
 | ``avy``                       |   ``prove``                     |
 +-------------------------------+---------------------------------+
-| ``rIC3``                      |   ``prove``                     |
+| ``rIC3``                      |   ``bmc``, ``prove``            |
 +-------------------------------+---------------------------------+
 | ``aigbmc``                    |   ``bmc``                       |
 +-------------------------------+---------------------------------+

sbysrc/sby_core.py

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

sbysrc/sby_engine_aiger.py

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

sbysrc/sby_engine_btor.py

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

sbysrc/sby_mode_prove.py

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

sbysrc/sby_sim.py

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

tests/make/required_tools.py

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

tests/regression/aiger_comb_witness.sby

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

tests/regression/aiger_options.sby

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

tests/regression/btor_options.sby

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