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..31dfcff0775d 100755
--- a/tools/circt-test/circt-test-runner-sby.py
+++ b/tools/circt-test/circt-test-runner-sby.py
@@ -9,29 +9,39 @@
 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 =