From 05d963b0df224767c8fc0e09e9d93821218e1cfa Mon Sep 17 00:00:00 2001
From: Jannis Harder <me@jix.one>
Date: Tue, 14 Jun 2022 17:15:32 +0200
Subject: [PATCH] aiger: check supported modes and aigbmc fixes

---
 sbysrc/sby_engine_aiger.py | 13 +++++++++++--
 sbysrc/sby_mode_bmc.py     |  4 ++++
 tests/unsorted/bmc_len.sby | 36 ++++++++++++++++++++++++++++++++++++
 3 files changed, 51 insertions(+), 2 deletions(-)
 create mode 100644 tests/unsorted/bmc_len.sby

diff --git a/sbysrc/sby_engine_aiger.py b/sbysrc/sby_engine_aiger.py
index 4665691..2850d46 100644
--- a/sbysrc/sby_engine_aiger.py
+++ b/sbysrc/sby_engine_aiger.py
@@ -28,16 +28,25 @@ def run(mode, task, engine_idx, engine):
     for o, a in opts:
         task.error("Unexpected AIGER engine options.")
 
+    status_2 = "UNKNOWN"
+
     if solver_args[0] == "suprove":
+        if mode not in ["live", "prove"]:
+            task.error("The aiger solver 'suprove' is only supported in live and prove modes.")
         if mode == "live" and (len(solver_args) == 1 or solver_args[1][0] != "+"):
             solver_args.insert(1, "+simple_liveness")
         solver_cmd = " ".join([task.exe_paths["suprove"]] + solver_args[1:])
 
     elif solver_args[0] == "avy":
+        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] == "aigbmc":
-        solver_cmd = " ".join([task.exe_paths["aigbmc"]] + solver_args[1:])
+        if mode != "bmc":
+            task.error("The aiger solver 'aigbmc' is only supported in bmc mode.")
+        solver_cmd = " ".join([task.exe_paths["aigbmc"], str(task.opt_depth - 1)] + solver_args[1:])
+        status_2 = "PASS"  # aigbmc outputs status 2 when BMC passes
 
     else:
         task.error(f"Invalid solver command {solver_args[0]}.")
@@ -76,7 +85,7 @@ def run(mode, task, engine_idx, engine):
             print(line, file=aiw_file)
             if line == "0": proc_status = "PASS"
             if line == "1": proc_status = "FAIL"
-            if line == "2": proc_status = "UNKNOWN"
+            if line == "2": proc_status = status_2
 
         return None
 
diff --git a/sbysrc/sby_mode_bmc.py b/sbysrc/sby_mode_bmc.py
index fd128ed..85ef882 100644
--- a/sbysrc/sby_mode_bmc.py
+++ b/sbysrc/sby_mode_bmc.py
@@ -39,6 +39,10 @@ def run(task):
             import sby_engine_abc
             sby_engine_abc.run("bmc", task, engine_idx, engine)
 
+        elif engine[0] == "aiger":
+            import sby_engine_aiger
+            sby_engine_aiger.run("bmc", task, engine_idx, engine)
+
         elif engine[0] == "btor":
             import sby_engine_btor
             sby_engine_btor.run("bmc", task, engine_idx, engine)
diff --git a/tests/unsorted/bmc_len.sby b/tests/unsorted/bmc_len.sby
new file mode 100644
index 0000000..938a1bd
--- /dev/null
+++ b/tests/unsorted/bmc_len.sby
@@ -0,0 +1,36 @@
+[tasks]
+smtbmc_pass: smtbmc pass
+smtbmc_fail: smtbmc fail
+aigbmc_pass: aigbmc pass
+aigbmc_fail: aigbmc fail
+btormc_pass: btormc pass
+btormc_fail: btormc fail
+abc_pass: abc pass
+abc_fail: abc fail
+
+[options]
+mode bmc
+pass: expect pass
+fail: expect fail
+pass: depth 5
+fail: depth 6
+
+[engines]
+smtbmc: smtbmc boolector
+aigbmc: aiger aigbmc
+btormc: btor btormc
+abc: abc bmc3
+
+[script]
+read -formal top.sv
+prep -top top
+
+[file top.sv]
+module top(input clk);
+    reg [7:0] counter = 0;
+
+    always @(posedge clk) begin
+        counter <= counter + 1;
+        assert (counter < 4);
+    end
+endmodule
-- 
2.30.2