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

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