[firtool] btor2 integration

[dobios]

Hi,

This PR adds a btor2 target to firtool.
The goal is to expose this directly in Chisel later.

The one thing I might add here is that it might also be useful to add the arc::InlineModulesPass to the pipeline, as module instances need to be inlined in order to get something that will work in btor2, but I wanted to get some opinions first before integrating some pass from an unrelated dialect into the pipeline.

Let me know what you think!

[uenoku]

Can we add a simple test for this pipeline? It would be also great if there is an integration test to check/run emitted btor2 with btormc or something.

[dtzSiFive]

Woohoo!!

Please register the pass with the other conversion passes so MLIR debugging bits work with this, I'm on mobile but can be more useful about what I mean if unclear!

[dobios]

Woohoo!!

Please register the pass with the other conversion passes so MLIR debugging bits work with this, I'm on mobile but can be more useful about what I mean if unclear!

I'm not quite sure that I understand what you mean by this, is this something specific to firtool or more general?

[dtzSiFive]

@dobios

circt/tools/firtool/firtool.cpp

Line 718 in f424ea3

registerLowerSimToSVPass();

, need passes registered when parsing command line options for some bits to work.

[dobios]

@dobios

circt/tools/firtool/firtool.cpp

Line 718 in f424ea3

registerLowerSimToSVPass();

, need passes registered when parsing command line options for some bits to work.

@dtzSiFive Got it, registered the pass with the other conversion passes!

[maerhart]

If people agree, we could also move the InlineModulesPass to HW transforms, as it only operates on HW operations and doesn't need a dependency on Arc.

[fabianschuiki]

If people agree, we could also move the InlineModulesPass to HW transforms, as it only operates on HW operations and doesn't need a dependency on Arc.

That sounds like a good idea! Maybe FlattenModulesPass to indicate that it doesn't make any decisions about when to inline, it just inlines everything.

[fabianschuiki]

This looks good to me! It would be great to have a tiny test that sanity checks whether you get something when you ask for this btor output. I'm not sure if we do this for some of the other formats, but it would probably be good to do so. There should be a firtool test directory where you could add something like target-btor.mlir to check this new emission option.

[uenoku]

That sounds like a good idea! Maybe FlattenModulesPass to indicate that it doesn't make any decisions about when to inline, it just inlines everything.

Can we instead add a callback to decide whether a module should be inlined? This approach would be useful when we want to inline only small modules etc.

[dtzSiFive]

Can we instead add a callback to decide whether a module should be inlined? This approach would be useful when we want to inline only small modules etc.

MLIR has an inliner interface -- maybe something like that, vs pass having a callback?
Ah, not question of legality but of intent (hence as an option/parameter/callback to the pass).

[fabianschuiki]

We could definitely try to reuse the inliner interface, or model something after that. Do we have a use case for that at the moment? Might make sense to simply do the move to unblock some work, and then add the interface and per-module inlining control ontop of that. It would be nice to have a proper inliner 😃.

[uenoku]

Ah, not question of legality but of intent (hence as an option/parameter/callback to the pass).

Yes probably the inliner cost model is not uniform so I think it's nicer to set a cost model aside from dialect interface. Checked MLIR inliner and the current design is to separate inlining logic into a helper struct which takes a predicate (https://discourse.llvm.org/t/inliner-cost-model/2992/13 and llvm/llvm-project#84258) so probably we can do the similar thing.

Anyway I think the PR looks good to me if there is a simple test for it 👍

[dtzSiFive]

Sounds great! Thanks for the links and explanation. Simply moving first seems like the way to go, agreed 👍.

[dobios]

I'm waiting to get #6964 merged in before merging this one, as it would break if modules aren't inlined beforehand.

[sequencer]

cc @SpriteOvO this should be included in the PanamaBinding in chisel.