[ExportVerilog] Enforce ltl.delay clock/edge match enclosing ltl.clock

Add validation so ltl.delay's clock and edge must match the enclosing ltl.clock,
as SVA only supports a single clock context for delays. Emit errors for mismatches. Placeholder clocks (hw.constant true) are allowed and inherit the outer clock.

Author: Clo91eaf

lib/Conversion/ExportVerilog/ExportVerilog.cpp

@@ -2304,8 +2304,7 @@ class ExprEmitter : public EmitterBase,
 
   /// Emit braced list of values surrounded by `{` and `}`.
   void emitBracedList(ValueRange ops) {
-    return emitBracedList(
-        ops, [&]() { ps << "{"; }, [&]() { ps << "}"; });
+    return emitBracedList(ops, [&]() { ps << "{"; }, [&]() { ps << "}"; });
   }
 
   /// Print an APInt constant.
@@ -3603,6 +3602,12 @@ class PropertyEmitter : public EmitterBase,
   /// location information tracking.
   SmallPtrSetImpl<Operation *> &emittedOps;
 
+  /// Current clock context from enclosing ltl.clock op. Used to verify that
+  /// ltl.delay ops have consistent clocks, since SVA does not support
+  /// per-delay clocks.
+  Value currentClock;
+  std::optional<ltl::ClockEdge> currentEdge;
+
   /// Tokens buffered for inserting casts/parens after emitting children.
   SmallVector<Token> localTokens;
 
@@ -3752,6 +3757,26 @@ EmittedProperty PropertyEmitter::visitLTL(ltl::IntersectOp op) {
 }
 
 EmittedProperty PropertyEmitter::visitLTL(ltl::DelayOp op) {
+  // Verify that the delay's clock matches the enclosing clock context.
+  // SVA does not support per-delay clocks; all delays inherit from the
+  // enclosing @(edge clock) specification.
+  Value delayClock = op.getClock();
+  if (currentClock) {
+    // Check if delay has a real clock (not a placeholder constant)
+    bool isPlaceholder = false;
+    if (auto constOp = delayClock.getDefiningOp<hw::ConstantOp>()) {
+      auto value = constOp.getValue();
+      isPlaceholder = value.getBitWidth() == 1 && value.isOne();
+    }
+
+    if (!isPlaceholder && delayClock != currentClock) {
+      emitOpError(op, "delay clock does not match enclosing clock; "
+                      "SVA does not support per-delay clocks");
+    } else if (!isPlaceholder && currentEdge && op.getEdge() != *currentEdge) {
+      emitOpError(op, "delay clock edge does not match enclosing clock edge");
+    }
+  }
+
   ps << "##";
   if (auto length = op.getLength()) {
     if (*length == 0) {
@@ -3907,7 +3932,18 @@ EmittedProperty PropertyEmitter::visitLTL(ltl::ClockOp op) {
     ps << ")";
   });
   ps << PP::space;
+
+  // Set the clock context for nested property emission.
+  // Save and restore to handle nested clock ops correctly.
+  Value savedClock = currentClock;
+  auto savedEdge = currentEdge;
+  currentClock = op.getClock();
+  currentEdge = op.getEdge();
+
   emitNestedProperty(op.getInput(), PropertyPrecedence::Clocking);
+
+  currentClock = savedClock;
+  currentEdge = savedEdge;
   return {PropertyPrecedence::Clocking};
 }