diff --git a/include/circt/Dialect/FIRRTL/FIRRTLExpressions.td b/include/circt/Dialect/FIRRTL/FIRRTLExpressions.td index 3e73bfb90363..f69fd6df3584 100644 --- a/include/circt/Dialect/FIRRTL/FIRRTLExpressions.td +++ b/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:$length); + ConfinedAttr]>:$delay, + OptionalAttr]>>:$length); let assemblyFormat = [{ $input `,` $delay (`,` $length^)? attr-dict `:` functional-type(operands, results) diff --git a/include/circt/Dialect/LTL/LTLOps.td b/include/circt/Dialect/LTL/LTLOps.td index 1a8c3389a68b..2a40a7bcd8f7 100644 --- a/include/circt/Dialect/LTL/LTLOps.td +++ b/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:$length); + ConfinedAttr]>:$delay, + OptionalAttr]>>:$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:$length); + ConfinedAttr]>:$delay, + OptionalAttr]>>:$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: diff --git a/test/Dialect/FIRRTL/ltl-errors.mlir b/test/Dialect/FIRRTL/ltl-errors.mlir new file mode 100644 index 000000000000..4d82fec6f238 --- /dev/null +++ b/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> + } +} diff --git a/test/Dialect/LTL/errors.mlir b/test/Dialect/LTL/errors.mlir new file mode 100644 index 000000000000..dedfa4389c79 --- /dev/null +++ b/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