[LTL][FIRRTL] Require non-negative LTL delay bounds

include/circt/Dialect/FIRRTL/FIRRTLExpressions.td

@@ -20,6 +20,7 @@ include "circt/Dialect/HW/HWAttributesNaming.td"
 include "circt/Dialect/HW/HWOpInterfaces.td"
 include "circt/Dialect/HW/HWTypes.td"
 include "circt/Types.td"
+include "mlir/IR/CommonAttrConstraints.td"
 include "mlir/Interfaces/InferTypeOpInterface.td"
 include "mlir/Interfaces/SideEffectInterfaces.td"
 
@@ -1775,8 +1776,8 @@ def LTLIntersectIntrinsicOp : BinaryLTLIntrinsicOp<"intersect", [Commutative]>;
 // Sequences
 def LTLDelayIntrinsicOp : LTLIntrinsicOp<"delay"> {
   let arguments = (ins NonConstUInt1Type:$input,
-                       I64Attr:$delay,
-                       OptionalAttr<I64Attr>:$length);
+                       ConfinedAttr<I64Attr, [IntMinValue<0>]>:$delay,
+                       OptionalAttr<ConfinedAttr<I64Attr, [IntMinValue<0>]>>:$length);
   let assemblyFormat = [{
     $input `,` $delay (`,` $length^)? attr-dict `:`
     functional-type(operands, results)

include/circt/Dialect/LTL/LTLOps.td

@@ -12,6 +12,7 @@
 include "circt/Dialect/HW/HWTypes.td"
 include "circt/Dialect/LTL/LTLDialect.td"
 include "circt/Dialect/LTL/LTLTypes.td"
+include "mlir/IR/CommonAttrConstraints.td"
 include "mlir/IR/EnumAttr.td"
 include "mlir/IR/PatternBase.td"
 include "mlir/Interfaces/InferTypeOpInterface.td"
@@ -110,8 +111,8 @@ def ClockOp : LTLOp<"clock", [
 def DelayOp : LTLOp<"delay", [Pure]> {
   let arguments = (ins
     LTLAnySequenceType:$input,
-    I64Attr:$delay,
-    OptionalAttr<I64Attr>:$length);
+    ConfinedAttr<I64Attr, [IntMinValue<0>]>:$delay,
+    OptionalAttr<ConfinedAttr<I64Attr, [IntMinValue<0>]>>:$length);
   let results = (outs LTLSequenceType:$result);
   let assemblyFormat = [{
     $input `,` $delay (`,` $length^)? attr-dict `:` type($input)
@@ -152,8 +153,8 @@ def ClockedDelayOp : LTLOp<"clocked_delay", [Pure]> {
     LTLAnySequenceType:$input,
     ClockEdgeAttr:$edge,
     I1:$clock,
-    I64Attr:$delay,
-    OptionalAttr<I64Attr>:$length);
+    ConfinedAttr<I64Attr, [IntMinValue<0>]>:$delay,
+    OptionalAttr<ConfinedAttr<I64Attr, [IntMinValue<0>]>>:$length);
   let results = (outs LTLSequenceType:$result);
   let assemblyFormat = [{
     $input `,` $edge $clock `,` $delay (`,` $length^)? attr-dict `:` type($input)
@@ -167,7 +168,8 @@ def ClockedDelayOp : LTLOp<"clocked_delay", [Pure]> {
     on the specified `$clock` and `$edge`.
 
     The optional `$length` specifies during how many cycles after the initial
-    delay the sequence can match. Omitting `$length` indicates an unbounded but
+    delay the sequence can match. The delay and length, when present, must be
+    greater than or equal to zero. Omitting `$length` indicates an unbounded but
     finite delay.
 
     For example:

test/Dialect/FIRRTL/ltl-errors.mlir

@@ -0,0 +1,17 @@
+// RUN: circt-opt %s --split-input-file --verify-diagnostics
+
+firrtl.circuit "Test" {
+  firrtl.module @Test(in %a : !firrtl.uint<1>) {
+    // expected-error @+1 {{attribute 'delay' failed to satisfy constraint}}
+    %0 = firrtl.int.ltl.delay %a, -1 : (!firrtl.uint<1>) -> !firrtl.uint<1>
+  }
+}
+
+// -----
+
+firrtl.circuit "Test" {
+  firrtl.module @Test(in %a : !firrtl.uint<1>) {
+    // expected-error @+1 {{attribute 'length' failed to satisfy constraint}}
+    %0 = firrtl.int.ltl.delay %a, 1, -1 : (!firrtl.uint<1>) -> !firrtl.uint<1>
+  }
+}

test/Dialect/LTL/errors.mlir

@@ -0,0 +1,29 @@
+// RUN: circt-opt %s --split-input-file --verify-diagnostics
+
+%s = unrealized_conversion_cast to !ltl.sequence
+
+// expected-error @+1 {{attribute 'delay' failed to satisfy constraint}}
+ltl.delay %s, -1 : !ltl.sequence
+
+// -----
+
+%s = unrealized_conversion_cast to !ltl.sequence
+
+// expected-error @+1 {{attribute 'length' failed to satisfy constraint}}
+ltl.delay %s, 1, -1 : !ltl.sequence
+
+// -----
+
+%s = unrealized_conversion_cast to !ltl.sequence
+%clk = hw.constant true
+
+// expected-error @+1 {{attribute 'delay' failed to satisfy constraint}}
+ltl.clocked_delay %s, posedge %clk, -1 : !ltl.sequence
+
+// -----
+
+%s = unrealized_conversion_cast to !ltl.sequence
+%clk = hw.constant true
+
+// expected-error @+1 {{attribute 'length' failed to satisfy constraint}}
+ltl.clocked_delay %s, posedge %clk, 1, -1 : !ltl.sequence