[LLHD] Allow verif ops in comb canonicalization

lib/Dialect/LLHD/IR/CMakeLists.txt

@@ -14,6 +14,7 @@ add_circt_dialect_library(CIRCTLLHD
   LINK_LIBS PUBLIC
   CIRCTHW
   CIRCTComb
+  CIRCTVerif
   MLIRIR
   MLIRSideEffectInterfaces
   MLIRControlFlowInterfaces

lib/Dialect/LLHD/IR/LLHDOps.cpp

@@ -10,6 +10,7 @@
 
 #include "circt/Dialect/Comb/CombOps.h"
 #include "circt/Dialect/HW/HWOps.h"
+#include "circt/Dialect/Verif/VerifOps.h"
 #include "circt/Support/CustomDirectiveImpl.h"
 #include "mlir/IR/Attributes.h"
 #include "mlir/IR/BuiltinDialect.h"
@@ -765,14 +766,36 @@ LogicalResult ProcessOp::canonicalize(ProcessOp op, PatternRewriter &rewriter) {
 LogicalResult CombinationalOp::canonicalize(CombinationalOp op,
                                             PatternRewriter &rewriter) {
   // Inline the combinational region if it consists of a single block and
-  // contains no side-effecting operations.
-  if (op.getBody().hasOneBlock() && isMemoryEffectFree(op)) {
-    auto &block = op.getBody().front();
-    auto *terminator = block.getTerminator();
-    rewriter.inlineBlockBefore(&block, op, ValueRange{});
-    rewriter.replaceOp(op, terminator->getOperands());
-    rewriter.eraseOp(terminator);
-    return success();
+  // contains no side-effecting operations, exception for verif assert like
+  // operations.
+  // The exception can be made because the verif ops are linked to the values
+  // via their operands and do not rely on the activation of the
+  // CombinationalOp environment.
+  if (op.getBody().hasOneBlock()) {
+    bool hasUnwantedEffects = false;
+    op.getBody().walk([&](Operation *inner) {
+      if (isa<circt::verif::AssertOp, verif::AssumeOp, verif::CoverOp>(inner))
+        return WalkResult::advance();
+      if (auto memInterface = dyn_cast<MemoryEffectOpInterface>(inner)) {
+        if (!memInterface.hasNoEffect()) {
+          hasUnwantedEffects = true;
+          return WalkResult::interrupt();
+        }
+      } else if (!inner->hasTrait<OpTrait::HasRecursiveMemoryEffects>()) {
+        hasUnwantedEffects = true;
+        return WalkResult::interrupt();
+      }
+      return WalkResult::advance();
+    });
+
+    if (!hasUnwantedEffects) {
+      auto &block = op.getBody().front();
+      auto *terminator = block.getTerminator();
+      rewriter.inlineBlockBefore(&block, op, ValueRange{});
+      rewriter.replaceOp(op, terminator->getOperands());
+      rewriter.eraseOp(terminator);
+      return success();
+    }
   }
   return failure();
 }

test/Dialect/LLHD/Canonicalization/processes.mlir

@@ -36,6 +36,22 @@ hw.module @InlineCombinational(in %a: i42, in %b: i42, in %c: i8917, out u: i42,
   hw.output %0, %1 : i42, i9001
 }
 
+// CHECK-LABEL: hw.module @InlineCombinationalVerif(
+hw.module @InlineCombinationalVerif(in %a: i1, in %b: i1, in %c: i1, out u: i1, out
+v: i3) {
+  // CHECK-NEXT: [[TMP1:%.+]] = comb.xor %a, %b
+  // CHECK-NEXT: verif.assert [[TMP1]] label "" : i1
+  // CHECK-NEXT: [[TMP2:%.+]] = comb.concat %a, %b, %c
+  // CHECK-NEXT: hw.output [[TMP1]], [[TMP2]]
+  %0, %1 = llhd.combinational -> i1, i3 {
+    %2 = comb.xor %a, %b : i1
+    verif.assert %2 label "" : i1
+    %3 = comb.concat %a, %b, %c : i1, i1, i1
+    llhd.yield %2, %3 : i1, i3
+  }
+  hw.output %0, %1 : i1, i3
+}
+
 // CHECK-LABEL: hw.module @IgnoreMultiBlockHalt
 hw.module @IgnoreMultiBlockHalt(in %a : i1, in %b : i1, out v1 : i1, out v2 : i1) {
   // CHECK: llhd.halt %a, %a