[LTLToCore] Lower LTL delay/clock patterns to core logic#9722
[LTLToCore] Lower LTL delay/clock patterns to core logic#9722robert-at-pretension-io wants to merge 3 commits intollvm:mainfrom
Conversation
TaoBi22
left a comment
There was a problem hiding this comment.
Hi @robert-at-pretension-io, thanks for taking a stab at this too! It would be great to support these cases, but it looks to me like what you've added to LTLToBMC would probably make sense to have in LTLToCore instead, since they all seem to tackle the issue by modelling the LTL using core dialects (LTLToCore isn't in the circt-bmc pipeline yet, but I've been meaning to add it so I'll open a PR for that to not stall you).
9ab3a65 to
b726cd2
Compare
1962c91 to
496ca58
Compare
TaoBi22
left a comment
There was a problem hiding this comment.
Thanks for taking another pass @robert-at-pretension-io - just some high level comments for now, I'll do another review once they're addressed to avoid any redundant feedback
496ca58 to
5f4aca5
Compare
5f4aca5 to
7428acf
Compare
TaoBi22
left a comment
There was a problem hiding this comment.
Thanks for swapping this to use pattern matching infrastructure @robert-at-pretension-io! It looks like now the rewrites are defined as patterns over AssertLike operations, but are actually rewriting ops further up the DAG rather than the AssertLike operations. Could this instead be some patterns on those actual ops? (I think it violates MLIR pattern rewriter restrictions to not actually modify the op the pattern is operating on)
Summary
Lowers
ltl.delay,ltl.implication, andltl.clockpatterns into corecomb/seqlogic during theLowerLTLToCorepass. This allows boundedmodel checking pipelines (like
circt-bmc) to natively verify temporal hardware properties.Details
Extends the existing
LowerLTLToCorepass to translate high-level LTL timing properties into physical hardware monitors (shift registers andcombinational gates). The lowering is implemented safely within MLIR's
OpConversionPatterninfrastructure (AssertLikeConversion), ensuringseamless integration with the pass driver's legality checks.
Key Features:
##N): Lowers strict delays by shifting the antecedent throughNseq.compregflip-flops and checking implication against theconsequent.
##[N:M]): Lowers bounded windows by generating a "pending request" token monitor. The monitor shifts forward each cycleand is dynamically cleared if the consequent is observed while the window is open. A violation is triggered if the token reaches the deadline
unsatisfied.
unsupported LTL delay pattern for LowerLTLToCore).circt::ltl::LTLDialectincirct-bmc.cppso the tool can safely parse and traverse LTL properties beforethey are lowered to core.
Tests Added
test/Conversion/LTLToCore/ltl-delay-ok.mlir: Validates the correct generation of shift registers and boolean logic for both exact and boundeddelays (via
FileCheck).test/Conversion/LTLToCore/ltl-delay-error.mlir: Ensures unbounded delays are properly rejected and flagged (via--verify-diagnostics).