From acd335d21509efd04b3a8ea7f21b5785e654efa5 Mon Sep 17 00:00:00 2001
From: mingzheTerapines <166383385+mingzheTerapines@users.noreply.github.com>
Date: Fri, 11 Oct 2024 09:40:59 +0800
Subject: [PATCH] [MooreToCore] Support assert, assume, cover ops (#7681)

* [MooreToCore] Support assert, assume, cover ops

Add conversion patterns from moore.{assert,assume,cover} to the corresponding verif.* op in MooreToConv. Consider rejecting deferred assertions for now. https://chipsalliance.github.io/sv-tests-results/?v=circt_verilog+16.2+assert_test
Fix issue https://github.com/llvm/circt/issues/7630


* Do not differentiate between the different scheduling regions in SV
---
 include/circt/Conversion/Passes.td         |  2 +-
 lib/Conversion/MooreToCore/CMakeLists.txt  |  1 +
 lib/Conversion/MooreToCore/MooreToCore.cpp | 29 ++++++++++++++++++++--
 test/Conversion/MooreToCore/basic.mlir     | 13 ++++++++++
 4 files changed, 42 insertions(+), 3 deletions(-)

diff --git a/include/circt/Conversion/Passes.td b/include/circt/Conversion/Passes.td
index 791c998bfd32..31e224c85b67 100644
--- a/include/circt/Conversion/Passes.td
+++ b/include/circt/Conversion/Passes.td
@@ -517,7 +517,7 @@ def ConvertMooreToCore : Pass<"convert-moore-to-core", "mlir::ModuleOp"> {
   let constructor = "circt::createConvertMooreToCorePass()";
   let dependentDialects = ["comb::CombDialect", "hw::HWDialect",
                            "llhd::LLHDDialect", "mlir::cf::ControlFlowDialect",
-                           "mlir::scf::SCFDialect"];
+                           "mlir::scf::SCFDialect", "verif::VerifDialect"];
 }
 
 //===----------------------------------------------------------------------===//
diff --git a/lib/Conversion/MooreToCore/CMakeLists.txt b/lib/Conversion/MooreToCore/CMakeLists.txt
index bcc88ab2233f..999a36e79ddb 100644
--- a/lib/Conversion/MooreToCore/CMakeLists.txt
+++ b/lib/Conversion/MooreToCore/CMakeLists.txt
@@ -13,6 +13,7 @@ add_circt_conversion_library(CIRCTMooreToCore
   CIRCTHW
   CIRCTLLHD
   CIRCTMoore
+  CIRCTVerif
   MLIRControlFlowDialect
   MLIRFuncDialect
   MLIRSCFDialect
diff --git a/lib/Conversion/MooreToCore/MooreToCore.cpp b/lib/Conversion/MooreToCore/MooreToCore.cpp
index 200dc183ab9c..127edf5a4865 100644
--- a/lib/Conversion/MooreToCore/MooreToCore.cpp
+++ b/lib/Conversion/MooreToCore/MooreToCore.cpp
@@ -16,6 +16,7 @@
 #include "circt/Dialect/HW/HWOps.h"
 #include "circt/Dialect/LLHD/IR/LLHDOps.h"
 #include "circt/Dialect/Moore/MooreOps.h"
+#include "circt/Dialect/Verif/VerifOps.h"
 #include "mlir/Dialect/ControlFlow/IR/ControlFlowOps.h"
 #include "mlir/Dialect/Func/IR/FuncOps.h"
 #include "mlir/Dialect/SCF/IR/SCF.h"
@@ -1237,6 +1238,24 @@ struct InPlaceOpConversion : public OpConversionPattern<SourceOp> {
   }
 };
 
+template <typename MooreOpTy, typename VerifOpTy>
+struct AssertLikeOpConversion : public OpConversionPattern<MooreOpTy> {
+  using OpConversionPattern<MooreOpTy>::OpConversionPattern;
+  using OpAdaptor = typename MooreOpTy::Adaptor;
+
+  LogicalResult
+  matchAndRewrite(MooreOpTy op, OpAdaptor adaptor,
+                  ConversionPatternRewriter &rewriter) const override {
+    StringAttr label =
+        op.getLabel().has_value()
+            ? StringAttr::get(op->getContext(), op.getLabel().value())
+            : StringAttr::get(op->getContext());
+    rewriter.replaceOpWithNewOp<VerifOpTy>(op, adaptor.getCond(), mlir::Value(),
+                                           label);
+    return success();
+  }
+};
+
 } // namespace
 
 //===----------------------------------------------------------------------===//
@@ -1250,6 +1269,7 @@ static void populateLegality(ConversionTarget &target,
   target.addLegalDialect<hw::HWDialect>();
   target.addLegalDialect<llhd::LLHDDialect>();
   target.addLegalDialect<comb::CombDialect>();
+  target.addLegalDialect<verif::VerifDialect>();
 
   target.addLegalOp<debug::ScopeOp>();
 
@@ -1423,7 +1443,7 @@ static void populateOpConversion(RewritePatternSet &patterns,
     ICmpOpConversion<WildcardNeOp, ICmpPredicate::wne>,
     CaseXZEqOpConversion<CaseZEqOp, true>,
     CaseXZEqOpConversion<CaseXZEqOp, false>,
-    
+
     // Patterns of structural operations.
     SVModuleOpConversion, InstanceOpConversion, ProcedureOpConversion, WaitEventOpConversion,
 
@@ -1444,7 +1464,12 @@ static void populateOpConversion(RewritePatternSet &patterns,
     CallOpConversion, UnrealizedConversionCastConversion,
     InPlaceOpConversion<debug::ArrayOp>,
     InPlaceOpConversion<debug::StructOp>,
-    InPlaceOpConversion<debug::VariableOp>
+    InPlaceOpConversion<debug::VariableOp>,
+
+    // Patterns of assert-like operations
+    AssertLikeOpConversion<AssertOp, verif::AssertOp>,
+    AssertLikeOpConversion<AssumeOp, verif::AssumeOp>,
+    AssertLikeOpConversion<CoverOp, verif::CoverOp>
   >(typeConverter, context);
   // clang-format on
   mlir::populateAnyFunctionOpInterfaceTypeConversionPattern(patterns,
diff --git a/test/Conversion/MooreToCore/basic.mlir b/test/Conversion/MooreToCore/basic.mlir
index b342270cd04a..8a21a601eba9 100644
--- a/test/Conversion/MooreToCore/basic.mlir
+++ b/test/Conversion/MooreToCore/basic.mlir
@@ -836,3 +836,16 @@ dbg.variable "b", %dbg0 scope %dbg1 : !moore.l32
 dbg.array [%dbg0] : !moore.l32
 // CHECK: dbg.struct {"q": [[TMP]]} : i32
 dbg.struct {"q": %dbg0} : !moore.l32
+
+// CHECK-LABEL: hw.module @Assert
+moore.module @Assert(in %cond : !moore.l1)  {
+  moore.procedure always {
+  // CHECK: verif.assert %cond label "cond" : i1
+  moore.assert immediate %cond label "cond" : l1
+  // CHECK: verif.assume %cond label "" : i1
+  moore.assume observed %cond  : l1
+  // CHECK: verif.cover %cond label "" : i1
+  moore.cover final %cond : l1
+  moore.return
+  }
+}