Add verif.bmc VerifToSMT lowering (#7603)

Co-authored-by: Martin Erhart <[email protected]>
llvm · Sep 24, 2024 · c601695 · c601695
1 parent 685cc3b
commit c601695
Show file tree

Hide file tree

Showing 8 changed files with 509 additions and 13 deletions.
diff --git a/include/circt/Conversion/Passes.td b/include/circt/Conversion/Passes.td
@@ -699,7 +699,12 @@ def ConvertHWToSMT : Pass<"convert-hw-to-smt", "mlir::ModuleOp"> {
 
 def ConvertVerifToSMT : Pass<"convert-verif-to-smt", "mlir::ModuleOp"> {
   let summary = "Convert Verif ops to SMT ops";
-  let dependentDialects = ["smt::SMTDialect", "mlir::arith::ArithDialect"];
+  let dependentDialects = [
+    "smt::SMTDialect",
+    "mlir::arith::ArithDialect",
+    "mlir::scf::SCFDialect",
+    "mlir::func::FuncDialect"
+  ];
 }
 
 //===----------------------------------------------------------------------===//

diff --git a/include/circt/Conversion/VerifToSMT.h b/include/circt/Conversion/VerifToSMT.h
@@ -13,13 +13,15 @@
 #include <memory>
 
 namespace circt {
+class Namespace;
 
 #define GEN_PASS_DECL_CONVERTVERIFTOSMT
 #include "circt/Conversion/Passes.h.inc"
 
 /// Get the Verif to SMT conversion patterns.
 void populateVerifToSMTConversionPatterns(TypeConverter &converter,
-                                          RewritePatternSet &patterns);
+                                          RewritePatternSet &patterns,
+                                          Namespace &names);
 
 } // namespace circt
 

diff --git a/lib/Conversion/HWToSMT/CMakeLists.txt b/lib/Conversion/HWToSMT/CMakeLists.txt
@@ -10,6 +10,7 @@ add_circt_conversion_library(CIRCTHWToSMT
   LINK_LIBS PUBLIC
   CIRCTHW
   CIRCTSMT
+  CIRCTSeq
   MLIRFuncDialect
   MLIRTransforms
   MLIRTransformUtils

diff --git a/lib/Conversion/HWToSMT/HWToSMT.cpp b/lib/Conversion/HWToSMT/HWToSMT.cpp
@@ -9,6 +9,7 @@
 #include "circt/Conversion/HWToSMT.h"
 #include "circt/Dialect/HW/HWOps.h"
 #include "circt/Dialect/SMT/SMTOps.h"
+#include "circt/Dialect/Seq/SeqOps.h"
 #include "mlir/Analysis/TopologicalSortUtils.h"
 #include "mlir/Dialect/Func/IR/FuncOps.h"
 #include "mlir/Pass/Pass.h"
@@ -92,6 +93,20 @@ struct InstanceOpConversion : OpConversionPattern<InstanceOp> {
   }
 };
 
+/// Remove redundant (seq::FromClock and seq::ToClock) ops.
+template <typename OpTy>
+struct ReplaceWithInput : OpConversionPattern<OpTy> {
+  using OpConversionPattern<OpTy>::OpConversionPattern;
+  using OpAdaptor = typename OpTy::Adaptor;
+
+  LogicalResult
+  matchAndRewrite(OpTy op, OpAdaptor adaptor,
+                  ConversionPatternRewriter &rewriter) const override {
+    rewriter.replaceOp(op, adaptor.getOperands());
+    return success();
+  }
+};
+
 } // namespace
 
 //===----------------------------------------------------------------------===//
@@ -118,6 +133,9 @@ void circt::populateHWToSMTTypeConverter(TypeConverter &converter) {
       return std::nullopt;
     return smt::BitVectorType::get(type.getContext(), type.getWidth());
   });
+  converter.addConversion([](seq::ClockType type) -> std::optional<Type> {
+    return smt::BitVectorType::get(type.getContext(), 1);
+  });
 
   // Default target materialization to convert from illegal types to legal
   // types, e.g., at the boundary of an inlined child block.
@@ -200,12 +218,16 @@ void circt::populateHWToSMTTypeConverter(TypeConverter &converter) {
 void circt::populateHWToSMTConversionPatterns(TypeConverter &converter,
                                               RewritePatternSet &patterns) {
   patterns.add<HWConstantOpConversion, HWModuleOpConversion, OutputOpConversion,
-               InstanceOpConversion>(converter, patterns.getContext());
+               InstanceOpConversion, ReplaceWithInput<seq::ToClockOp>,
+               ReplaceWithInput<seq::FromClockOp>>(converter,
+                                                   patterns.getContext());
 }
 
 void ConvertHWToSMTPass::runOnOperation() {
   ConversionTarget target(getContext());
   target.addIllegalDialect<hw::HWDialect>();
+  target.addIllegalOp<seq::FromClockOp>();
+  target.addIllegalOp<seq::ToClockOp>();
   target.addLegalDialect<smt::SMTDialect>();
   target.addLegalDialect<mlir::func::FuncDialect>();
 

diff --git a/lib/Conversion/VerifToSMT/CMakeLists.txt b/lib/Conversion/VerifToSMT/CMakeLists.txt
@@ -13,6 +13,8 @@ add_circt_conversion_library(CIRCTVerifToSMT
   CIRCTSMT
   CIRCTVerif
   MLIRArithDialect
+  MLIRFuncDialect
+  MLIRSCFDialect
   MLIRTransforms
   MLIRTransformUtils
   MLIRReconcileUnrealizedCasts