diff --git a/include/circt/Dialect/Verif/CMakeLists.txt b/include/circt/Dialect/Verif/CMakeLists.txt
index b95dc2e169bb..d0394870e4e4 100644
--- a/include/circt/Dialect/Verif/CMakeLists.txt
+++ b/include/circt/Dialect/Verif/CMakeLists.txt
@@ -1,2 +1,12 @@
 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)
+
+set(LLVM_TARGET_DEFINITIONS Passes.td)
+mlir_tablegen(Passes.h.inc -gen-pass-decls)
+add_public_tablegen_target(CIRCTVerifTransformsIncGen)
diff --git a/include/circt/Dialect/Verif/Passes.td b/include/circt/Dialect/Verif/Passes.td
new file mode 100644
index 000000000000..ae19032263ee
--- /dev/null
+++ b/include/circt/Dialect/Verif/Passes.td
@@ -0,0 +1,30 @@
+//===-- Passes.td - Verif pass definition file ----------------*- tablegen -*-===//
+//
+// Part of the LLVM Project, under the Apache License v2.0 with LLVM Exceptions.
+// See https://llvm.org/LICENSE.txt for license information.
+// SPDX-License-Identifier: Apache-2.0 WITH LLVM-exception
+//
+//===----------------------------------------------------------------------===//
+//
+// This file defines the passes that work on the Verif dialect.
+//
+//===----------------------------------------------------------------------===//
+
+#ifndef CIRCT_DIALECT_VERIF_PASSES_TD
+#define CIRCT_DIALECT_VERIF_PASSES_TD
+
+include "mlir/Pass/PassBase.td"
+
+/**
+ * Checks the validity of clocked assertions, assumptions, and cover ops.
+ */
+def VerifyClockedAssertLike : Pass<"verify-clocked-assert-like", "hw::HWModuleOp"> {
+  let summary = "Check that clocked-assert-like are valid.";
+  let description = [{
+    Checks that every `clocked_assert`, `clocked_assume` or `clocked_cover` op does not contain 
+    a nested `ltl.clock` or `ltl.disable` operation in its operand tree.
+  }];
+  let constructor = "circt::verif::createVerifyClockedAssertLikePass()";
+}
+
+#endif // CIRCT_DIALECT_VERIF_PASSES_TD
diff --git a/include/circt/Dialect/Verif/Verif.td b/include/circt/Dialect/Verif/Verif.td
index 30fae85b0ab5..389eb4069fb7 100644
--- a/include/circt/Dialect/Verif/Verif.td
+++ b/include/circt/Dialect/Verif/Verif.td
@@ -10,6 +10,7 @@
 #define CIRCT_DIALECT_VERIF_VERIF_TD
 
 include "circt/Dialect/Verif/VerifDialect.td"
+include "circt/Dialect/Verif/Passes.td"
 include "circt/Dialect/Verif/VerifOps.td"
 
 #endif // CIRCT_DIALECT_VERIF_VERIF_TD
diff --git a/include/circt/Dialect/Verif/VerifDialect.h b/include/circt/Dialect/Verif/VerifDialect.h
index 99735e84519a..40f54348aa9e 100644
--- a/include/circt/Dialect/Verif/VerifDialect.h
+++ b/include/circt/Dialect/Verif/VerifDialect.h
@@ -13,6 +13,8 @@
 #include "mlir/IR/BuiltinOps.h"
 #include "mlir/IR/Dialect.h"
 
+#include "circt/Dialect/Verif/Passes.h.inc"
 #include "circt/Dialect/Verif/VerifDialect.h.inc"
+#include "circt/Dialect/Verif/VerifEnums.h.inc"
 
 #endif // CIRCT_DIALECT_VERIF_VERIFDIALECT_H
diff --git a/include/circt/Dialect/Verif/VerifOps.td b/include/circt/Dialect/Verif/VerifOps.td
index ce803339162b..fd101e964b6d 100644
--- a/include/circt/Dialect/Verif/VerifOps.td
+++ b/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,56 @@ 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)
+  }];
+}
+
+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
 //===----------------------------------------------------------------------===//
diff --git a/include/circt/Dialect/Verif/VerifPasses.h b/include/circt/Dialect/Verif/VerifPasses.h
new file mode 100644
index 000000000000..f68077a6c758
--- /dev/null
+++ b/include/circt/Dialect/Verif/VerifPasses.h
@@ -0,0 +1,34 @@
+
+//===- Passes.h - Verif pass entry points ------------------------*- C++-*-===//
+//
+// Part of the LLVM Project, under the Apache License v2.0 with LLVM Exceptions.
+// See https://llvm.org/LICENSE.txt for license information.
+// SPDX-License-Identifier: Apache-2.0 WITH LLVM-exception
+//
+//===----------------------------------------------------------------------===//
+//
+// This header file defines prototypes that expose pass constructors.
+//
+//===----------------------------------------------------------------------===//
+
+#ifndef CIRCT_DIALECT_VERIF_VERIFPASSES_H
+#define CIRCT_DIALECT_VERIF_VERIFPASSES_H
+
+#include "circt/Dialect/HW/HWOps.h"
+#include "mlir/Pass/Pass.h"
+#include "mlir/Pass/PassRegistry.h"
+#include <memory>
+#include <optional>
+
+namespace circt {
+namespace verif {
+
+std::unique_ptr<mlir::Pass> createVerifyClockedAssertLikePass();
+
+#define GEN_PASS_REGISTRATION
+#include "circt/Dialect/Verif/Passes.h.inc"
+
+} // namespace verif
+} // namespace circt
+
+#endif // CIRCT_DIALECT_VERIF_VERIFPASSES_H
diff --git a/include/circt/Dialect/Verif/VerifVisitors.h b/include/circt/Dialect/Verif/VerifVisitors.h
index 7ef700c8fff3..77b098b2b9ae 100644
--- a/include/circt/Dialect/Verif/VerifVisitors.h
+++ b/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...);
         });
@@ -50,6 +52,9 @@ class Visitor {
   HANDLE(AssertOp, Unhandled);
   HANDLE(AssumeOp, Unhandled);
   HANDLE(CoverOp, Unhandled);
+  HANDLE(ClockedAssertOp, Unhandled);
+  HANDLE(ClockedAssumeOp, Unhandled);
+  HANDLE(ClockedCoverOp, Unhandled);
 #undef HANDLE
 };
 
diff --git a/include/circt/InitAllPasses.h b/include/circt/InitAllPasses.h
index 231a8c05fd9e..3e65635c5e0c 100644
--- a/include/circt/InitAllPasses.h
+++ b/include/circt/InitAllPasses.h
@@ -34,6 +34,7 @@
 #include "circt/Dialect/SV/SVPasses.h"
 #include "circt/Dialect/Seq/SeqPasses.h"
 #include "circt/Dialect/SystemC/SystemCPasses.h"
+#include "circt/Dialect/Verif/VerifPasses.h"
 #include "circt/Tools/circt-lec/Passes.h"
 #include "circt/Transforms/Passes.h"
 
@@ -68,6 +69,7 @@ inline void registerAllPasses() {
   pipeline::registerPasses();
   ssp::registerPasses();
   systemc::registerPasses();
+  verif::registerPasses();
 }
 
 } // namespace circt
diff --git a/lib/Conversion/ExportVerilog/ExportVerilog.cpp b/lib/Conversion/ExportVerilog/ExportVerilog.cpp
index 2f39d39de8b2..146d63c2adec 100644
--- a/lib/Conversion/ExportVerilog/ExportVerilog.cpp
+++ b/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>;
@@ -3452,6 +3471,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
@@ -3876,6 +3924,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;
 
@@ -4665,6 +4721,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");
diff --git a/lib/Dialect/Verif/CMakeLists.txt b/lib/Dialect/Verif/CMakeLists.txt
index c23d6831756c..a9061cdf23aa 100644
--- a/lib/Dialect/Verif/CMakeLists.txt
+++ b/lib/Dialect/Verif/CMakeLists.txt
@@ -12,6 +12,10 @@ add_circt_dialect_library(CIRCTVerif
   Support
 
   LINK_LIBS PUBLIC
+  CIRCTHW
   CIRCTLTL
   MLIRIR
+  MLIRTransforms
 )
+
+add_subdirectory(Transforms)
diff --git a/lib/Dialect/Verif/Transforms/CMakeLists.txt b/lib/Dialect/Verif/Transforms/CMakeLists.txt
new file mode 100644
index 000000000000..fa1b9b5be106
--- /dev/null
+++ b/lib/Dialect/Verif/Transforms/CMakeLists.txt
@@ -0,0 +1,16 @@
+add_circt_dialect_library(CIRCTVerifTransforms
+  VerifyClockedAssertLike.cpp
+
+  DEPENDS
+  CIRCTVerifTransformsIncGen
+
+  LINK_LIBS PUBLIC
+  CIRCTVerif
+  CIRCTLTL
+  CIRCTHW
+  CIRCTSupport
+  MLIRIR
+  MLIRPass
+  MLIRTransforms
+  MLIRTransformUtils
+)
diff --git a/lib/Dialect/Verif/Transforms/PassDetails.h b/lib/Dialect/Verif/Transforms/PassDetails.h
new file mode 100644
index 000000000000..b8438a506958
--- /dev/null
+++ b/lib/Dialect/Verif/Transforms/PassDetails.h
@@ -0,0 +1,32 @@
+//===- PassDetails.h - Verif pass class details -----------------*- C++ -*-===//
+//
+// Part of the LLVM Project, under the Apache License v2.0 with LLVM Exceptions.
+// See https://llvm.org/LICENSE.txt for license information.
+// SPDX-License-Identifier: Apache-2.0 WITH LLVM-exception
+//
+//===----------------------------------------------------------------------===//
+//
+// Stuff shared between the different Verif passes.
+//
+//===----------------------------------------------------------------------===//
+
+// clang-tidy seems to expect the absolute path in the header guard on some
+// systems, so just disable it.
+// NOLINTNEXTLINE(llvm-header-guard)
+#ifndef DIALECT_VERIF_TRANSFORMS_PASSDETAILS_H
+#define DIALECT_VERIF_TRANSFORMS_PASSDETAILS_H
+
+#include "circt/Dialect/Verif/VerifOps.h"
+#include "circt/Dialect/Verif/VerifPasses.h"
+#include "mlir/Pass/Pass.h"
+
+namespace circt {
+namespace verif {
+
+#define GEN_PASS_CLASSES
+#include "circt/Dialect/Verif/Passes.h.inc"
+
+} // namespace verif
+} // namespace circt
+
+#endif // DIALECT_FSM_TRANSFORMS_PASSDETAILS_H
diff --git a/lib/Dialect/Verif/Transforms/VerifyClockedAssertLike.cpp b/lib/Dialect/Verif/Transforms/VerifyClockedAssertLike.cpp
new file mode 100644
index 000000000000..c1cbfd925edf
--- /dev/null
+++ b/lib/Dialect/Verif/Transforms/VerifyClockedAssertLike.cpp
@@ -0,0 +1,108 @@
+//===- VerifyClockedAssertLike.cpp - Check Clocked Asserts -------*- C++-*-===//
+//
+// Part of the LLVM Project, under the Apache License v2.0 with LLVM Exceptions.
+// See https://llvm.org/LICENSE.txt for license information.
+// SPDX-License-Identifier: Apache-2.0 WITH LLVM-exception
+//===----------------------------------------------------------------------===//
+//
+// Checks that clocked assert-like ops are constructed correctly.
+//
+//===----------------------------------------------------------------------===//
+
+#include "PassDetails.h"
+#include "circt/Dialect/HW/HWAttributes.h"
+#include "circt/Dialect/HW/HWModuleGraph.h"
+#include "circt/Dialect/HW/HWOps.h"
+#include "circt/Dialect/HW/HWPasses.h"
+#include "circt/Dialect/HW/HWTypes.h"
+#include "circt/Dialect/LTL/LTLOps.h"
+#include "circt/Dialect/LTL/LTLTypes.h"
+#include "circt/Dialect/Verif/VerifDialect.h"
+#include "circt/Dialect/Verif/VerifOps.h"
+#include "circt/Dialect/Verif/VerifPasses.h"
+#include "mlir/Pass/Pass.h"
+#include "llvm/ADT/TypeSwitch.h"
+
+using namespace circt;
+using namespace verif;
+
+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 VerifyClockedAssertLikePass
+    : VerifyClockedAssertLikeBase<VerifyClockedAssertLikePass> {
+private:
+  // 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;
+
+public:
+  void runOnOperation() override;
+
+private:
+  void verify(Operation *clockedAssertLikeOp) {
+
+    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;
+        }
+
+        // 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;
+      }
+    }
+
+    // Clear worklist and such
+    worklist.clear();
+    handledOps.clear();
+  }
+};
+} // namespace
+
+void VerifyClockedAssertLikePass::runOnOperation() {
+  getOperation()->walk([&](Operation *op) {
+    llvm::TypeSwitch<Operation *, void>(op)
+        .Case<verif::ClockedAssertOp, verif::ClockedAssumeOp,
+              verif::ClockedCoverOp>([&](auto clockedOp) { verify(clockedOp); })
+        .Default([&](auto) {});
+  });
+}
+
+std::unique_ptr<mlir::Pass> circt::verif::createVerifyClockedAssertLikePass() {
+  return std::make_unique<VerifyClockedAssertLikePass>();
+}
diff --git a/lib/Dialect/Verif/VerifDialect.cpp b/lib/Dialect/Verif/VerifDialect.cpp
index 87cc21ff7c5d..7c8cab8c0703 100644
--- a/lib/Dialect/Verif/VerifDialect.cpp
+++ b/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"
diff --git a/lib/Dialect/Verif/VerifOps.cpp b/lib/Dialect/Verif/VerifOps.cpp
index 3c838415da79..e380bc081794 100644
--- a/lib/Dialect/Verif/VerifOps.cpp
+++ b/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,7 @@
 #include "mlir/IR/SymbolTable.h"
 #include "mlir/Interfaces/FunctionImplementation.h"
 #include "mlir/Interfaces/SideEffectInterfaces.h"
+#include "llvm/ADT/MapVector.h"
 
 using namespace circt;
 using namespace verif;
diff --git a/lib/Firtool/CMakeLists.txt b/lib/Firtool/CMakeLists.txt
index 6a311dd659e5..9441b95172cf 100644
--- a/lib/Firtool/CMakeLists.txt
+++ b/lib/Firtool/CMakeLists.txt
@@ -6,6 +6,7 @@ add_circt_library(CIRCTFirtool
   CIRCTExportVerilog
   CIRCTFIRRTLToHW
   CIRCTFIRRTLTransforms
+  CIRCTHWToBTOR2
   CIRCTHWTransforms
   CIRCTLTLToCore
   CIRCTOMTransforms
@@ -15,7 +16,7 @@ add_circt_library(CIRCTFirtool
   CIRCTSVTransforms
   CIRCTTransforms
   CIRCTVerifToSV
-  CIRCTHWToBTOR2
+  CIRCTVerifTransforms
 
   MLIRIR
   MLIRSupport
diff --git a/lib/Firtool/Firtool.cpp b/lib/Firtool/Firtool.cpp
index e5e79f138843..876cd1f43486 100644
--- a/lib/Firtool/Firtool.cpp
+++ b/lib/Firtool/Firtool.cpp
@@ -14,6 +14,7 @@
 #include "circt/Dialect/OM/OMPasses.h"
 #include "circt/Dialect/SV/SVPasses.h"
 #include "circt/Dialect/Seq/SeqPasses.h"
+#include "circt/Dialect/Verif/VerifPasses.h"
 #include "circt/Support/Passes.h"
 #include "circt/Transforms/Passes.h"
 #include "mlir/Transforms/Passes.h"
@@ -264,6 +265,9 @@ LogicalResult firtool::populateLowFIRRTLToHW(mlir::PassManager &pm,
   // Check OM object fields.
   pm.addPass(om::createVerifyObjectFieldsPass());
 
+  // Run the verif op verification pass
+  pm.addNestedPass<hw::HWModuleOp>(verif::createVerifyClockedAssertLikePass());
+
   return success();
 }
 
@@ -322,6 +326,9 @@ LogicalResult
 populatePrepareForExportVerilog(mlir::PassManager &pm,
                                 const firtool::FirtoolOptions &opt) {
 
+  // Run the verif op verification pass
+  pm.addNestedPass<hw::HWModuleOp>(verif::createVerifyClockedAssertLikePass());
+
   // Legalize unsupported operations within the modules.
   pm.nest<hw::HWModuleOp>().addPass(sv::createHWLegalizeModulesPass());
 
diff --git a/test/Conversion/ExportVerilog/verif.mlir b/test/Conversion/ExportVerilog/verif.mlir
index b35068592f24..be582e999ccf 100644
--- a/test/Conversion/ExportVerilog/verif.mlir
+++ b/test/Conversion/ExportVerilog/verif.mlir
@@ -298,3 +298,19 @@ hw.module @Issue5763(in %a: i3) {
   %2 = comb.and bin %1, %0 : i1
   verif.assert %2 : i1
 }
+
+
+// CHECK-LABEL: module ClockedAsserts
+hw.module @ClockedAsserts(in %clk: i1, in %a: i1, in %b: i1) {
+  %true = hw.constant true
+  %n0 = ltl.not %a : i1
+
+  // CHECK: assert property (@(posedge clk) disable iff (b) not a);
+  verif.clocked_assert %n0 disable %b clock posedge %clk : !ltl.property
+
+  // CHECK: assume property (@(posedge clk) disable iff (b) not a);
+  verif.clocked_assume %n0 disable %b clock posedge %clk : !ltl.property
+
+  // CHECK: cover property (@(posedge clk) disable iff (b) not a);
+  verif.clocked_cover %n0 disable %b clock posedge %clk : !ltl.property
+}
diff --git a/test/Dialect/Verif/verify.mlir b/test/Dialect/Verif/verify.mlir
new file mode 100644
index 000000000000..7344c1a8fb69
--- /dev/null
+++ b/test/Dialect/Verif/verify.mlir
@@ -0,0 +1,74 @@
+// RUN: circt-opt --verify-clocked-assert-like %s --split-input-file --verify-diagnostics | circt-opt
+
+hw.module @verifyDisables(in %clk: i1, in %a: i1, in %b: i1) {
+  %n0 = ltl.not %a : i1
+
+  // expected-error @below {{Nested clock or disable operations are not allowed for clock_assertlike operations.}}
+  %disabled0 = ltl.disable %n0 if %b : !ltl.property
+  verif.clocked_assert %disabled0 disable %b clock posedge %clk : !ltl.property
+}
+
+// -----
+
+hw.module @verifyDisables1(in %clk: i1, in %a: i1, in %b: i1) {
+  %n0 = ltl.not %a : i1
+
+  // expected-error @below {{Nested clock or disable operations are not allowed for clock_assertlike operations.}}
+  %disabled1 = ltl.disable %n0 if %b : !ltl.property
+  verif.clocked_assume %disabled1 disable %b clock posedge %clk : !ltl.property
+}
+
+// -----
+
+hw.module @verifyDisables2(in %clk: i1, in %a: i1, in %b: i1) {
+  %n0 = ltl.not %a : i1
+
+  // expected-error @below {{Nested clock or disable operations are not allowed for clock_assertlike operations.}}
+  %disabled2 = ltl.disable %n0 if %b : !ltl.property
+  verif.clocked_cover %disabled2 disable %b clock posedge %clk : !ltl.property
+}
+
+// -----
+
+hw.module @verifyClocks(in %clk: i1, in %a: i1, in %b: i1) {
+  %n0 = ltl.not %a : i1
+
+  // expected-error @below {{Nested clock or disable operations are not allowed for clock_assertlike operations.}}
+  %clocked = ltl.clock %n0, posedge %clk : !ltl.property
+  verif.clocked_assert %clocked disable %b clock posedge %clk : !ltl.property
+}
+
+// -----
+
+hw.module @verifyClocks1(in %clk: i1, in %a: i1, in %b: i1) {
+  %n0 = ltl.not %a : i1
+
+  // expected-error @below {{Nested clock or disable operations are not allowed for clock_assertlike operations.}}
+  %clocked = ltl.clock %n0, posedge %clk : !ltl.property
+  verif.clocked_assume %clocked disable %b clock posedge %clk : !ltl.property
+}
+
+// -----
+
+hw.module @verifyClocks2(in %clk: i1, in %a: i1, in %b: i1) {
+  %n0 = ltl.not %a : i1
+
+  // expected-error @below {{Nested clock or disable operations are not allowed for clock_assertlike operations.}}
+  %clocked = ltl.clock %n0, posedge %clk : !ltl.property
+  verif.clocked_cover %clocked disable %b clock posedge %clk : !ltl.property
+}
+
+// -----
+
+hw.module @deeplynested(in %clk: i1, in %a: i1, in %b: i1) {
+  %n0 = ltl.not %a : i1
+  // expected-error @below {{Nested clock or disable operations are not allowed for clock_assertlike operations.}}
+  %clocked = ltl.clock %n0, posedge %clk : !ltl.property
+
+  %e1 = ltl.eventually %clocked : !ltl.property
+  %i1 = ltl.implication %b, %e1 : i1, !ltl.property
+  %a1 = ltl.and %b, %i1 : i1, !ltl.property
+  %o1 = ltl.or %b, %a1 : i1, !ltl.property
+
+  verif.clocked_assert %o1 disable %b clock posedge %clk : !ltl.property
+}
\ No newline at end of file
diff --git a/tools/circt-opt/CMakeLists.txt b/tools/circt-opt/CMakeLists.txt
index de3435532e82..1dbf079ee29b 100644
--- a/tools/circt-opt/CMakeLists.txt
+++ b/tools/circt-opt/CMakeLists.txt
@@ -92,6 +92,7 @@ target_link_libraries(circt-opt
   CIRCTSystemCTransforms
   CIRCTTransforms
   CIRCTVerif
+  CIRCTVerifTransforms
   CIRCTVerifToSMT
   CIRCTVerifToSV
   CIRCTLTLToCore
diff --git a/tools/firtool/CMakeLists.txt b/tools/firtool/CMakeLists.txt
index 37fb822eb18c..6d1650537aee 100644
--- a/tools/firtool/CMakeLists.txt
+++ b/tools/firtool/CMakeLists.txt
@@ -15,6 +15,8 @@ target_link_libraries(firtool PRIVATE
   CIRCTFIRRTLTransforms
   CIRCTHWTransforms
   CIRCTOMTransforms
+  CIRCTVerifTransforms
+  CIRCTVerif
   CIRCTSeq
   CIRCTSim
   CIRCTSVTransforms
diff --git a/tools/firtool/firtool.cpp b/tools/firtool/firtool.cpp
index da247a926ab5..f92f25635a7b 100644
--- a/tools/firtool/firtool.cpp
+++ b/tools/firtool/firtool.cpp
@@ -34,6 +34,7 @@
 #include "circt/Dialect/Seq/SeqDialect.h"
 #include "circt/Dialect/Sim/SimDialect.h"
 #include "circt/Dialect/Verif/VerifDialect.h"
+#include "circt/Dialect/Verif/VerifPasses.h"
 #include "circt/Support/LoweringOptions.h"
 #include "circt/Support/LoweringOptionsParser.h"
 #include "circt/Support/Passes.h"
@@ -711,6 +712,7 @@ int main(int argc, char **argv) {
     om::registerPasses();
     sv::registerPasses();
     hw::registerFlattenModulesPass();
+    verif::registerVerifyClockedAssertLikePass();
 
     // Export passes:
     registerExportChiselInterfacePass();