So I rewrote the pass to do a (fairly hacky) backwards walk from the assertion to handle all of the ltl ops. This allowed me to integrate the direct lowering (without the use of an automata conversion) of ltl.implication, ltl.concat, and ltl.delay, which allows for the expression of properties that fit the "basic" non-overlapping and overlapping implication form, i.e. something like :

bool a, b
int n

a |=> b
a ##n true |-> b
a |-> b

The implementation is incredibly special cased and only supports these three cases due to the complexity of implementing a generic version of this without an even more complex automata conversion and deterministication before hand, which I have only gotten working reasonably (so without state explosion) by using an external tool called SPOT. I don't think that having such an external dependency would make sense for CIRCT, which is why I propose this more realistic implementation following a technique similar to the one implemented in symbiyosys and BSV.

Let me know what you think !

Sorry if this is not going to be a focused review and mostly me rambling instead, but this is stretching my knowledge of both MLIR rewrites and SVA/LTL. So, I may well be writing nonsense.

Let's start with an easy point: The conversion of non-overlapping implications is currently incorrect. For a ##n true |-> b you are delaying true and ignoring a. If you run./build/bin/circt-opt --lower-ltl-to-core test/Conversion/LTLToCore/noi.mlir | ./build/bin/circt-opt --canonicalize --lower-seq-to-sv --prepare-for-emission --export-verilog you can see that the assertion just checks b staying high one cycle after reset.

Now for the rambling part: As you mention yourself the implementation is fairly hacky and there is a bunch of minor stuff in need of fixing or tidying. But I think that there is still the more fundamental problem of this pass being stuck in a limbo between being a full-fledged dialect conversion and just a transformation of two very specific patterns. If I understand you correctly, you're saying that this problem in general is too complex for a simple conversion pass. So we should just commit to matching these patterns and leave everything else alone.
In this case, I think, the HasBeenResetOp needs to be included in the pattern. Firstly, if you convert it individually, you'll just end up with a dangling UnrealizedConversionCast. Secondly, by including it you get a reliable handle on the reset signal and do not need the less than ideal heuristic of looking for a port called "reset" in the other pattern.

Matching on DAG patterns is such a fundamental thing in MLIR that I feel there should be no need for you to implement the walk manually. To my surprise I cannot find an obvious example of how this should be done, which probably means I' missing something. The options I can see which would hopefully provide a more robust and legible solution:

1. Using the RecursivePatternMatcher class via matchPattern and m_Op<...>(m_Op<...>(...)) in a custom rewrite/conversion pattern
2. Using DRR to define a rewrite in TableGen
3. Using PDLL for a particularly fancy solution

I'm far too inexperienced to tell you which, if any, of those is the right way. I'd have to try it myself. But I'm sure someone around here knows. 😁

For the theoretical aspects of dealing with more complex SVA or LTL expressions, the best thing I can do is to ping @fzi-antonpaule . In contrast to me he actually knows about this stuff and has also done work on integrating SVA in Chisel in the past.

Sorry if this is not going to be a focused review and mostly me rambling instead, but this is stretching my knowledge of both MLIR rewrites and SVA/LTL. So, I may well be writing nonsense.

Let's start with an easy point: The conversion of non-overlapping implications is currently incorrect. For a ##n true |-> b you are delaying true and ignoring a. If you run./build/bin/circt-opt --lower-ltl-to-core test/Conversion/LTLToCore/noi.mlir | ./build/bin/circt-opt --canonicalize --lower-seq-to-sv --prepare-for-emission --export-verilog you can see that the assertion just checks b staying high one cycle after reset.

Now for the rambling part: As you mention yourself the implementation is fairly hacky and there is a bunch of minor stuff in need of fixing or tidying. But I think that there is still the more fundamental problem of this pass being stuck in a limbo between being a full-fledged dialect conversion and just a transformation of two very specific patterns. If I understand you correctly, you're saying that this problem in general is too complex for a simple conversion pass. So we should just commit to matching these patterns and leave everything else alone. In this case, I think, the HasBeenResetOp needs to be included in the pattern. Firstly, if you convert it individually, you'll just end up with a dangling UnrealizedConversionCast. Secondly, by including it you get a reliable handle on the reset signal and do not need the less than ideal heuristic of looking for a port called "reset" in the other pattern.

Matching on DAG patterns is such a fundamental thing in MLIR that I feel there should be no need for you to implement the walk manually. To my surprise I cannot find an obvious example of how this should be done, which probably means I' missing something. The options I can see which would hopefully provide a more robust and legible solution:

1. Using the `RecursivePatternMatcher` class via `matchPattern` and `m_Op<...>(m_Op<...>(...))` in a custom rewrite/conversion pattern

2. Using [DRR](https://mlir.llvm.org/docs/DeclarativeRewrites/) to define a rewrite in TableGen

3. Using [PDLL](https://mlir.llvm.org/docs/PDLL/) for a particularly fancy solution

I'm far too inexperienced to tell you which, if any, of those is the right way. I'd have to try it myself. But I'm sure someone around here knows. 😁

For the theoretical aspects of dealing with more complex SVA or LTL expressions, the best thing I can do is to ping @fzi-antonpaule . In contrast to me he actually knows about this stuff and has also done work on integrating SVA in Chisel in the past.

Thanks for the detailed comment. I was currently aware that my a ##n true |=> b implementation was maybe a bit iffy, I've been trying to figure out good ways to test it, I was hoping that you would catch it and maybe help me out with it a bit, doing a direct lowering is quite tricky for that type of pattern. I will try to tackle that lowering again, it seemed to work well on paper, so I might have just messed something up in the implementation, I'll take another look. My main goal with opening this pr again was to get more opinions on the weird backwards walk that I mentioned on discord a few days ago.

As for the backwards walk, this was a solution to all of the comments that were against the forward walk (which I understand). The way I did it was super hacky for several reasons (including a severe time crunch on my side ^^"), but mostly in hopes of hearing of a better solution from more MLIR-adept people, thank you for that btw :). I don't think that including HasBeenReset in that walk is a good idea to retrieve the reset, as it is only generated when no explicit disable condition was given for the assertions. Given that it's presence in not guaranteed, I don't want to rely on it to gain access to the reset, so I think that my sub-ideal heuristic is still better than relying on an optional operation. But as you mentioned the main issue is the hackyness of the walk itself, for which I need to look into the methods you mentioned and use those.

Either way, thank you for the review, I will take a deeper at this and see if I can use one of the methods you recommended.

@fzi-hielscher I found my typo in the implementation, I confused delay.getInput() with concat.getInputs.front(). The NOI lowering should work now.

Just also wanted to add a final comment about a more general LTL conversion. It's not that it's impossible to do, it's just that finding a direct lowering like the one I'm proposing here isn't something that can be done in the general case. A solution to this would be to generate a Büchi automaton from the LTL equivalent of the SVA property (if any), and then massage and lower this into a deterministic form that can be implemented in hardware. There are two reasons why I'm not taking this approach:

1. There is no elegant way (yet) to encode general automata in MLIR, so I would have to do this through an in-memory representation which is just unreasonable given the amount of optimizations that are needed on the output automaton in order to synthesize it in a reasonable manner. Hyper-engineered tools such as SPOT which have been improved and optimized for over a decade, are basically all we have to do this task efficiently, and re-implementing it from-scratch in a standalone pass is an unreasonably difficult and lengthy task.
2. Generalizing the automata conversion is actually surprisingly tricky. I banged my head against a wall for half a year and came up with a method to do so, but it's just unreasonable to implement and is difficult to compose with other methods. The idea is to generate "atomic automata" from every base operation of the type property(a, b); a, b: bool where the property can be any single SVA operation, and to create merge semantics for each operation that describe how to connect the initial, active, and dead states of the lhs automaton to those in the rhs automaton (often requiring a form of state Cartesian product between the two causing a state explosion if no nodes are collapsed or optimized out). The issue with this is that it almost always produces a non-deterministic automaton and thus requires some form of determistication (if that's even a word) to get it into an FSM-ish form that we can them implement in the core dialect. This process is well known but is also NP complete so it's quite time consuming to implement in a way that outputs useful results and would be unreasonable to do inside of an already super complex pass that does a bunch of other stuff, which is why I'm advocating for a generalized automata dialect in CIRCT.

All of this rambling is to justify why I took this hyper-special-cased approach, and I hope that in the future, I (or someone else) will have the time (and resources) to tackle the more general approach, but that just isn't the case right now.

I just throw in my two cents worth.
Implementing a general approach where you convert any LTL formula to the core hardware dialects just to use it in formal verification via the btor2 transformation is probably possible but way too much effort.

Tools like SPOT and LamaConv already implement the automaton transformations you need, but without a generalized automaton dialect in CIRCT, you cannot take full advantage of the tools' capabilities.
If you restrict your LTL formulae to safety properties and bounded sequences, this would be a viable option to start with.
For a well-designed subset of bounded LTL properties, you could implement a naive conversion by unrolling all delays without using SPOT or LamaConv.
For bounded model checking, this should work perfectly but synthesizing optimal runtime monitors is a different story.

I just throw in my two cents worth. Implementing a general approach where you convert any LTL formula to the core hardware dialects just to use it in formal verification via the btor2 transformation is probably possible but way too much effort.

Tools like SPOT and LamaConv already implement the automaton transformations you need, but without a generalized automaton dialect in CIRCT, you cannot take full advantage of the tools' capabilities. If you restrict your LTL formulae to safety properties and bounded sequences, this would be a viable option to start with. For a well-designed subset of bounded LTL properties, you could implement a naive conversion by unrolling all delays without using SPOT or LamaConv. For bounded model checking, this should work perfectly but synthesizing optimal runtime monitors is a different story.

Thanks for your input!
I completely agree that a full integration of tools like SPOT are the most reasonable approach for a generalized solution. CIRCT has an fsm dialect that can be used to integrate the optimized deterministic outputs from SPOT, but currently the mindset in this project is to avoid all external dependencies so I do think that such a contribution can ever get upstreamed unfortunately. The method I'm currently is as you describe, so a naive unrolling of delays (as long as there isn't any fancy nesting going on).

Thanks again for your input!

I've done a little experimenting to simplify the matching: I have not felt adventurous enough to try PDLL though. As impressive as it is conceptually, it seems to get very little use. DRR would be nice to use but it won't work, at least not for the non-overlapping case. We need to match on the ConcatOp's variadic operands. DRR cannot do that. ☹️

I had more luck with the RecursivePatternMatcher but needed define two helper matchers. The first one to specifically match on single bit integers:

struct I1ValueMatcher {
  Value *what;
  I1ValueMatcher(Value *what) : what(what) {}
  bool match(Value op) const {
    if (!op.getType().isSignlessInteger(1))
      return false;
    *what = op;
    return true;
  }
};

static inline I1ValueMatcher m_Bool(Value* const val) { return I1ValueMatcher(val); }

Secondly, m_Op cannot capture or match on attributes. But we need them on the delay and clock ops. So, I fudged it to at least capture a reference on the matching operation:

template <typename OpType, typename... OperandMatchers>
struct BindingRecursivePatternMatcher: mlir::detail::RecursivePatternMatcher<OpType, OperandMatchers...> {
  
  using BaseMatcher = mlir::detail::RecursivePatternMatcher<OpType, OperandMatchers...>;
  BindingRecursivePatternMatcher(OpType *_op, OperandMatchers... matchers)
    : BaseMatcher(matchers...), opBind(_op) {}

  bool match(Operation *op) {
    if (BaseMatcher::match(op)) {
      *opBind = llvm::cast<OpType>(op);
      return true;
    }
    return false;
  }

  OpType *opBind;
};

template <typename OpType, typename... Matchers>
static inline auto m_OpWithBind(OpType *op, Matchers... matchers) { 
    return BindingRecursivePatternMatcher<OpType, Matchers...>(op, matchers...); 
} 

This may be evil, but I think it's okay. It should then allow us to boil the actual matching on the AssertOp's argument down to (for the non-overlapping case):

...
Value ltlClock, disableCond, antecedent, consequent;
ltl::ClockOp clockOp;
ltl::DelayOp delayOp;

bool matched = matchPattern(op.getProperty(), 
        m_OpWithBind<ltl::ClockOp>(&clockOp,
            m_Op<ltl::DisableOp>(
              m_Op<ltl::ImplicationOp>(
                m_Op<ltl::ConcatOp>(
                  m_Bool(&antecedent),
                  m_OpWithBind<ltl::DelayOp>(&delayOp,
                    m_One())),
                m_Bool(&consequent)),
              m_Bool(&disableCond)),
            m_Bool(&ltlClock)));


if (!matched || delayOp.getLength() != 0)
  return failure();
...

It should also give easy access to all the values and attributes required for the rewrite, except for the reset...

I don't think that including HasBeenReset in that walk is a good idea to retrieve the reset, as it is only generated when no explicit disable condition was given for the assertions. Given that it's presence in not guaranteed, I don't want to rely on it to gain access to the reset, so I think that my sub-ideal heuristic is still better than relying on an optional operation.

You're right. Thinking about it again, it should not be part of the pattern. My first point was actually incorrect. Since
HasBeenResetOp returns an i1 we don't actually need any type conversions. However, I still dislike just grabbing the "reset" port. In fact, I'd even say it is semantically wrong to do so. You are effectively making your result depend on an arbitrary signal that is never mentioned in the original sequence of operations. And I don't think it is correct to assume this dependency implicitly. That's just my gut feeling though. I have not fully grasped the nitty-gritty details of the DisableOp's semantics yet and how it interacts with temporal relations.

Thanks a lot for exploring betters ways to write this backwards walk, I think I can definitely use that to make things a whole lot more readable!

As for the use of the reset, I see what you mean, you are right that in the particular case where the antecedent is an input, then this implicit tying to the reset doesn't make as much sense. This isn't clearly defined anywhere, so I basically need to make some decision about implementing the more subtle parts, maybe this would require a bit more discussion first.

I could check the defining op of the antecedent and use it's reset as the delay register's reset in the case where it's a resetable register, and then just not tie our generated registers to any reset if the antecedent doesn't have one. What do you think?

I updated the pass to use the RecursivePatternMatcher that was recommended to drastically clean my special casing up. I also changed the implementation such that the generated registers use the disable condition as their resets instead of the implicit reset. Let me know if there's anything else bothering you about the pass!

It has definitely become more readable now. 👍 It is also making it fairly obvious that there is a hierarchy on your patterns: Generic AssertProperty > OI > NOI. So, you should not be matching on the most specialized case (NOI) first. Start with the generic case. If that one does not match there is no point in continuing. If it does match, you don't need to match the outer operations again. That way you can split up the rather monstrous NOI pattern.

Since you are not actually doing any type conversions anymore, I would consider ditching the dialect conversion framework in favor of the simpler greedy rewriter. That should trim down the code some more.

Finally, when you do the cleanup, you can't just erase the operations. You need to check that they have not other uses first.

I think after that, the pass should be in a decent general shape and we can start with the pedantic stuff. 😁

This is being reworked and will be part of a few separate PRs, so I'm going to close this one.