circt
circt copied to clipboard
llvm
RFC: [AIG] Add an AIG dialect and circt-synth
This proposes AIG(And Inverter Graph) dialect which is meant to be a foundational dialect for logic synthesis.
Please see docs/Dialects/AIG/RationaleAIG.md and include/Diaclects/AIG/AIGOps.td for design details.
This PR implements E2E flow for FPGA synthesis with a naive implementation for LUT mapping (test/circt-synth/lut-size.mlir). Only comb.and/or/xor are supported as an input but it’s straightforward to implement a lowering for arithmetic ops. Right now comb.truth_table op is used as a target of LUT mapping.
We probably still want Yosys integration (https://github.com/llvm/circt/pull/7663) but CIRCT-native synthesizer would be worth doing in the long term.
Since the developing of logic synthesis is really a non-trivial work, I wonder rather than using CIRCT to do the synthesis job by itself, how about exporting the aiger file directly, and then we can consume it by abc or mockturtle for future use.
Since the developing of logic synthesis is really a non-trivial work, I wonder rather than using CIRCT to do the synthesis job by itself, how about exporting the aiger file directly, and then we can consume it by abc or mockturtle for future use.
Implementing AIGER file exporter/importer is trivial once we lowered the IR to (low) AIG dialect (= aig.and_inv is lowered to have a single bit and two operands). It's totally reasonable to have an integration with AIGER file to leverage other tools and I'm happy to work/help on that!
That said even though I agree it's non-trivial to implement logic synthesizer but I believe it would be feasible to get OK results once we implemented necessary passes (Lower to FRAIG, Bit-sensitive IMCP/IMDCE, inlining, re-balancing).
This is super exciting :partying_face:! I still have to look through the code in more detail. One question I had after a cursory look: is it beneficial to allow each operand in aig.and_inv to be inverted, or does that make writing passes more complex? I think I remember seeing other implementations make the single output of the AND gate invertable, which would mean it's just a boolean on the op.
One question I had after a cursory look: is it beneficial to allow each operand in aig.and_inv to be inverted, or does that make writing passes more complex?
Inverting on operands would be more closer to traditional AIG format including AIGER (thank you for checking @fabianschuiki!) so the current representation seems to be right way to go.
@maerhart Thank you for really detailed review! and really sorry for a bunch of dirty code remaining in my PR. I'll make sure to double check basic stuffs before removing draft..
Thank you really for detailed review @mikeurbach @fabianschuiki @maerhart! I'm going to merge basic stuffs in refined PRs/commits. I'll separate non-trivial passes (GreedyCutDecomp, CutToLUT) into a different PR for the ease of review.