small fixes + add regression tests for aiger and btor engines exercising all options

sbysrc/sby_engine_btor.py

@@ -34,7 +34,7 @@ def run(mode, task, engine_idx, engine):
     for o, a in opts:
         if o == "--seed":
             random_seed = a
-        if o == "--nomem":
+        elif o == "--nomem":
             nomem_opt = True
         elif o == "--syn":
             syn_opt = True
@@ -47,8 +47,8 @@ def run(mode, task, engine_idx, engine):
     if nomem_opt: model_name += "_nomem"
 
     if solver_args[0] == "btormc":
-        if mode != "bmc":
-            task.error("The btormc solver is only supported in bmc mode.")
+        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} "
@@ -134,6 +134,9 @@ def run(mode, task, engine_idx, engine):
             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.")

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