Skip to content

[LTL] Add explict clocked operations and types #9026

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Draft
wants to merge 1 commit into
base: main
Choose a base branch
from
Draft

[LTL] Add explict clocked operations and types #9026

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
265 changes: 223 additions & 42 deletions include/circt/Dialect/LTL/LTLOps.td
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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<InferTypeOpInterface>]> {
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<LTLClockedSequenceType>:$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<LTLClockedSequenceType>:$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.
}];
}
Comment on lines +131 to +163
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Do and/or operations require a clock? These oparations sound like they only take two sequences and performa a boolean and/or on them. But if those sequences contain any delays, those delays would already specify a clock. Wouldn't that suffice?

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Do and/or operations require a clock? These oparations sound like they only take two sequences and performa a boolean and/or on them. But if those sequences contain any delays, those delays would already specify a clock. Wouldn't that suffice?

The clock in the operand is mainly used to specify the clock of the result type, because when two operands are in different clock domains, the clock of the result becomes difficult to determine


def ClockedIntersectOp : LTLOp<"clocked_intersect", [Pure, Commutative]> {
let arguments = (ins
Variadic<LTLClockedSequenceType>:$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<I64Attr>:$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`
}];
}
Comment on lines +182 to +215
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

It's very cool that we get a properly clocked delay operation! Could we just name this ltl.delay and delete the old unclocked ltl.delay? I don't think we need both ops.

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

It's very cool that we get a properly clocked delay operation! Could we just name this ltl.delay and delete the old unclocked ltl.delay? I don't think we need both ops.

Yes! This is a good suggestion, in fact I'm not sure if break changes should be made in this PR, if you think it's okay then it would be a good idea to replace the delay entirely


def DelayOp : LTLOp<"delay", [Pure]> {
let arguments = (ins
LTLAnySequenceType:$input,
Expand Down Expand Up @@ -119,6 +268,24 @@ def PastOp : LTLOp<"past", [Pure]> {
}];
}

def ClockedConcatOp : LTLOp<"clocked_concat", [Pure]> {
let arguments = (ins
Variadic<LTLClockedSequenceType>:$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.
}];
}

Comment on lines +271 to +288
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Same as with the and/or operation: ltl.concat probably doesn't need to know what clock the input sequences are sensitive to. The concat corresponds to a ##0 b in Verilog, which means a and b happen at the exact same time, not a specific clocked delay apart. And since there's no delay, the op probably doesn't need a clock 🤔

def ConcatOp : LTLOp<"concat", [Pure]> {
let arguments = (ins Variadic<LTLAnySequenceType>:$inputs);
let results = (outs LTLSequenceType:$result);
Expand Down Expand Up @@ -178,6 +345,24 @@ def ConcatOp : LTLOp<"concat", [Pure]> {
}];
}

def ClockedRepeatOp : LTLOp<"clocked_repeat", [Pure]> {
let arguments = (ins
LTLClockedSequenceType:$input,
I64Attr:$base,
OptionalAttr<I64Attr>:$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,
Expand All @@ -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,
Expand All @@ -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,
Expand All @@ -248,7 +471,6 @@ def NonConsecutiveRepeatOp : LTLOp<"non_consecutive_repeat", [Pure]> {
}];
}


//===----------------------------------------------------------------------===//
// Properties
//===----------------------------------------------------------------------===//
Expand Down Expand Up @@ -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<InferTypeOpInterface>
]> {
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
40 changes: 32 additions & 8 deletions include/circt/Dialect/LTL/LTLTypes.td
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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.
}];
}
Comment on lines +31 to 67
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Do we need to distinguish between these two? If we have all clocked operations (basically just delay, repeat, and some of the goto stuff I'd guess) have an explicit clock, and all other operations are clock agnostic (because they don't need a clock to express their semantics), I think all of that would just be a plain old !ltl.property. I don't think we need an explicit distinction betweem clocked and unclocked here 🤔. When we emit things to Verilog, we can just scan the LTL operations to find all the clocks used, and insert @(posedge clock) around all the LTL ops that share the same clock 🤔

Copy link
Contributor Author

@Clo91eaf Clo91eaf Oct 2, 2025 •
edited
Loading

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Do we need to distinguish between these two? If we have all clocked operations (basically just delay, repeat, and some of the goto stuff I'd guess) have an explicit clock, and all other operations are clock agnostic (because they don't need a clock to express their semantics), I think all of that would just be a plain old !ltl.property. I don't think we need an explicit distinction betweem clocked and unclocked here 🤔. When we emit things to Verilog, we can just scan the LTL operations to find all the clocks used, and insert @(posedge clock) around all the LTL ops that share the same clock 🤔

Yes, thank you for your suggestion. After thinking about it, I agree with your point. There are actually two core aspects here: the "clock of the operands" and "clocked delays". For operations like concat/and/or, if the operands are in different clock domains, the semantics become unclear, so these operations do not need to explicitly carry a clock—it's enough to ensure that all their input operands have the same clock.

Although the proposal in #8673 suggests enforcing clock consistency for operands at the type system level, the fundamental goal is to prevent combining operands from different clock domains. In other words, these logical/combination operations can be designed as clock-agnostic—as long as the type system guarantees that operands with different clocks cannot be mixed, the semantics remain clear.

Additionally, I will remove APIs such as clocked_and and clocked_or. Based on our discussion and the recommendations from #8673, as long as these logical operations ensure operand clocks are consistent, there's no need to explicitly distinguish "clocked" versions of and/or. This will make the API simpler and the type system clearer.

Thank you again for your insightful suggestions!


Expand Down
15 changes: 14 additions & 1 deletion include/circt/Dialect/LTL/LTLVisitors.h
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -23,7 +23,11 @@ class Visitor {
return TypeSwitch<Operation *, ResultType>(op)
.template Case<AndOp, OrOp, DelayOp, ConcatOp, RepeatOp, NotOp,
ImplicationOp, UntilOp, EventuallyOp, ClockOp,
IntersectOp, NonConsecutiveRepeatOp, GoToRepeatOp>(
ClockedAndOp, ClockedOrOp, ClockedIntersectOp,
CreateClockedSequenceOp, ClockedDelayOp, ClockedConcatOp,
IntersectOp, ClockedNonConsecutiveRepeatOp,
ClockedGoToRepeatOp, ClockedRepeatOp,
NonConsecutiveRepeatOp, GoToRepeatOp>(
[&](auto op) -> ResultType {
return thisCast->visitLTL(op, args...);
})
Expand Down Expand Up @@ -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
};

Expand Down
Loading