[Verif] Add StripContracts pass

Add a simple pass that removes all contracts from the IR, treating them
as passthroughs. Run the pass in firtool's HW-to-SV pipeline early on to
add additional optimization opportunities. ExportVerilog will eventually
ignore contracts anyway.

include/circt/Dialect/Verif/Passes.td

@@ -71,4 +71,12 @@ def SimplifyAssumeEqPass : Pass<"simplify-assume-eq", "hw::HWModuleOp"> {
   }];
 }
 
+def StripContractsPass : Pass<"strip-contracts"> {
+  let summary = "Remove contracts from the IR";
+  let description = [{
+    Replaces all `verif.contract` ops in the IR with their operands, making them
+    act as simple passthroughs.
+  }];
+}
+
 #endif // CIRCT_DIALECT_VERIF_PASSES_TD

lib/Dialect/Verif/Transforms/CMakeLists.txt

@@ -1,9 +1,10 @@
 add_circt_dialect_library(CIRCTVerifTransforms
-  VerifyClockedAssertLike.cpp
-  PrepareForFormal.cpp
-  LowerFormalToHW.cpp
   LowerContracts.cpp
+  LowerFormalToHW.cpp
+  PrepareForFormal.cpp
   SimplifyAssumeEq.cpp
+  StripContracts.cpp
+  VerifyClockedAssertLike.cpp
 
   DEPENDS
   CIRCTVerifTransformsIncGen

lib/Dialect/Verif/Transforms/StripContracts.cpp

@@ -0,0 +1,44 @@
+//===- StripContracts.cpp -------------------------------------------------===//
+//
+// Part of the LLVM Project, under the Apache License v2.0 with LLVM Exceptions.
+// See https://llvm.org/LICENSE.txt for license information.
+// SPDX-License-Identifier: Apache-2.0 WITH LLVM-exception
+//
+//===----------------------------------------------------------------------===//
+
+#include "circt/Dialect/Verif/VerifOps.h"
+#include "circt/Dialect/Verif/VerifPasses.h"
+#include "mlir/Pass/Pass.h"
+
+namespace circt {
+namespace verif {
+#define GEN_PASS_DEF_STRIPCONTRACTSPASS
+#include "circt/Dialect/Verif/Passes.h.inc"
+} // namespace verif
+} // namespace circt
+
+using namespace mlir;
+using namespace circt;
+using namespace verif;
+
+namespace {
+struct StripContractsPass
+    : public verif::impl::StripContractsPassBase<StripContractsPass> {
+  void runOnOperation() override {
+    getOperation()->walk([](ContractOp op) {
+      op->replaceUsesWithIf(op.getInputs(), [&](OpOperand &operand) {
+        return operand.getOwner() != op;
+      });
+      // Prevent removal of self-referential contracts that have other users.
+      // Removing them would result in invalid IR.
+      for (auto operand : op->getOperands())
+        if (operand.getDefiningOp() == op)
+          for (auto *user : operand.getUsers())
+            if (user != op)
+              return;
+      op->dropAllReferences();
+      op->erase();
+    });
+  }
+};
+} // namespace

lib/Firtool/Firtool.cpp

@@ -304,6 +304,7 @@ LogicalResult firtool::populateLowFIRRTLToHW(mlir::PassManager &pm,
 
 LogicalResult firtool::populateHWToSV(mlir::PassManager &pm,
                                       const FirtoolOptions &opt) {
+  pm.nestAny().addPass(verif::createStripContractsPass());
   pm.addPass(verif::createLowerFormalToHWPass());
 
   if (opt.shouldExtractTestCode())

test/Dialect/Verif/strip-contracts.mlir

@@ -0,0 +1,25 @@
+// RUN: circt-opt --strip-contracts %s | FileCheck %s
+
+// CHECK-LABEL: func @foo
+func.func @foo(%arg0: i42) -> i42 {
+  // CHECK-NOT: verif.contract
+  %0 = verif.contract %arg0 : i42 {}
+  // CHECK: return %arg0
+  return %0 : i42
+}
+
+// CHECK-LABEL: hw.module @bar
+hw.module @bar() {
+  // CHECK-NOT: verif.contract
+  %0 = verif.contract %1 : i42 {}
+  %1 = verif.contract %0 : i42 {}
+}
+
+// CHECK-LABEL: hw.module @baz
+hw.module @baz(out z: i42) {
+  // CHECK: [[TMP:%.+]] = verif.contract [[TMP]]
+  // CHECK: hw.output [[TMP]]
+  %2 = verif.contract %3 : i42 {}
+  %3 = verif.contract %2 : i42 {}
+  hw.output %3 : i42
+}