[Moore] Add assert, assume, and conver ops. (#7589)

These immediate assertion ops borrow from the SV dialect.

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

@@ -463,6 +463,76 @@ 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();
+
+    // Handle assertion statements that don't have an action block.
+    if (stmt.ifTrue && stmt.ifTrue->as_if<slang::ast::EmptyStatement>()) {
+      auto defer = moore::DeferAssert::Immediate;
+      if (stmt.isFinal)
+        defer = moore::DeferAssert::Final;
+      else if (stmt.isDeferred)
+        defer = moore::DeferAssert::Observed;
+
+      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) << "unsupported immediate assertion kind: "
+                           << slang::ast::toString(stmt.assertionKind);
+      return failure();
+    }
+
+    // Regard assertion statements with an action block as the "if-else".
+    cond = builder.create<moore::ConversionOp>(loc, builder.getI1Type(), cond);
+
+    // Create the blocks for the true and false branches, and the exit block.
+    Block &exitBlock = createBlock();
+    Block *falseBlock = stmt.ifFalse ? &createBlock() : nullptr;
+    Block &trueBlock = createBlock();
+    builder.create<cf::CondBranchOp>(loc, cond, &trueBlock,
+                                     falseBlock ? falseBlock : &exitBlock);
+
+    // Generate the true branch.
+    builder.setInsertionPointToEnd(&trueBlock);
+    if (stmt.ifTrue && failed(context.convertStatement(*stmt.ifTrue)))
+      return failure();
+    if (!isTerminated())
+      builder.create<cf::BranchOp>(loc, &exitBlock);
+
+    if (stmt.ifFalse) {
+      // Generate the false branch if present.
+      builder.setInsertionPointToEnd(falseBlock);
+      if (failed(context.convertStatement(*stmt.ifFalse)))
+        return failure();
+      if (!isTerminated())
+        builder.create<cf::BranchOp>(loc, &exitBlock);
+    }
+
+    // If control never reaches the exit block, remove it and mark control flow
+    // as terminated. Otherwise we continue inserting ops in the exit block.
+    if (exitBlock.hasNoPredecessors()) {
+      exitBlock.erase();
+      setTerminated();
+    } else {
+      builder.setInsertionPointToEnd(&exitBlock);
+    }
+    return success();
+  }
+
   /// Emit an error for all other statements.
   template <typename T>
   LogicalResult visit(T &&stmt) {

test/Conversion/ImportVerilog/basic.sv

@@ -1904,3 +1904,78 @@ 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
+
+// CHECK-LABEL: moore.module @ImmediateAssertiWithActionBlock() 
+module ImmediateAssertiWithActionBlock;
+  logic x;
+  int a;
+// CHEK: moore.procedure always {
+  // CHEK: [[READ_X:%.+]] = moore.read %x : <l1>
+  // CHEK: [[CONV_X:%.+]] = moore.conversion [[READ_X]] : !moore.l1 -> i1
+  // CHEK: cf.cond_br [[CONV_X]], ^bb1, ^bb2
+// CHEK: ^bb1:  // pred: ^bb0
+  // CHEK: [[C1:%.+]] = moore.constant 1 : i32
+  // CHEK: moore.blocking_assign %a, [[C1]] : i32
+  // CHEK: cf.br ^bb2
+// CHEK: ^bb2:  // 2 preds: ^bb0, ^bb1
+  // CHEK:   moore.return
+// CHEK: }
+  assert (x) a = 1;
+
+// CHEK: moore.procedure always {
+  // CHEK: [[READ_X:%.+]] = moore.read %x : <l1>
+  // CHEK: [[CONV_X:%.+]] = moore.conversion [[READ_X]] : !moore.l1 -> i1
+  // CHEK: cf.cond_br [[CONV_X]], ^bb1, ^bb2
+// CHEK: ^bb1:  // pred: ^bb0
+  // CHEK: cf.br ^bb3
+// CHEK: ^bb2:  // pred: ^bb0
+  // CHEK: [[C0:%.+]] = moore.constant 0 : i32
+  // CHEK: moore.blocking_assign %a, [[C0]] : i32
+  // CHEK: cf.br ^bb3
+// CHEK: ^bb3:  // 2 preds: ^bb1, ^bb2
+  // CHEK: moore.return
+// CHEK: }
+  assert (x) else a = 0;
+
+// CHEK: moore.procedure always {
+  // CHEK: [[READ_X:%.+]] = moore.read %x : <l1>
+  // CHEK: [[CONV_X:%.+]] = moore.conversion [[READ_X]] : !moore.l1 -> i1
+  // CHEK: cf.cond_br [[CONV_X]], ^bb1, ^bb2
+// CHEK: ^bb1:  // pred: ^bb0
+  // CHEK: [[C1:%.+]] = moore.constant 1 : i32
+  // CHEK: moore.blocking_assign %a, [[C1]] : i32
+  // CHEK: cf.br ^bb3
+// CHEK: ^bb2:  // pred: ^bb0
+  // CHEK: [[C0:%.+]] = moore.constant 0 : i32
+  // CHEK: moore.blocking_assign %a, [[C0]] : i32
+  // CHEK: cf.br ^bb3
+// CHEK: ^bb3:  // 2 preds: ^bb1, ^bb2
+  // CHEK: moore.return
+// CHEK: }
+  assert (x) a = 1; else a = 0;
+endmodule