[circt-test] Add support for contracts (#8166)

Add the `LowerContracts` or `StripContracts` pass to the circt-test
pipeline in order to leverage contracts during formal verification. To
make this work, circt-test has to run a preparatory pass pipeline on the
input MLIR, and pass the result as input to the MLIR runners instead of
the original file.

Also add an `--ir` option to dump the IR after the preparatory passes.

test/circt-test/pipeline.mlir

@@ -0,0 +1,20 @@
+// RUN: circt-test --ir %s | FileCheck %s
+// RUN: circt-test --ir --ignore-contracts %s | FileCheck %s --check-prefix=NOCONTRACT
+
+// CHECK: hw.module @Foo
+// CHECK-NOT: verif.contract
+// CHECK: verif.formal @Foo_CheckContract
+
+// NOCONTRACT: hw.module @Foo
+// NOCONTRACT-NOT: verif.contract
+// NOCONTRACT-NOT: verif.formal @Foo
+
+hw.module @Foo(in %a: i1, in %b: i1, out z: i1) {
+  %0 = comb.xor %a, %b : i1
+  %1 = verif.contract %0 : i1 {
+    %2 = comb.add %a, %b : i1
+    %3 = comb.icmp eq %1, %2 : i1
+    verif.ensure %3 : i1
+  }
+  hw.output %1 : i1
+}

tools/circt-test/circt-test.cpp

@@ -24,6 +24,7 @@
 #include "circt/Dialect/Verif/VerifOps.h"
 #include "circt/Dialect/Verif/VerifPasses.h"
 #include "circt/Support/JSON.h"
+#include "circt/Support/Passes.h"
 #include "circt/Support/Version.h"
 #include "mlir/Dialect/Arith/IR/Arith.h"
 #include "mlir/Dialect/ControlFlow/IR/ControlFlowOps.h"
@@ -35,6 +36,7 @@
 #include "mlir/Pass/PassManager.h"
 #include "mlir/Support/FileUtilities.h"
 #include "mlir/Support/ToolUtilities.h"
+#include "mlir/Transforms/Passes.h"
 #include "llvm/ADT/ScopeExit.h"
 #include "llvm/Support/CommandLine.h"
 #include "llvm/Support/FileSystem.h"
@@ -82,15 +84,23 @@ struct Options {
       "d", cl::desc("Result directory (default `.circt-test`)"),
       cl::value_desc("dir"), cl::init(".circt-test"), cl::cat(cat)};
 
-  cl::opt<bool> verifyPasses{
-      "verify-each",
-      cl::desc("Run the verifier after each transformation pass"),
-      cl::init(true), cl::cat(cat)};
-
   cl::list<std::string> runners{"r", cl::desc("Use a specific set of runners"),
                                 cl::value_desc("name"),
                                 cl::MiscFlags::CommaSeparated, cl::cat(cat)};
 
+  cl::opt<bool> ignoreContracts{
+      "ignore-contracts",
+      cl::desc("Do not use contracts to simplify and parallelize tests"),
+      cl::init(false), cl::cat(cat)};
+
+  cl::opt<bool> emitIR{"ir", cl::desc("Emit IR after initial lowering"),
+                       cl::init(false), cl::cat(cat)};
+
+  cl::opt<bool> verifyPasses{
+      "verify-each",
+      cl::desc("Run the verifier after each transformation pass"),
+      cl::init(true), cl::Hidden, cl::cat(cat)};
+
   cl::opt<bool> verifyDiagnostics{
       "verify-diagnostics",
       cl::desc("Check that emitted diagnostics match expected-* lines on the "
@@ -404,10 +414,38 @@ static LogicalResult listTests(TestSuite &suite) {
 static LogicalResult executeWithHandler(MLIRContext *context,
                                         RunnerSuite &runnerSuite,
                                         SourceMgr &srcMgr) {
+  std::string errorMessage;
   auto module = parseSourceFile<ModuleOp>(srcMgr, context);
   if (!module)
     return failure();
 
+  // Preprocess the input.
+  {
+    PassManager pm(context);
+    pm.enableVerifier(opts.verifyPasses);
+    if (opts.ignoreContracts)
+      pm.addPass(verif::createStripContractsPass());
+    else
+      pm.addPass(verif::createLowerContractsPass());
+    pm.addNestedPass<hw::HWModuleOp>(verif::createSimplifyAssumeEqPass());
+    pm.addPass(createCSEPass());
+    pm.addPass(createSimpleCanonicalizerPass());
+    if (failed(pm.run(*module)))
+      return failure();
+  }
+
+  // Emit the IR and exit if requested.
+  if (opts.emitIR) {
+    auto output = openOutputFile(opts.outputFilename, &errorMessage);
+    if (!output) {
+      WithColor::error() << errorMessage << "\n";
+      return failure();
+    }
+    module->print(output->os());
+    output->keep();
+    return success();
+  }
+
   // Discover all tests in the input.
   TestSuite suite(context, opts.listIgnored);
   if (failed(suite.discoverInModule(*module)))
@@ -428,10 +466,21 @@ static LogicalResult executeWithHandler(MLIRContext *context,
     return failure();
   }
 
+  // Generate the MLIR output.
+  SmallString<128> mlirPath(opts.resultDir);
+  llvm::sys::path::append(mlirPath, "design.mlir");
+  auto mlirFile = openOutputFile(mlirPath, &errorMessage);
+  if (!mlirFile) {
+    WithColor::error() << errorMessage << "\n";
+    return failure();
+  }
+  module->print(mlirFile->os());
+  mlirFile->os().flush();
+  mlirFile->keep();
+
   // Open the Verilog file for writing.
   SmallString<128> verilogPath(opts.resultDir);
   llvm::sys::path::append(verilogPath, "design.sv");
-  std::string errorMessage;
   auto verilogFile = openOutputFile(verilogPath, &errorMessage);
   if (!verilogFile) {
     WithColor::error() << errorMessage << "\n";
@@ -448,6 +497,7 @@ static LogicalResult executeWithHandler(MLIRContext *context,
   pm.addPass(createExportVerilogPass(verilogFile->os()));
   if (failed(pm.run(*module)))
     return failure();
+  verilogFile->os().flush();
   verilogFile->keep();
 
   // Run the tests.
@@ -502,7 +552,7 @@ static LogicalResult executeWithHandler(MLIRContext *context,
     SmallVector<StringRef> args;
     args.push_back(runner->binary);
     if (runner->readsMLIR)
-      args.push_back(opts.inputFilename);
+      args.push_back(mlirPath);
     else
       args.push_back(verilogPath);
     args.push_back("-t");