[Moore] Add assert, assume, and conver ops.

include/circt/Dialect/Moore/MooreOps.td

@@ -1329,4 +1329,47 @@ def YieldOp : MooreOp<"yield", [
   let hasVerifier = 1;
 }
 
+//===----------------------------------------------------------------------===//
+// Assertions
+//===----------------------------------------------------------------------===//
+
+// Simple immediate assertions, like `assert`.
+def ImmediateAssert: I32EnumAttrCase<"Immediate", 0, "immediate">;
+// Observed deferred assertions, like `assert #0`.
+def ObservedAssert: I32EnumAttrCase<"Observed", 1, "observed">;
+// Final deferred assertions, like `assert final`.
+def FinalAssert: I32EnumAttrCase<"Final", 2, "final">;
+
+// A mode specifying how immediate/deferred assertions operate.
+def DeferAssertAttr : I32EnumAttr<
+  "DeferAssert", "assertion deferring mode",
+  [ImmediateAssert, ObservedAssert, FinalAssert]>
+{
+  let cppNamespace = "circt::moore";
+}
+
+class ImmediateAssertOp<string mnemonic, list<Trait> traits = []> : 
+    MooreOp<mnemonic, traits # [HasParent<"ProcedureOp">]>{
+  let arguments = (ins
+    DeferAssertAttr:$defer,
+    AnySingleBitType:$cond,
+    OptionalAttr<StrAttr>:$label
+  );
+  let assemblyFormat = [{
+    $defer $cond (`label` $label^)? attr-dict `:` type($cond)
+  }];
+}
+
+def AssertOp : ImmediateAssertOp<"assert">{
+  let summary = "If cond is not true, an error should be thrown.";
+}
+
+def AssumeOp : ImmediateAssertOp<"assume">{
+  let summary = "Verify the cond whether has the expected behavior.";
+}
+
+def CoverOp : ImmediateAssertOp<"cover">{
+  let summary = "Monitor the coverage information.";
+}
+
 #endif // CIRCT_DIALECT_MOORE_MOOREOPS

lib/Conversion/ImportVerilog/Statements.cpp

@@ -13,6 +13,16 @@ using namespace mlir;
 using namespace circt;
 using namespace ImportVerilog;
 
+static moore::DeferAssert convertDeferAssert(bool isDeferred, bool isFinal) {
+  if (isDeferred && isFinal)
+    return moore::DeferAssert::Final;
+  if (isDeferred && !isFinal)
+    return moore::DeferAssert::Observed;
+  if (!isDeferred && !isFinal)
+    return moore::DeferAssert::Immediate;
+  llvm_unreachable("all immediate assertions are handled");
+}
+
 // NOLINTBEGIN(misc-no-recursion)
 namespace {
 struct StmtVisitor {
@@ -463,6 +473,31 @@ struct StmtVisitor {
     return success();
   }
 
+  // Handle immediate assertion statements.
+  LogicalResult visit(const slang::ast::ImmediateAssertionStatement &stmt) {
+    auto cond = context.convertRvalueExpression(stmt.cond);
+    cond = context.convertToBool(cond);
+    if (!cond)
+      return failure();
+
+    auto defer = convertDeferAssert(stmt.isDeferred, stmt.isFinal);
+    switch (stmt.assertionKind) {
+    case slang::ast::AssertionKind::Assert:
+      builder.create<moore::AssertOp>(loc, defer, cond, StringAttr{});
+      return success();
+    case slang::ast::AssertionKind::Assume:
+      builder.create<moore::AssumeOp>(loc, defer, cond, StringAttr{});
+      return success();
+    case slang::ast::AssertionKind::CoverProperty:
+      builder.create<moore::CoverOp>(loc, defer, cond, StringAttr{});
+      return success();
+    default:
+      break;
+    }
+    mlir::emitError(loc, "all immediate assertions handled");
+    return failure();
+  }
+
   /// Emit an error for all other statements.
   template <typename T>
   LogicalResult visit(T &&stmt) {

test/Conversion/ImportVerilog/basic.sv

@@ -1904,3 +1904,28 @@ task automatic ImplicitEventControlExamples();
     x[a] = !b;
   end
 endtask
+
+// CHECK-LABEL: moore.module @ImmediateAssert(in %clk : !moore.l1) 
+module ImmediateAssert(input clk);
+  // CHECK: [[CLK:%.+]] = moore.net name "clk" wire : <l1>
+  // CHECK: [[A:%.+]] = moore.variable : <i1>
+  bit a;
+
+  // CHECK: moore.procedure always
+    // CHECK: [[READ_CLK:%.+]] = moore.read [[CLK]] : <l1>
+    // CHECK: [[OneBX:%.+]] = moore.constant bX : l1
+    // CHECK: [[NE:%.+]] = moore.ne [[READ_CLK]], [[OneBX]] : l1 -> l1
+    // CHECK: moore.assert immediate [[NE]] : l1
+  assert (clk != 1'bx);
+
+  // CHECK: moore.procedure always
+    // CHECK: [[C100:%.+]] = moore.constant 100 : i32
+    // CHECK: [[BC:%.+]] = moore.bool_cast [[C100]] : i32 -> i1
+    // CHECK: moore.assume observed [[BC]] : i1
+  assume #0 (100);
+
+  // CHECK: moore.procedure always
+    // CHECK: [[READ_A:%.+]] = moore.read [[A]] : <i1>
+    // CHECK: moore.cover final [[READ_A]] : i1
+  cover final (a);
+endmodule