Lowering From LTL to Core (original) (raw)

I’m fairly new to CIRCT, so apologies if I’m overlooking something obvious.
I was experimenting with the LTL dialect and tried lowering it to the core dialect using the ./circt-opt -lower-ltl-to-core
However, it doesn’t seem to handle LTL operators like I expected.

Here’s a simple example:

Input MLIR:

hw.module @test(in %a : !ltl.sequence, in %b : !ltl.sequence) {
  %true = hw.constant true
  %1 = ltl.delay %true, 1, 0 : i1
  %2 = ltl.concat %a, %1 : !ltl.sequence, !ltl.sequence
  %3 = ltl.implication %2, %b : !ltl.sequence, !ltl.sequence
}

I would expect it to convert the LTL dialect over to an core dialect.
However if i run it through ./circt-opt -lower-ltl-to-core <file>.mlir it becomes

module {
  hw.module @test(in %a : !ltl.sequence, in %b : !ltl.sequence) {
    %true = hw.constant true
    %0 = ltl.delay %true, 1, 0 : i1
    %1 = ltl.concat %a, %0 : !ltl.sequence, !ltl.sequence
    %2 = ltl.implication %1, %b : !ltl.sequence, !ltl.sequence
    hw.output
  }
}

As you can see, none of the LTL operations are lowered. From the Git history, it seems like support for this lowering has been added, so I’m wondering if I’m missing a required flag or precondition for it to work. Or it has been broken in a later build.

Any insight would be awesome.

Hey @Collin! Unfortunately the LTL-to-Core conversion pass is more or less a stub at the moment. We would love to have a pass that translates the LTL dialect into something closer to hardware. The fact that some properties that you can express in the LTL dialect require potentially unbounded memory to match, which makes lowering to the core dialect very challenging.

If your final goal is to get Verilog out of CIRCT, you can throw the LTL dialect directly at ExportVerilog. The exporter will print the LTL formula as SystemVerilog sequences, properties, and assertions.

Sorry that this doesn’t yet work out of the box. I’d love to hear your thoughts and insights on how a mapping of the LTL dialect to the core dialects could look like, or what you’d expect as a final result of such a lowering

Collin May 12, 2025, 8:46am 3

Hey @fabianschuiki, no need to be sorry.
The main idea i my head would be to get some sort of LTL + Verif down to the core dialect, which means the properties can be changed to RTL. That way some properties of a system could be checked in any opensource checker, instead of cadence as an example.

Immediate and Deferred assertions seems trivial, but concurrent assertion would require some way of storing values across clock/events.

My look into System Verilog and how they handle properties seems to be shift registers with some control around it, and unbounded memory could be done with those. Which could be described with the core dialects.
The book SVA: The power of Assertions in SystemVerilog at least describes the lowering of SVA properties like without going into detail. (Has been a year since i looked in the book and i can’t find it again)

It seems simple in concept, but actually exploring the difficulties associated with it might be very different from easy.

I don’t think this would be optimal for formal verification, but could help with simulation based verification.

Would like to say i have only taken a rough look into it yet, so can’t say the total feasibility of anything.

Lastly saw your + others paper on LTL to core.
https://www.cs.princeton.edu/~ad4048/pdfs/latte25-final14.pdf. Which seems like an excellent starting point for simple SVA.

You say, you can change LTL into SVA, but does it work the opposite way as in SVA to LTL as that would also be good. Though can understand some problems with it.

Lowering from LTL+Verif to core would be absolutely fantastic! There is some precedence in Yosys to do that to a certain degree, although only through the Verific frontend of Yosys. I’m not familiar with the book you mentioned, but if it outlines a few lowerings we might as well take those as a starting point . @adobis might also have other ideas and insights. That LATTE paper was an initial idea we had to try to go from the expression grammar representation of SVA and try to lower it to something that looks more like an IR, with ops representing certain boxes/matchers/states. Similar to how BNF-like grammars can be transformed/lowered to a state machine recognizing that language.

SVA to LTL is definitely something CIRCT is working towards. The circt-verilog frontend is progressing very nicely, but it’s still missing the SVA support. The LTL dialect seems like a natural lowering target. There has been some recent interest in getting SVA support into circt-verilog; a few discussions have sprung up in the weekly CIRCT Open Design Meeting.