[circt-test] Add runner for circt-bmc

Add a runner script for `circt-bmc` to circt-test. This allows CIRCT's
own model checker to be used to verify `verif.formal` operations in MLIR
inputs. The user currently has to pass the runner to circt-test
explicitly using the `-r` option. In the future, we'll want to add a
mechanism to circt-test to list available runners, check if the needed
software is installed on the system, and configure new local runners
through some config file.

integration_test/CMakeLists.txt

@@ -11,7 +11,7 @@ set(CIRCT_INTEGRATION_TEST_DEPENDS
   circt-lec
   circt-bmc
   circt-test
-  circt-test-runner-sby
+  circt-test-runners
   firtool
   hlstool
   ibistool

integration_test/circt-test/basic-circt-bmc.mlir

@@ -0,0 +1,3 @@
+// RUN: env Z3LIB=%libz3 not circt-test %S/basic.mlir -r circt-test-runner-circt-bmc.py --mlir-runner 2>&1 | FileCheck %S/basic.mlir
+// REQUIRES: libz3
+// REQUIRES: circt-bmc-jit

integration_test/circt-test/basic-sby.mlir

@@ -0,0 +1,2 @@
+// RUN: not circt-test %S/basic.mlir -r circt-test-runner-sby.py 2>&1 | FileCheck %S/basic.mlir
+// REQUIRES: sby

integration_test/circt-test/basic.mlir

@@ -1,5 +1,5 @@
-// RUN: circt-test %s -r circt-test-runner-sby.py | FileCheck %s
-// REQUIRES: sby
+// See other `basic-*.mlir` files for run lines.
+// RUN: true
 
 // CHECK: 1 tests FAILED, 6 passed, 1 ignored
 
@@ -66,7 +66,7 @@ verif.formal @CustomAdderWorks {} {
   %0 = comb.icmp eq %z0, %c5_i4 : i4
   %1 = comb.icmp ne %a, %b : i4
   %2 = comb.and %0, %1 : i1
-  verif.cover %2 : i1
+  // verif.cover %2 : i1  // not supported in circt-bmc currently
 }
 
 hw.module @ALU(in %a: i4, in %b: i4, in %sub: i1, out z: i4) {

tools/circt-test/CMakeLists.txt

@@ -29,5 +29,16 @@ target_link_libraries(circt-test PRIVATE ${libs})
 llvm_update_compile_flags(circt-test)
 mlir_check_all_link_libraries(circt-test)
 
-configure_file(circt-test-runner-sby.py ${CIRCT_TOOLS_DIR}/circt-test-runner-sby.py)
-add_custom_target(circt-test-runner-sby SOURCES ${CIRCT_TOOLS_DIR}/circt-test-runner-sby.py)
+set(all_runner_paths "")
+foreach(runner sby circt-bmc)
+  set(src_path ${CMAKE_CURRENT_SOURCE_DIR}/circt-test-runner-${runner}.py)
+  set(dst_path ${CIRCT_TOOLS_DIR}/circt-test-runner-${runner}.py)
+  add_custom_command(
+    OUTPUT ${dst_path}
+    DEPENDS ${src_path}
+    COMMAND ${CMAKE_COMMAND} -E copy ${src_path} ${dst_path}
+  )
+  list(APPEND all_runner_paths ${dst_path})
+endforeach()
+add_custom_target(circt-test-runners DEPENDS ${all_runner_paths})
+add_dependencies(circt-test circt-test-runners)

tools/circt-test/circt-test-runner-circt-bmc.py

@@ -0,0 +1,44 @@
+#!/usr/bin/env python3
+from pathlib import Path
+import argparse
+import os
+import shlex
+import subprocess
+import sys
+
+parser = argparse.ArgumentParser()
+parser.add_argument("mlir")
+parser.add_argument("-t", "--test", required=True)
+parser.add_argument("-d", "--directory", required=True)
+parser.add_argument("-m", "--mode")
+parser.add_argument("-k", "--depth", type=int)
+args = parser.parse_args()
+
+# Use circt-opt to lower any `verif.formal` ops to `hw.module`s. Once circt-bmc
+# natively supports `verif.formal`, we can directly run it on the input MLIR.
+lowered_mlir = Path(args.directory) / "lowered.mlir"
+cmd = ["circt-opt", args.mlir, "-o", lowered_mlir, "--lower-formal-to-hw"]
+sys.stderr.write("# " + shlex.join(str(c) for c in cmd) + "\n")
+sys.stderr.flush()
+result = subprocess.call(cmd)
+if result != 0:
+  sys.exit(result)
+
+# Run circt-bmc. We currently have to capture the output and look for a specific
+# string to know if the verification passed or failed. Once the tool properly
+# exits on test failure, we can skip this.
+cmd = ["circt-bmc", lowered_mlir]
+cmd += ["-b", str(args.depth or 20)]
+cmd += ["--module", args.test]
+cmd += ["--shared-libs", os.environ.get("Z3LIB", "/usr/lib/libz3.so")]
+
+sys.stderr.write("# " + shlex.join(str(c) for c in cmd) + "\n")
+sys.stderr.flush()
+with open(Path(args.directory) / "output.log", "w") as output:
+  result = subprocess.call(cmd, stdout=output, stderr=output)
+with open(Path(args.directory) / "output.log", "r") as output:
+  output_str = output.read()
+sys.stderr.write(output_str)
+if result != 0:
+  sys.exit(result)
+sys.exit(0 if "Bound reached with no violations" in output_str else 1)

tools/circt-test/circt-test.cpp

@@ -86,6 +86,11 @@ struct Options {
   cl::opt<std::string> runner{
       "r", cl::desc("Program to run individual tests"), cl::value_desc("bin"),
       cl::init("circt-test-runner-sby.py"), cl::cat(cat)};
+
+  cl::opt<bool> runnerReadsMLIR{
+      "mlir-runner",
+      cl::desc("Pass the MLIR file to the runner instead of Verilog"),
+      cl::init(false), cl::cat(cat)};
 };
 Options opts;
 
@@ -309,7 +314,10 @@ static LogicalResult execute(MLIRContext *context) {
     // Assemble the runner arguments.
     SmallVector<StringRef> args;
     args.push_back(runner);
-    args.push_back(verilogPath);
+    if (opts.runnerReadsMLIR)
+      args.push_back(opts.inputFilename);
+    else
+      args.push_back(verilogPath);
     args.push_back("-t");
     args.push_back(test.name.getValue());
     args.push_back("-d");