[Verif] Add clocked Assert Assume Cover ops

include/circt/Dialect/Verif/CMakeLists.txt

@@ -1,2 +1,8 @@
 add_circt_dialect(Verif verif)
 add_circt_doc(VerifOps Dialects/VerifOps -gen-op-doc)
+
+set(LLVM_TARGET_DEFINITIONS Verif.td)
+mlir_tablegen(VerifEnums.h.inc -gen-enum-decls)
+mlir_tablegen(VerifEnums.cpp.inc -gen-enum-defs)
+add_public_tablegen_target(CIRCTVerifEnumsIncGen)
+add_dependencies(circt-headers CIRCTVerifEnumsIncGen)

include/circt/Dialect/Verif/VerifDialect.h

@@ -14,5 +14,6 @@
 #include "mlir/IR/Dialect.h"
 
 #include "circt/Dialect/Verif/VerifDialect.h.inc"
+#include "circt/Dialect/Verif/VerifEnums.h.inc"
 
 #endif // CIRCT_DIALECT_VERIF_VERIFDIALECT_H

include/circt/Dialect/Verif/VerifOps.td

@@ -10,10 +10,14 @@
 #define CIRCT_DIALECT_VERIF_VERIFOPS_TD
 
 include "circt/Dialect/Verif/VerifDialect.td"
+include "circt/Dialect/LTL/LTLDialect.td"
 include "circt/Dialect/LTL/LTLTypes.td"
 include "circt/Dialect/HW/HWTypes.td"
 include "mlir/Interfaces/InferTypeOpInterface.td"
 include "mlir/Interfaces/SideEffectInterfaces.td"
+include "mlir/IR/EnumAttr.td"
+include "mlir/IR/AttrTypeBase.td"
+include "mlir/IR/PatternBase.td"
 
 class VerifOp<string mnemonic, list<Trait> traits = []> :
   Op<VerifDialect, mnemonic, traits>;
@@ -43,6 +47,57 @@ def CoverOp : AssertLikeOp<"cover"> {
   let summary = "Ensure that a property can hold.";
 }
 
+// Edge behavior enum for always block.  See SV Spec 9.4.2.
+
+/// AtPosEdge triggers on a rise from 0 to 1/X/Z, or X/Z to 1.
+def AtPosEdge: I32EnumAttrCase<"Pos", 0, "posedge">;
+/// AtNegEdge triggers on a drop from 1 to 0/X/Z, or X/Z to 0.
+def AtNegEdge: I32EnumAttrCase<"Neg", 1, "negedge">;
+/// AtEdge is syntactic sugar for AtPosEdge or AtNegEdge.
+def AtEdge   : I32EnumAttrCase<"Both", 2, "edge">;
+
+def ClockEdgeAttr : I32EnumAttr<"ClockEdge", "clock edge",
+                                [AtPosEdge, AtNegEdge, AtEdge]> {
+  let cppNamespace = "circt::verif";
+}
+
+class ClockedAssertLikeOp<string mnemonic, list<Trait> traits = []> :
+  VerifOp<mnemonic, traits> {
+  let arguments = (ins LTLAnyPropertyType:$property,
+                      I1:$disable,
+                      ClockEdgeAttr:$edge, I1:$clock,
+                      OptionalAttr<StrAttr>:$label);
+  let assemblyFormat = [{
+    $property `disable` $disable `clock` $edge $clock 
+    (`label` $label^)? attr-dict `:` type($property)
+  }];
+  let hasVerifier = 1;
+}
+
+def ClockedAssertOp : ClockedAssertLikeOp<"clocked_assert"> {
+  let summary = [{ 
+    Assert that a property holds, checked on a given clock's 
+    ticks and disabled if a given condition holds. Only supports
+    a single clock and a single disable.
+  }];
+}
+
+def ClockedAssumeOp : ClockedAssertLikeOp<"clocked_assume"> {
+  let summary = [{ 
+    Assume that a property holds, checked on a given clock's 
+    ticks and disabled if a given condition holds. Only supports
+    a single clock and a single disable.
+  }];
+}
+
+def ClockedCoverOp : ClockedAssertLikeOp<"clocked_cover"> {
+  let summary = [{ 
+    Cover on the holding of a property, checked on a given clock's 
+    ticks and disabled if a given condition holds. Only supports
+    a single clock and a single disable.
+  }];
+}
+
 //===----------------------------------------------------------------------===//
 // Printing Formatted Messages
 //===----------------------------------------------------------------------===//

include/circt/Dialect/Verif/VerifVisitors.h

@@ -21,9 +21,11 @@ class Visitor {
   ResultType dispatchVerifVisitor(Operation *op, ExtraArgs... args) {
     auto *thisCast = static_cast<ConcreteType *>(this);
     return TypeSwitch<Operation *, ResultType>(op)
-        .template Case<AssertOp, AssumeOp, CoverOp>([&](auto op) -> ResultType {
-          return thisCast->visitVerif(op, args...);
-        })
+        .template Case<AssertOp, AssumeOp, CoverOp, ClockedAssertOp,
+                       ClockedAssumeOp, ClockedCoverOp>(
+            [&](auto op) -> ResultType {
+              return thisCast->visitVerif(op, args...);
+            })
         .Default([&](auto) -> ResultType {
           return thisCast->visitInvalidVerif(op, args...);
         });

lib/Conversion/ExportVerilog/ExportVerilog.cpp

@@ -70,6 +70,18 @@ using namespace pretty;
 StringRef circtHeader = "circt_header.svh";
 StringRef circtHeaderInclude = "`include \"circt_header.svh\"\n";
 
+static ltl::ClockEdge verifToltlClockEdge(verif::ClockEdge ce) {
+  switch (ce) {
+  case verif::ClockEdge::Pos:
+    return ltl::ClockEdge::Pos;
+  case verif::ClockEdge::Neg:
+    return ltl::ClockEdge::Neg;
+  case verif::ClockEdge::Both:
+    return ltl::ClockEdge::Both;
+  }
+  llvm_unreachable("Unknown event control kind");
+}
+
 namespace {
 /// This enum keeps track of the precedence level of various binary operators,
 /// where a lower number binds tighter.
@@ -3396,6 +3408,13 @@ class PropertyEmitter : public EmitterBase,
       Value property,
       PropertyPrecedence parenthesizeIfLooserThan = PropertyPrecedence::Lowest);
 
+  // Emits a property that is directly associated to a single clock and a single
+  // disable. Note that it is illegal to nest disable or clock operations in the
+  // property itself here.
+  void emitClockedProperty(
+      Value property, Value clock, ltl::ClockEdge edge, Value disable,
+      PropertyPrecedence parenthesizeIfLooserThan = PropertyPrecedence::Lowest);
+
 private:
   using ltl::Visitor<PropertyEmitter, EmittedProperty>::visitLTL;
   friend class ltl::Visitor<PropertyEmitter, EmittedProperty>;
@@ -3450,6 +3469,35 @@ void PropertyEmitter::emitProperty(
     buffer.flush(state.pp);
 }
 
+void PropertyEmitter::emitClockedProperty(
+    Value property, Value clock, ltl::ClockEdge edge, Value disable,
+    PropertyPrecedence parenthesizeIfLooserThan) {
+  assert(localTokens.empty());
+  // Wrap to this column.
+  ps << "@(";
+  ps.scopedBox(PP::ibox2, [&] {
+    ps << PPExtString(stringifyClockEdge(edge)) << PP::space;
+    emitNestedProperty(clock, PropertyPrecedence::Lowest);
+    ps << ")";
+  });
+
+  ps << PP::space;
+  ps << "disable iff" << PP::nbsp << "(";
+  ps.scopedBox(PP::ibox2, [&] {
+    emitNestedProperty(disable, PropertyPrecedence::Lowest);
+    ps << ")";
+  });
+
+  ps << PP::space;
+  ps.scopedBox(PP::ibox0,
+               [&] { emitNestedProperty(property, parenthesizeIfLooserThan); });
+  // If we are not using an external token buffer provided through the
+  // constructor, but we're using the default `PropertyEmitter`-scoped buffer,
+  // flush it.
+  if (&buffer.tokens == &localTokens)
+    buffer.flush(state.pp);
+}
+
 EmittedProperty PropertyEmitter::emitNestedProperty(
     Value property, PropertyPrecedence parenthesizeIfLooserThan) {
   // Emit the property as a plain expression if it doesn't have a property or
@@ -3839,6 +3887,14 @@ class StmtEmitter : public EmitterBase,
   LogicalResult visitVerif(verif::AssumeOp op);
   LogicalResult visitVerif(verif::CoverOp op);
 
+  LogicalResult emitVerifClockedAssertLike(Operation *op, Value property,
+                                           Value disable, Value clock,
+                                           verif::ClockEdge edge,
+                                           PPExtString opName);
+  LogicalResult visitVerif(verif::ClockedAssertOp op);
+  LogicalResult visitVerif(verif::ClockedAssumeOp op);
+  LogicalResult visitVerif(verif::ClockedCoverOp op);
+
 public:
   ModuleEmitter &emitter;
 
@@ -4579,17 +4635,15 @@ LogicalResult StmtEmitter::visitSV(CoverConcurrentOp op) {
 /// `verif.assert`, `verif.assume`, and `verif.cover`.
 LogicalResult StmtEmitter::emitVerifAssertLike(Operation *op, Value property,
                                                PPExtString opName) {
-  if (hasSVAttributes(op))
-    emitError(op, "SV attributes emission is unimplemented for the op");
 
   // If we are inside a procedural region we have the option of emitting either
   // an `assert` or `assert property`. If we are in a non-procedural region,
   // e.g., the body of a module, we have to use the concurrent form `assert
   // property` (which also supports plain booleans).
   //
-  // See IEEE 1800-2017 section 16.14.5 "Using concurrent assertion statements
-  // outside procedural code" and 16.14.6 "Embedding concurrent assertions in
-  // procedural code".
+  // See IEEE 1800-2017 section 16.14.5 "Using concurrent assertion
+  // statements outside procedural code" and 16.14.6 "Embedding concurrent
+  // assertions in procedural code".
   bool isTemporal = !property.getType().isSignlessInteger(1);
   bool isProcedural = op->getParentOp()->hasTrait<ProceduralRegion>();
   bool emitAsImmediate = !isTemporal && isProcedural;
@@ -4628,6 +4682,69 @@ LogicalResult StmtEmitter::visitVerif(verif::CoverOp op) {
   return emitVerifAssertLike(op, op.getProperty(), PPExtString("cover"));
 }
 
+/// Emit an assert-like operation from the `verif` dialect. This covers
+/// `verif.clocked_assert`, `verif.clocked_assume`, and `verif.clocked_cover`.
+LogicalResult StmtEmitter::emitVerifClockedAssertLike(
+    Operation *op, Value property, Value disable, Value clock,
+    verif::ClockEdge edge, PPExtString opName) {
+  if (hasSVAttributes(op))
+    emitError(op, "SV attributes emission is unimplemented for the op");
+
+  // If we are inside a procedural region we have the option of emitting either
+  // an `assert` or `assert property`. If we are in a non-procedural region,
+  // e.g., the body of a module, we have to use the concurrent form `assert
+  // property` (which also supports plain booleans).
+  //
+  // See IEEE 1800-2017 section 16.14.5 "Using concurrent assertion statements
+  // outside procedural code" and 16.14.6 "Embedding concurrent assertions in
+  // procedural code".
+  bool isTemporal = !property.getType().isSignlessInteger(1);
+  bool isProcedural = op->getParentOp()->hasTrait<ProceduralRegion>();
+  bool emitAsImmediate = !isTemporal && isProcedural;
+
+  startStatement();
+  SmallPtrSet<Operation *, 8> ops;
+  ops.insert(op);
+  ps.addCallback({op, true});
+  ps.scopedBox(PP::ibox2, [&]() {
+    emitAssertionLabel(op);
+    ps.scopedBox(PP::cbox0, [&]() {
+      if (emitAsImmediate)
+        ps << opName << "(";
+      else
+        ps << opName << PP::nbsp << "property" << PP::nbsp << "(";
+      ps.scopedBox(PP::ibox2, [&]() {
+        PropertyEmitter(emitter, ops)
+            .emitClockedProperty(property, clock, verifToltlClockEdge(edge),
+                                 disable);
+        ps << ");";
+      });
+    });
+  });
+  ps.addCallback({op, false});
+  emitLocationInfoAndNewLine(ops);
+  return success();
+}
+
+// FIXME: emit property assertion wrapped in a clock and disabled
+LogicalResult StmtEmitter::visitVerif(verif::ClockedAssertOp op) {
+  return emitVerifClockedAssertLike(op, op.getProperty(), op.getDisable(),
+                                    op.getClock(), op.getEdge(),
+                                    PPExtString("assert"));
+}
+
+LogicalResult StmtEmitter::visitVerif(verif::ClockedAssumeOp op) {
+  return emitVerifClockedAssertLike(op, op.getProperty(), op.getDisable(),
+                                    op.getClock(), op.getEdge(),
+                                    PPExtString("assume"));
+}
+
+LogicalResult StmtEmitter::visitVerif(verif::ClockedCoverOp op) {
+  return emitVerifClockedAssertLike(op, op.getProperty(), op.getDisable(),
+                                    op.getClock(), op.getEdge(),
+                                    PPExtString("cover"));
+}
+
 LogicalResult StmtEmitter::emitIfDef(Operation *op, MacroIdentAttr cond) {
   if (hasSVAttributes(op))
     emitError(op, "SV attributes emission is unimplemented for the op");

lib/Dialect/Verif/VerifDialect.cpp

@@ -32,3 +32,4 @@ Operation *VerifDialect::materializeConstant(OpBuilder &builder,
 }
 
 #include "circt/Dialect/Verif/VerifDialect.cpp.inc"
+#include "circt/Dialect/Verif/VerifEnums.cpp.inc"

lib/Dialect/Verif/VerifOps.cpp

@@ -7,6 +7,7 @@
 //===----------------------------------------------------------------------===//
 
 #include "circt/Dialect/Verif/VerifOps.h"
+#include "circt/Dialect/LTL/LTLOps.h"
 #include "circt/Dialect/LTL/LTLTypes.h"
 #include "circt/Support/CustomDirectiveImpl.h"
 #include "circt/Support/FoldUtils.h"
@@ -16,6 +17,9 @@
 #include "mlir/IR/SymbolTable.h"
 #include "mlir/Interfaces/FunctionImplementation.h"
 #include "mlir/Interfaces/SideEffectInterfaces.h"
+#include "llvm/ADT/MapVector.h"
+#include "llvm/ADT/TypeSwitch.h"
+#include "llvm/Support/raw_ostream.h"
 
 using namespace circt;
 using namespace verif;
@@ -56,6 +60,80 @@ LogicalResult LogicEquivalenceCheckingOp::verifyRegions() {
   return success();
 }
 
+//===----------------------------------------------------------------------===//
+// ClockedAssertLikeOps
+//===----------------------------------------------------------------------===//
+
+namespace {
+// Verify function for clocked assert / assume / cover ops.
+// This checks that they do not contiain any nested clocks or disable operations
+// Clocked assertlike ops are a simple form of assertions that only
+// contain one clock and one disable condition.
+struct ClockedAssertLikeOp {
+  static LogicalResult verify(Operation *clockedAssertLikeOp) {
+    // Used to perform a DFS search through the module to visit all operands
+    // before they are used
+    llvm::SmallMapVector<Operation *, OperandRange::iterator, 16> worklist;
+
+    // Keeps track of operations that have been visited
+    llvm::DenseSet<Operation *> handledOps;
+
+    Operation *property = clockedAssertLikeOp->getOperand(0).getDefiningOp();
+
+    // Fill in our worklist
+    worklist.insert({property, property->operand_begin()});
+
+    // Process the elements in our worklist
+    while (!worklist.empty()) {
+      auto &[op, operandIt] = worklist.back();
+
+      if (operandIt == op->operand_end()) {
+        // Check that our property doesn't contain any illegal ops
+        if (isa<ltl::ClockOp, ltl::DisableOp>(op)) {
+          op->emitError("Nested clock or disable operations are not "
+                        "allowed for clock_assertlike operations.");
+          return failure();
+        }
+
+        // Record that our op has been visited
+        handledOps.insert(op);
+        worklist.pop_back();
+        continue;
+      }
+
+      // Send the operands of our op to the worklist in case they are still
+      // un-visited
+      Value operand = *(operandIt++);
+      auto *defOp = operand.getDefiningOp();
+
+      // Make sure that we don't visit the same operand twice
+      if (!defOp || handledOps.contains(defOp))
+        continue;
+
+      // This is triggered if our operand is already in the worklist and
+      // wasn't handled
+      if (!worklist.insert({defOp, defOp->operand_begin()}).second) {
+        op->emitError("dependency cycle");
+        return failure();
+      }
+    }
+    return success();
+  }
+};
+} // namespace
+
+LogicalResult ClockedAssertOp::verify() {
+  return ClockedAssertLikeOp::verify(getOperation());
+}
+
+LogicalResult ClockedAssumeOp::verify() {
+  return ClockedAssertLikeOp::verify(getOperation());
+}
+
+LogicalResult ClockedCoverOp::verify() {
+  return ClockedAssertLikeOp::verify(getOperation());
+}
+
 //===----------------------------------------------------------------------===//
 // Generated code
 //===----------------------------------------------------------------------===//