diff --git a/include/circt/Dialect/LTL/LTLOps.td b/include/circt/Dialect/LTL/LTLOps.td index e51a0a66a2dc..86b22c707454 100644 --- a/include/circt/Dialect/LTL/LTLOps.td +++ b/include/circt/Dialect/LTL/LTLOps.td @@ -61,10 +61,159 @@ def IntersectOp : AssocLTLOp<"intersect"> { let hasCanonicalizeMethod = 1; } +//===----------------------------------------------------------------------===// +// Clocking +//===----------------------------------------------------------------------===// + +// 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::ltl"; +} + +def ClockOp : LTLOp<"clock", [Pure, InferTypeOpInterface, + DeclareOpInterfaceMethods]> { + let arguments = (ins + LTLAnyPropertyType:$input, + ClockEdgeAttr:$edge, + I1:$clock); + let results = (outs LTLSequenceOrPropertyType:$result); + let assemblyFormat = [{ + $input `,` $edge $clock attr-dict `:` type($input) + }]; + + let summary = "Specify the clock for a property or sequence."; + let description = [{ + Specifies the `$edge` on a given `$clock` to be the clock for an `$input` + property or sequence. All cycle delays in the `$input` implicitly refer to a + clock that advances the state to the next cycle. The `ltl.clock` operation + provides that clock. The clock applies to the entire property or sequence + expression tree below `$input`, up to any other nested `ltl.clock` + operations. + + The operation returns a property if the `$input` is a property, and a + sequence otherwise. + }]; +} + //===----------------------------------------------------------------------===// // Sequences //===----------------------------------------------------------------------===// +def CreateClockedSequenceOp : LTLOp<"create_clocked_sequence", [Pure]> { + let arguments = (ins + LTLAnySequenceType:$input, + ClockEdgeAttr:$edge, + I1:$clock); + let results = (outs LTLClockedSequenceType:$result); + let assemblyFormat = [{ + $input `,` $edge $clock attr-dict `:` type($input) + }]; + + let summary = "Create an explicitly clocked sequence from input " + "sequences/booleans."; + let description = [{ + Creates an explicitly clocked sequence by binding a single input sequence + or boolean value to a specific clock edge. This operation is fundamental to + the explicit clocking model, ensuring that all temporal operations have + well-defined clock semantics. + }]; +} + +def ClockedAndOp : LTLOp<"clocked_and", [Pure, Commutative]> { + let arguments = (ins + Variadic:$inputs, + ClockEdgeAttr:$edge, + I1:$clock); + let results = (outs LTLClockedSequenceType:$result); + let assemblyFormat = [{ + $edge $clock `,` $inputs attr-dict + }]; + let hasCanonicalizeMethod = 1; + + let summary = "A conjunction of explicitly clocked sequences with a specified clock domain."; + let description = [{ + See `ltl.and` op. $edge and $clock specify the clock domain for the result. + }]; +} + +def ClockedOrOp : LTLOp<"clocked_or", [Pure, Commutative]> { + let arguments = (ins + Variadic:$inputs, + ClockEdgeAttr:$edge, + I1:$clock); + let results = (outs LTLClockedSequenceType:$result); + let assemblyFormat = [{ + $edge $clock `,` $inputs attr-dict + }]; + let hasCanonicalizeMethod = 1; + + let summary = "A disjunction of explicitly clocked sequences with a specified clock domain."; + let description = [{ + See `ltl.or` op. $edge and $clock specify the clock domain for the result. + }]; +} + +def ClockedIntersectOp : LTLOp<"clocked_intersect", [Pure, Commutative]> { + let arguments = (ins + Variadic:$inputs, + ClockEdgeAttr:$edge, + I1:$clock); + let results = (outs LTLClockedSequenceType:$result); + let assemblyFormat = [{ + $edge $clock `,` $inputs attr-dict + }]; + let hasCanonicalizeMethod = 1; + + let summary = "Intersection of explicitly clocked sequences with a specified clock domain."; + let description = [{ + See `ltl.intersect` op. $edge and $clock specify the clock domain for the result. + }]; +} + +def ClockedDelayOp : LTLOp<"clocked_delay", [Pure]> { + let arguments = (ins + LTLAnySequenceType:$input, + ClockEdgeAttr:$edge, + I1:$clock, + I64Attr:$delay, + OptionalAttr:$length); + let results = (outs LTLClockedSequenceType:$result); + let assemblyFormat = [{ + $edge $clock `,` $input `,` $delay (`,` $length^)? attr-dict `:` type($input) + }]; + + let summary = "Create an explicitly clocked delay sequence from i1 or sequence."; + let description = [{ + Creates a standalone "pure delay" sequence that is explicitly bound to a + specific clock. This sequence evaluates to true immediately and matches + after the specified number of clock ticks. + + The `$input` must be an explicitly clocked sequence. The `$delay` specifies + the number of clock cycles to delay, and the optional `$length` specifies + the range of cycles during which the delay can match. Omitting `$length` + indicates an unbounded but finite delay. + + Examples: + - `ltl.clocked_delay posedge %clk, %seq, 2, 0` creates a delay that matches + exactly 2 cycles after the current time on the positive edge of %clk. + - `ltl.clocked_delay posedge %clk, %seq, 2, 2` creates a delay that matches + 2, 3, or 4 cycles after the current time. + - `ltl.clocked_delay posedge %clk, %seq, 2` creates an unbounded but finite + delay of 2 or more cycles. + + This operation enables clean lowering of SVA expressions like `##1 b` + }]; +} + def DelayOp : LTLOp<"delay", [Pure]> { let arguments = (ins LTLAnySequenceType:$input, @@ -119,6 +268,24 @@ def PastOp : LTLOp<"past", [Pure]> { }]; } +def ClockedConcatOp : LTLOp<"clocked_concat", [Pure]> { + let arguments = (ins + Variadic:$inputs, + ClockEdgeAttr:$edge, + I1:$clock); + let results = (outs LTLClockedSequenceType:$result); + let assemblyFormat = [{ + $edge $clock `,` $inputs attr-dict + }]; + let hasFolder = 1; + let hasCanonicalizer = 1; + + let summary = "Concatenate explicitly clocked sequences with a specified clock domain."; + let description = [{ + See `ltl.concat` op. $edge and $clock specify the clock domain for the result. + }]; +} + def ConcatOp : LTLOp<"concat", [Pure]> { let arguments = (ins Variadic:$inputs); let results = (outs LTLSequenceType:$result); @@ -178,6 +345,24 @@ def ConcatOp : LTLOp<"concat", [Pure]> { }]; } +def ClockedRepeatOp : LTLOp<"clocked_repeat", [Pure]> { + let arguments = (ins + LTLClockedSequenceType:$input, + I64Attr:$base, + OptionalAttr:$more); + let results = (outs LTLClockedSequenceType:$result); + let assemblyFormat = [{ + $input `,` $base (`,` $more^)? attr-dict + }]; + let hasFolder = 1; + + let summary = "Repeats a clocked sequence by a number of times."; + let description = [{ + See `ltl.repeat` op. The `$input` must be an explicitly clocked sequence. + The result is also an explicitly clocked sequence with the same clock domain of `$input`. + }]; +} + def RepeatOp : LTLOp<"repeat", [Pure]> { let arguments = (ins LTLAnySequenceType:$input, @@ -203,6 +388,25 @@ def RepeatOp : LTLOp<"repeat", [Pure]> { }]; } +def ClockedGoToRepeatOp : LTLOp<"clocked_goto_repeat", [Pure]> { + let arguments = (ins + LTLClockedSequenceType:$input, + I64Attr:$base, + I64Attr:$more); + let results = (outs LTLClockedSequenceType:$result); + let assemblyFormat = [{ + $input `,` $base `,` $more attr-dict + }]; + + let hasFolder = 1; + + let summary = "`goto`-style non-consecutively repeating clocked sequence."; + let description = [{ + See `ltl.goto_repeat` op. The `$input` must be an explicitly clocked sequence. + The result is also an explicitly clocked sequence with the same clock domain of `$input`. + }]; +} + def GoToRepeatOp : LTLOp<"goto_repeat", [Pure]> { let arguments = (ins LTLAnySequenceType:$input, @@ -225,6 +429,25 @@ def GoToRepeatOp : LTLOp<"goto_repeat", [Pure]> { }]; } +def ClockedNonConsecutiveRepeatOp : LTLOp<"clocked_non_consecutive_repeat", [Pure]> { + let arguments = (ins + LTLClockedSequenceType:$input, + I64Attr:$base, + I64Attr:$more); + let results = (outs LTLClockedSequenceType:$result); + let assemblyFormat = [{ + $input `,` $base `,` $more attr-dict + }]; + + let hasFolder = 1; + + let summary = "`goto`-style non-consecutively repeating sequence."; + let description = [{ + See `ltl.non_consecutive_repeat` op. The `$input` must be an explicitly clocked sequence. + The result is also an explicitly clocked sequence with the same clock domain of `$input`. + }]; +} + def NonConsecutiveRepeatOp : LTLOp<"non_consecutive_repeat", [Pure]> { let arguments = (ins LTLAnySequenceType:$input, @@ -248,7 +471,6 @@ def NonConsecutiveRepeatOp : LTLOp<"non_consecutive_repeat", [Pure]> { }]; } - //===----------------------------------------------------------------------===// // Properties //===----------------------------------------------------------------------===// @@ -322,45 +544,4 @@ def EventuallyOp : LTLOp<"eventually", [Pure]> { }]; } -//===----------------------------------------------------------------------===// -// Clocking -//===----------------------------------------------------------------------===// - -// 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::ltl"; -} - -def ClockOp : LTLOp<"clock", [ - Pure, InferTypeOpInterface, DeclareOpInterfaceMethods -]> { - let arguments = (ins LTLAnyPropertyType:$input, ClockEdgeAttr:$edge, I1:$clock); - let results = (outs LTLSequenceOrPropertyType:$result); - let assemblyFormat = [{ - $input `,` $edge $clock attr-dict `:` type($input) - }]; - - let summary = "Specify the clock for a property or sequence."; - let description = [{ - Specifies the `$edge` on a given `$clock` to be the clock for an `$input` - property or sequence. All cycle delays in the `$input` implicitly refer to a - clock that advances the state to the next cycle. The `ltl.clock` operation - provides that clock. The clock applies to the entire property or sequence - expression tree below `$input`, up to any other nested `ltl.clock` - operations. - - The operation returns a property if the `$input` is a property, and a - sequence otherwise. - }]; -} - #endif // CIRCT_DIALECT_LTL_LTLOPS_TD diff --git a/include/circt/Dialect/LTL/LTLTypes.td b/include/circt/Dialect/LTL/LTLTypes.td index 194849f37c51..b0e8afb86b65 100644 --- a/include/circt/Dialect/LTL/LTLTypes.td +++ b/include/circt/Dialect/LTL/LTLTypes.td @@ -28,17 +28,41 @@ def LTLSequenceType : LTLTypeDef<"Sequence", "sequence"> { }]; } +def LTLClockedSequenceType : LTLTypeDef<"ClockedSequence", "clocked_sequence"> { + let summary = "LTL clocked sequence type"; + let description = [{ + The `ltl.clocked_sequence` type is the fundamental type for representing + temporal sequences in linear temporal logic, for example, *"on the rising + edge of clk, A is true two cycles after B is true"*. + + This type intrinsically carries its clocking context, explicitly binding a + temporal sequence of events to a specific clock. Operations like ltl.concat, + ltl.and, and ltl.or operate on `ltl.clocked_sequence` operands, ensuring + all sequence operands share the same clock. This makes clock domains + explicit and type-checked, preventing errors and clarifying clock domains + for analysis passes. + + Boolean inputs (`i1`) are implicitly lifted to a zero-length clocked + sequence. Operations that accept a clocked sequence as an operand will use + the `AnyClockedSequence` constraint, which also accepts `i1`. + }]; +} + def LTLPropertyType : LTLTypeDef<"Property", "property"> { let summary = "LTL property type"; let description = [{ - The `ltl.property` type represents a verifiable property built from linear - temporal logic sequences and quantifiers, for example, *"if you see sequence - A, eventually you will see sequence B"*. - - Note that this type explicitly identifies a *property*. However, a boolean - value (`i1`) or a sequence (`ltl.sequence`) is also a valid property. - Operations that accept a property as an operand will use the `AnyProperty` - constraint, which also accepts `ltl.sequence` and `i1`. + The `ltl.property` type represents a clock-agnostic, verifiable property + built from explicitly clocked sequences and quantifiers, for example, *"if + you see sequence A, eventually you will see sequence B"*. + + This type is fundamentally clock-independent - it represents a quantified + statement about explicitly clocked sequences rather than being a clocked + entity itself. The "lifting" from clocked sequences to clock-agnostic + properties occurs via property operators like `ltl.implication`, + `ltl.always`, and `ltl.eventually`. + + Properties can describe relationships between temporal patterns that may + exist in different clock domains, enabling cross-domain verification. }]; } diff --git a/include/circt/Dialect/LTL/LTLVisitors.h b/include/circt/Dialect/LTL/LTLVisitors.h index b5f673195d74..c53cb5d3b1c9 100644 --- a/include/circt/Dialect/LTL/LTLVisitors.h +++ b/include/circt/Dialect/LTL/LTLVisitors.h @@ -23,7 +23,11 @@ class Visitor { return TypeSwitch(op) .template Case( + ClockedAndOp, ClockedOrOp, ClockedIntersectOp, + CreateClockedSequenceOp, ClockedDelayOp, ClockedConcatOp, + IntersectOp, ClockedNonConsecutiveRepeatOp, + ClockedGoToRepeatOp, ClockedRepeatOp, + NonConsecutiveRepeatOp, GoToRepeatOp>( [&](auto op) -> ResultType { return thisCast->visitLTL(op, args...); }) @@ -62,6 +66,15 @@ class Visitor { HANDLE(IntersectOp, Unhandled); HANDLE(NonConsecutiveRepeatOp, Unhandled); HANDLE(GoToRepeatOp, Unhandled); + HANDLE(ClockedAndOp, Unhandled); + HANDLE(ClockedConcatOp, Unhandled); + HANDLE(ClockedDelayOp, Unhandled); + HANDLE(ClockedGoToRepeatOp, Unhandled); + HANDLE(ClockedIntersectOp, Unhandled); + HANDLE(ClockedNonConsecutiveRepeatOp, Unhandled); + HANDLE(ClockedOrOp, Unhandled); + HANDLE(ClockedRepeatOp, Unhandled); + HANDLE(CreateClockedSequenceOp, Unhandled); #undef HANDLE }; diff --git a/lib/Dialect/LTL/LTLFolds.cpp b/lib/Dialect/LTL/LTLFolds.cpp index 963dc2022e18..b695b5c22121 100644 --- a/lib/Dialect/LTL/LTLFolds.cpp +++ b/lib/Dialect/LTL/LTLFolds.cpp @@ -141,3 +141,84 @@ OpFoldResult GoToRepeatOp::fold(FoldAdaptor adaptor) { OpFoldResult NonConsecutiveRepeatOp::fold(FoldAdaptor adaptor) { return RepeatLikeOp::fold(adaptor.getBase(), adaptor.getMore(), getInput()); } + +//===----------------------------------------------------------------------===// +// ClockedAndOp / ClockedOrOp +//===----------------------------------------------------------------------===// + +LogicalResult ClockedAndOp::canonicalize(ClockedAndOp op, + PatternRewriter &rewriter) { + if (op.getType() == rewriter.getI1Type()) { + rewriter.replaceOpWithNewOp(op, op.getInputs(), true); + return success(); + } + return failure(); +} + +LogicalResult ClockedOrOp::canonicalize(ClockedOrOp op, + PatternRewriter &rewriter) { + if (op.getType() == rewriter.getI1Type()) { + rewriter.replaceOpWithNewOp(op, op.getInputs(), true); + return success(); + } + return failure(); +} + +LogicalResult ClockedIntersectOp::canonicalize(ClockedIntersectOp op, + PatternRewriter &rewriter) { + if (op.getType() == rewriter.getI1Type()) { + rewriter.replaceOpWithNewOp(op, op.getInputs(), true); + return success(); + } + return failure(); +} + +//===----------------------------------------------------------------------===// +// ClockedConcatOp +//===----------------------------------------------------------------------===// + +OpFoldResult ClockedConcatOp::fold(FoldAdaptor adaptor) { + // concat(s) -> s + if (getInputs().size() == 1) + return getInputs()[0]; + + return {}; +} + +void ClockedConcatOp::getCanonicalizationPatterns(RewritePatternSet &results, + MLIRContext *context) { + results.add(results.getContext()); +} + +//===----------------------------------------------------------------------===// +// ClockedRepeatLikeOps +//===----------------------------------------------------------------------===// + +namespace { +struct ClockedRepeatLikeOp { + static OpFoldResult fold(uint64_t base, uint64_t more, Value input) { + // clocked_repeat(s, 1, 0) -> s + if (base == 1 && more == 0 && isa(input.getType())) + return input; + + return {}; + } +}; +} // namespace + +OpFoldResult ClockedRepeatOp::fold(FoldAdaptor adaptor) { + auto more = adaptor.getMore(); + if (more.has_value()) + return ClockedRepeatLikeOp::fold(adaptor.getBase(), *more, getInput()); + return {}; +} + +OpFoldResult ClockedGoToRepeatOp::fold(FoldAdaptor adaptor) { + return ClockedRepeatLikeOp::fold(adaptor.getBase(), adaptor.getMore(), + getInput()); +} + +OpFoldResult ClockedNonConsecutiveRepeatOp::fold(FoldAdaptor adaptor) { + return ClockedRepeatLikeOp::fold(adaptor.getBase(), adaptor.getMore(), + getInput()); +}