[LTL] Add ClockedAtomOp description#10541
Conversation
|
This looks like it's moving in the right direction to me (though CC: @fabianschuiki since he and I have spoken about this kind of thing a few times). I wonder if it's worth holding off on merging this until we've finished migrating the DelayOp? Otherwise it seems like we might end up with no way to provide a clock for a DelayOp. (sorry for the Copilot review, I hit the button by accident and it doesn't seem to let you cancel it 🤦) |
|
@TaoBi22 That's perfectly fine👍 ! But what means Another set of analyses includes These two solutions are independent of each other. My expectation is that after the latter is implemented, these two solutions will coexist for a period of time, then we will migrate to Chisel and completely deprecate |
Motivation
ltl.clockcurrently carries too many responsibilities.As clock operands become explicit on operations such as
ltl.clocked_delayandltl.past, the remaining scope ofltl.clockbecomes much smaller. Once frontends stop emitting implicitly clocked temporal operations, the remaining necessary use ofltl.clockis to assign a sampling clock to boolean atoms.Change
This PR introduces
ltl.clocked_atomto separate out that responsibility. It converts ani1into an!ltl.sequenceunder an explicit clocking event.With this op, LTL can move toward a cleaner form: no
ltl.clock, every operation that needs a clock gets one explicitly from the frontend, and every!ltl.sequenceproduced from ani1is clocked throughltl.clocked_atom.Follow-up
ltl.clocked_atomwill require updates to passes and canonicalizations that currently handleltl.clock. Those changes will be implemented in follow-up PRs.Assisted-by: Codex:gpt-5.5