[Verif] Add LowerFormalToHW pass (llvm#7707)

* Rewrites `verif.formal` to `hw.module`
* Lifts `verif.symbolic_value` to be an input to the module

include/circt/Dialect/Verif/Passes.td

@@ -42,4 +42,14 @@ def VerifyClockedAssertLike : Pass<"verify-clocked-assert-like", "hw::HWModuleOp
   let constructor = "circt::verif::createVerifyClockedAssertLikePass()";
 }
 
+/**
+ * Converts verif.formal ops into hw.module.
+ */
+def LowerFormalToHW : Pass<"lower-formal-to-hw", "mlir::ModuleOp"> {
+  let summary = "Lower verif.formal ops to hw.module ops.";
+  let description = [{
+    Converts verif.formal ops into hw.module ops.
+  }];
+}
+
 #endif // CIRCT_DIALECT_VERIF_PASSES_TD

include/circt/Dialect/Verif/VerifPasses.h

@@ -14,17 +14,22 @@
 #ifndef CIRCT_DIALECT_VERIF_VERIFPASSES_H
 #define CIRCT_DIALECT_VERIF_VERIFPASSES_H
 
-#include "circt/Dialect/HW/HWOps.h"
 #include "mlir/Pass/Pass.h"
 #include "mlir/Pass/PassRegistry.h"
 #include <memory>
-#include <optional>
+
+namespace circt {
+namespace verif {
+class FormalOp;
+} // namespace verif
+} // namespace circt
 
 namespace circt {
 namespace verif {
 
 std::unique_ptr<mlir::Pass> createVerifyClockedAssertLikePass();
 std::unique_ptr<mlir::Pass> createPrepareForFormalPass();
+std::unique_ptr<mlir::Pass> createLowerFormalToHW();
 
 #define GEN_PASS_REGISTRATION
 #include "circt/Dialect/Verif/Passes.h.inc"

lib/Dialect/Verif/Transforms/CMakeLists.txt

@@ -1,6 +1,7 @@
 add_circt_dialect_library(CIRCTVerifTransforms
   VerifyClockedAssertLike.cpp
   PrepareForFormal.cpp
+  LowerFormalToHW.cpp
 
   DEPENDS
   CIRCTVerifTransformsIncGen

lib/Dialect/Verif/Transforms/LowerFormalToHW.cpp

@@ -0,0 +1,76 @@
+//===- LowerFormalToHW.cpp - Formal Preparations --*- C++ -*---------------===//
+//
+// 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
+//===----------------------------------------------------------------------===//
+//
+// Lower verif.formal to hw.module.
+//
+//===----------------------------------------------------------------------===//
+#include "circt/Dialect/Verif/VerifOps.h"
+#include "circt/Dialect/Verif/VerifPasses.h"
+
+#include "mlir/Transforms/GreedyPatternRewriteDriver.h"
+
+using namespace circt;
+
+namespace circt {
+namespace verif {
+#define GEN_PASS_DEF_LOWERFORMALTOHW
+#include "circt/Dialect/Verif/Passes.h.inc"
+} // namespace verif
+} // namespace circt
+
+using namespace mlir;
+using namespace verif;
+
+namespace {
+struct LowerFormalToHW
+    : circt::verif::impl::LowerFormalToHWBase<LowerFormalToHW> {
+  void runOnOperation() override;
+};
+
+struct FormalOpRewritePattern : public OpRewritePattern<verif::FormalOp> {
+  using OpRewritePattern<FormalOp>::OpRewritePattern;
+
+  LogicalResult matchAndRewrite(FormalOp op,
+                                PatternRewriter &rewriter) const override {
+    // Create the ports for all the symbolic values
+    SmallVector<hw::PortInfo> ports;
+    for (auto symOp : op.getBody().front().getOps<verif::SymbolicValueOp>()) {
+      ports.push_back(
+          hw::PortInfo({{rewriter.getStringAttr("symbolic_value_" +
+                                                std::to_string(ports.size())),
+                         symOp.getType(), hw::ModulePort::Input}}));
+    }
+
+    auto moduleOp =
+        rewriter.create<hw::HWModuleOp>(op.getLoc(), op.getNameAttr(), ports);
+
+    rewriter.inlineBlockBefore(&op.getBody().front(),
+                               &moduleOp.getBodyBlock()->front(),
+                               op.getBody().getArguments());
+
+    // Replace symbolic values with module arguments
+    size_t i = 0;
+    for (auto symOp : make_early_inc_range(
+             moduleOp.getBodyBlock()->getOps<SymbolicValueOp>())) {
+      rewriter.replaceAllUsesWith(symOp.getResult(),
+                                  moduleOp.getArgumentForInput(i));
+      i++;
+      rewriter.eraseOp(symOp);
+    }
+    rewriter.eraseOp(op);
+    return success();
+  }
+};
+} // namespace
+
+void LowerFormalToHW::runOnOperation() {
+  RewritePatternSet patterns(&getContext());
+  patterns.add<FormalOpRewritePattern>(patterns.getContext());
+
+  if (failed(applyPatternsAndFoldGreedily(getOperation(), std::move(patterns))))
+    signalPassFailure();
+}

test/Dialect/Verif/lower-formal-to-hw.mlir

@@ -0,0 +1,16 @@
+// RUN: circt-opt --lower-formal-to-hw %s | FileCheck %s
+
+hw.module @Foo(in %bar : i32, in %baz : i16, in %clk : !seq.clock) {}
+
+// CHECK-LABEL: hw.module @FormalTop(in %symbolic_value_0 : i32, in %symbolic_value_1 : i16)
+verif.formal @FormalTop {
+  %0 = verif.symbolic_value : i32
+  %1 = verif.symbolic_value : i16
+  // CHECK: [[CLK:%[0-9]+]] = seq.const_clock high
+  %high = seq.const_clock high
+  %2 = comb.extract %0 from 16 :  (i32) -> i16
+  // CHECK: [[RES:%[0-9]+]] = comb.xor
+  %3 = comb.xor %1, %2 : i16
+  // CHECK: hw.instance "foo" @Foo(bar: %symbolic_value_0: i32, baz: [[RES]]: i16, clk: [[CLK]]: !seq.clock)
+  hw.instance "foo" @Foo(bar: %0: i32, baz: %3: i16, clk: %high: !seq.clock) -> ()
+}