[circt-test] Add simple runner interface for choosing modes and depth (…

…llvm#7763)

* 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

@@ -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

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

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 =