From f454c92bcf541273140ab193d1d659d4960de8dd Mon Sep 17 00:00:00 2001
From: Lenny Truong <lenny.truong@sifive.com>
Date: Fri, 1 Nov 2024 15:27:09 -0700
Subject: [PATCH 1/2] [circt-test] Add simple runner interface for choosing
 modes and depth

* Maintains default behavior of using `cover`, `bmc`, and `induction`
  tasks, but allows the user to supply a custom comma-separated `mode`
  string selecting specific tasks.  NOTE: The runner script still
  expects mode to be some subset of the above three.
* Adds a depth attribute/parameter for controlling bound or induction
  factor.  For now, this parameter is shared across all tasks.
---
 integration_test/circt-test/basic.mlir    |  6 ++--
 tools/circt-test/circt-test-runner-sby.py | 39 +++++++++++++++--------
 tools/circt-test/circt-test.cpp           | 22 +++++++++++++
 3 files changed, 51 insertions(+), 16 deletions(-)

diff --git a/integration_test/circt-test/basic.mlir b/integration_test/circt-test/basic.mlir
index e8cd39c46cec..864732b8ef45 100644
--- a/integration_test/circt-test/basic.mlir
+++ b/integration_test/circt-test/basic.mlir
@@ -86,7 +86,7 @@ verif.formal @ALUCanAdd {
   verif.assert %eq : i1
 }
 
-verif.formal @ALUCanSub {
+verif.formal @ALUCanSub attributes {mode = "cover,induction"} {
   %a = verif.symbolic_value : i4
   %b = verif.symbolic_value : i4
   %true = hw.constant true
@@ -96,7 +96,7 @@ verif.formal @ALUCanSub {
   verif.assert %eq : i1
 }
 
-verif.formal @ALUWorks {
+verif.formal @ALUWorks attributes {mode = "cover,bmc", depth = 5} {
   %a = verif.symbolic_value : i4
   %b = verif.symbolic_value : i4
   %sub = verif.symbolic_value : i1
@@ -132,7 +132,7 @@ verif.formal @ALUIgnoreFailure attributes {ignore = true} {
   verif.assert %ne : i1
 }
 
-verif.formal @ALUFailure {
+verif.formal @ALUFailure attributes {depth = 3} {
   %a = verif.symbolic_value : i4
   %b = verif.symbolic_value : i4
   %sub = verif.symbolic_value : i1
diff --git a/tools/circt-test/circt-test-runner-sby.py b/tools/circt-test/circt-test-runner-sby.py
index fd1dd43e0271..d4dd11c28c4b 100755
--- a/tools/circt-test/circt-test-runner-sby.py
+++ b/tools/circt-test/circt-test-runner-sby.py
@@ -9,29 +9,42 @@
 parser.add_argument("verilog")
 parser.add_argument("-t", "--test")
 parser.add_argument("-d", "--directory")
+parser.add_argument("-m", "--mode")
+parser.add_argument("-k", "--depth")
 args = parser.parse_args()
 
 directory = Path(args.directory)
 source_path = Path(args.verilog)
 script_path = directory / "script.sby"
 
+if args.mode is not None:
+    tasks = args.mode.split(",")
+else:
+    tasks = ["cover", "bmc", "induction"]
+
+depth = f"depth {args.depth}" if args.depth is not None else ""
+
+options = """
+  [options]
+"""
+for task in tasks:
+    mode = {
+        "induction": "prove"
+    }.get(task, task)
+    options += f"""
+  {task}:
+  mode {mode}
+  {depth}
+  --
+"""
+
+
 # Generate the SymbiYosys script.
 script = f"""
   [tasks]
-  cover
-  bmc
-  induction
+  {('\n  ').join(tasks)}
 
-  [options]
-  cover:
-  mode cover
-  --
-  bmc:
-  mode bmc
-  --
-  induction:
-  mode prove
-  --
+{options}
 
   [engines]
   smtbmc z3
diff --git a/tools/circt-test/circt-test.cpp b/tools/circt-test/circt-test.cpp
index 258c44b0c3a1..3453325bf376 100644
--- a/tools/circt-test/circt-test.cpp
+++ b/tools/circt-test/circt-test.cpp
@@ -315,6 +315,28 @@ static LogicalResult execute(MLIRContext *context) {
     args.push_back("-d");
     args.push_back(testDir);
 
+    if (auto mode = test.attrs.get("mode")) {
+      args.push_back("-m");
+      auto modeStr = dyn_cast<StringAttr>(mode);
+      if (!modeStr) {
+        mlir::emitError(test.loc) << "invalid mode for test " << test.name;
+        return;
+      }
+      args.push_back(cast<StringAttr>(mode).getValue());
+    }
+
+    if (auto depth = test.attrs.get("depth")) {
+      args.push_back("-k");
+      auto depthInt = dyn_cast<IntegerAttr>(depth);
+      if (!depthInt) {
+        mlir::emitError(test.loc) << "invalid depth for test " << test.name;
+        return;
+      }
+      SmallVector<char> str;
+      depthInt.getValue().toStringUnsigned(str);
+      args.push_back(std::string(str.begin(), str.end()));
+    }
+
     // Execute the test runner.
     std::string errorMessage;
     auto result =

From 6d29fad535882dbaba21f114dae99a435a6621e3 Mon Sep 17 00:00:00 2001
From: Lenny Truong <lenny.truong@sifive.com>
Date: Sun, 3 Nov 2024 08:14:35 -0600
Subject: [PATCH 2/2] Python format

---
 tools/circt-test/circt-test-runner-sby.py | 11 ++++-------
 1 file changed, 4 insertions(+), 7 deletions(-)

diff --git a/tools/circt-test/circt-test-runner-sby.py b/tools/circt-test/circt-test-runner-sby.py
index d4dd11c28c4b..31dfcff0775d 100755
--- a/tools/circt-test/circt-test-runner-sby.py
+++ b/tools/circt-test/circt-test-runner-sby.py
@@ -18,9 +18,9 @@
 script_path = directory / "script.sby"
 
 if args.mode is not None:
-    tasks = args.mode.split(",")
+  tasks = args.mode.split(",")
 else:
-    tasks = ["cover", "bmc", "induction"]
+  tasks = ["cover", "bmc", "induction"]
 
 depth = f"depth {args.depth}" if args.depth is not None else ""
 
@@ -28,17 +28,14 @@
   [options]
 """
 for task in tasks:
-    mode = {
-        "induction": "prove"
-    }.get(task, task)
-    options += f"""
+  mode = {"induction": "prove"}.get(task, task)
+  options += f"""
   {task}:
   mode {mode}
   {depth}
   --
 """
 
-
 # Generate the SymbiYosys script.
 script = f"""
   [tasks]