24#include "mlir/Analysis/TopologicalSortUtils.h"
25#include "mlir/IR/Builders.h"
26#include "mlir/IR/BuiltinOps.h"
27#include "mlir/IR/DialectRegistry.h"
28#include "mlir/IR/OperationSupport.h"
29#include "mlir/IR/RegionKindInterface.h"
30#include "mlir/IR/Visitors.h"
31#include "mlir/Support/LogicalResult.h"
32#include "mlir/Tools/mlir-translate/Translation.h"
33#include "llvm/ADT/DenseMap.h"
34#include "llvm/ADT/EquivalenceClasses.h"
35#include "llvm/ADT/SmallVector.h"
36#include "llvm/ADT/StringExtras.h"
37#include "llvm/ADT/StringRef.h"
38#include "llvm/Support/Debug.h"
39#include "llvm/Support/raw_ostream.h"
49#define DEBUG_TYPE "export-aiger"
57 return hw::getBitWidth(value.getType());
73 : module(module), os(os), options(options), handler(handler) {}
76 LogicalResult exportModule();
79 using Object = std::pair<Value, int>;
83 llvm::raw_ostream &os;
88 DenseMap<Object, unsigned> valueLiteralMap;
91 unsigned getNumInputs() {
return inputs.size(); }
92 unsigned getNumLatches() {
return latches.size(); }
93 unsigned getNumOutputs() {
return outputs.size(); }
94 unsigned getNumAnds() {
return andGates.size(); }
96 llvm::EquivalenceClasses<Object> valueEquivalence;
97 SmallVector<std::pair<Object, StringAttr>> inputs;
98 SmallVector<std::tuple<Object, StringAttr, Object>>
100 SmallVector<std::pair<Object, StringAttr>> outputs;
101 SmallVector<std::tuple<Object, Object, Object>> andGates;
103 std::optional<Value> clock;
106 LogicalResult analyzeModule();
109 StringAttr getIndexName(
Object obj, StringAttr name) {
111 obj.first.getType().isInteger(1))
114 return StringAttr::get(name.getContext(),
115 name.getValue() +
"[" + Twine(obj.second) +
"]");
119 void addInput(
Object obj, StringAttr name = {}) {
120 inputs.push_back({obj, getIndexName(obj, name)});
124 void addLatch(
Object current,
Object next, StringAttr name = {}) {
125 latches.push_back({current, getIndexName(current, name), next});
129 void addOutput(
Object obj, StringAttr name = {}) {
130 outputs.push_back({obj, getIndexName(obj, name)});
140 LogicalResult assignLiterals();
143 LogicalResult writeHeader();
144 LogicalResult writeInputs();
145 LogicalResult writeLatches();
146 LogicalResult writeOutputs();
147 LogicalResult writeAndGates();
148 LogicalResult writeSymbolTable();
149 LogicalResult writeComments();
152 LogicalResult visit(Operation *op);
155 LogicalResult visit(aig::AndInverterOp op);
159 LogicalResult visit(comb::ReplicateOp op);
162 unsigned getLiteral(
Object obj,
bool inverted =
false);
165 void writeUnsignedLEB128(
unsigned value);
174LogicalResult AIGERExporter::exportModule() {
175 LLVM_DEBUG(llvm::dbgs() <<
"Starting AIGER export\n");
176 if (failed(analyzeModule()) || failed(writeHeader()) ||
177 failed(writeInputs()) || failed(writeLatches()) ||
178 failed(writeOutputs()) || failed(writeAndGates()) ||
179 failed(writeSymbolTable()) || failed(writeComments()))
182 LLVM_DEBUG(llvm::dbgs() <<
"AIGER export completed successfully\n");
186LogicalResult AIGERExporter::analyzeModule() {
187 LLVM_DEBUG(llvm::dbgs() <<
"Analyzing module\n");
189 auto topModule =
module;
190 LLVM_DEBUG(llvm::dbgs() <<
"Found top module: " << topModule.getModuleName()
194 if (failed(analyzePorts(topModule)))
198 if (failed(analyzeOperations(topModule)))
202 if (failed(assignLiterals()))
205 LLVM_DEBUG(llvm::dbgs() <<
"Analysis complete: M="
206 << getNumInputs() + getNumLatches() + getNumAnds()
207 <<
" I=" << getNumInputs() <<
" L=" << getNumLatches()
208 <<
" O=" << getNumOutputs() <<
" A=" << getNumAnds()
214LogicalResult AIGERExporter::writeHeader() {
215 LLVM_DEBUG(llvm::dbgs() <<
"Writing AIGER header\n");
224 os <<
" " << getNumInputs() + getNumLatches() + getNumAnds() <<
" "
225 << getNumInputs() <<
" " << getNumLatches() <<
" " << getNumOutputs()
226 <<
" " << getNumAnds() <<
"\n";
231LogicalResult AIGERExporter::writeInputs() {
232 LLVM_DEBUG(llvm::dbgs() <<
"Writing inputs\n");
239 for (
auto [input, name] : inputs)
240 os << getLiteral(input) <<
"\n";
245LogicalResult AIGERExporter::writeLatches() {
246 LLVM_DEBUG(llvm::dbgs() <<
"Writing latches\n");
249 for (
auto [current, currentName, next] : latches) {
253 unsigned nextLiteral = getLiteral(next);
257 os << nextLiteral <<
"\n";
259 os << getLiteral(current) <<
" " << nextLiteral <<
"\n";
266LogicalResult AIGERExporter::writeOutputs() {
267 LLVM_DEBUG(llvm::dbgs() <<
"Writing outputs\n");
270 for (
auto [output, _] : outputs)
271 os << getLiteral(output) <<
"\n";
276LogicalResult AIGERExporter::writeAndGates() {
277 LLVM_DEBUG(llvm::dbgs() <<
"Writing AND gates\n");
281 for (
auto [lhs, rhs0, rhs1] : andGates) {
282 unsigned lhsLiteral = getLiteral(lhs);
285 auto andInvOp = lhs.first.getDefiningOp<aig::AndInverterOp>();
286 assert(andInvOp && andInvOp.getInputs().size() == 2);
289 bool rhs0Inverted = andInvOp.getInverted()[0];
290 bool rhs1Inverted = andInvOp.getInverted()[1];
292 unsigned rhs0Literal = getLiteral(rhs0, rhs0Inverted);
293 unsigned rhs1Literal = getLiteral(rhs1, rhs1Inverted);
296 if (rhs0Literal < rhs1Literal) {
297 std::swap(rhs0Literal, rhs1Literal);
298 std::swap(rhs0, rhs1);
299 std::swap(rhs0Inverted, rhs1Inverted);
305 unsigned delta0 = lhsLiteral - rhs0Literal;
306 unsigned delta1 = rhs0Literal - rhs1Literal;
308 LLVM_DEBUG(llvm::dbgs()
309 <<
"Writing AND gate: " << lhsLiteral <<
" = " << rhs0Literal
310 <<
" & " << rhs1Literal <<
" (deltas: " << delta0 <<
", "
312 assert(lhsLiteral >= rhs0Literal &&
"lhsLiteral >= rhs0Literal");
313 assert(rhs0Literal >= rhs1Literal &&
"rhs0Literal >= rhs1Literal");
316 writeUnsignedLEB128(delta0);
317 writeUnsignedLEB128(delta1);
321 for (
auto [lhs, rhs0, rhs1] : andGates) {
322 unsigned lhsLiteral = getLiteral(lhs);
325 auto andInvOp = lhs.first.getDefiningOp<aig::AndInverterOp>();
327 assert(andInvOp && andInvOp.getInputs().size() == 2);
330 bool rhs0Inverted = andInvOp.getInverted()[0];
331 bool rhs1Inverted = andInvOp.getInverted()[1];
333 unsigned rhs0Literal = getLiteral(rhs0, rhs0Inverted);
334 unsigned rhs1Literal = getLiteral(rhs1, rhs1Inverted);
336 os << lhsLiteral <<
" " << rhs0Literal <<
" " << rhs1Literal <<
"\n";
343LogicalResult AIGERExporter::writeSymbolTable() {
344 LLVM_DEBUG(llvm::dbgs() <<
"Writing symbol table\n");
349 for (
auto [index, elem] :
llvm::enumerate(inputs)) {
350 auto [obj, name] = elem;
354 os <<
"i" << index <<
" " << name.getValue() <<
"\n";
357 for (
auto [index, elem] :
llvm::enumerate(latches)) {
358 auto [current, currentName, next] = elem;
362 os <<
"l" << index <<
" " << currentName.getValue() <<
"\n";
365 for (
auto [index, elem] :
llvm::enumerate(outputs)) {
366 auto [obj, name] = elem;
370 os <<
"o" << index <<
" " << name.getValue() <<
"\n";
376LogicalResult AIGERExporter::writeComments() {
377 LLVM_DEBUG(llvm::dbgs() <<
"Writing comments\n");
382 os <<
"module: " <<
module.getModuleName() << "\n";
387unsigned AIGERExporter::getLiteral(
Object obj,
bool inverted) {
389 obj = valueEquivalence.getOrInsertLeaderValue(obj);
392 auto value = obj.first;
393 auto pos = obj.second;
395 auto it = valueLiteralMap.find({value, pos});
396 if (it != valueLiteralMap.end()) {
397 unsigned literal = it->second;
398 return inverted ? literal ^ 1 : literal;
403 APInt constValue = constOp.getValue();
404 if (constValue[obj.second])
406 return inverted ? 0 : 1;
408 return inverted ? 1 : 0;
412 if (
auto andInvOp = value.getDefiningOp<aig::AndInverterOp>()) {
413 if (andInvOp.getInputs().size() == 1) {
415 Value input = andInvOp.getInputs()[0];
416 bool inputInverted = andInvOp.getInverted()[0];
417 unsigned inputLiteral = getLiteral({input, pos}, inputInverted);
419 valueLiteralMap[{value, pos}] = inputLiteral;
420 return inverted ? inputLiteral ^ 1 : inputLiteral;
425 assert((!isa_and_nonnull<comb::ConcatOp, comb::ExtractOp, comb::ReplicateOp>(
426 value.getDefiningOp())) &&
427 "Unhandled operation type");
430 auto it = valueLiteralMap.find({value, pos});
431 if (it != valueLiteralMap.end()) {
432 unsigned literal = it->second;
433 return inverted ? literal ^ 1 : literal;
436 llvm::errs() <<
"Unhandled: Value not found in literal map: " << value <<
"["
440 assert(
false &&
"Value not found in literal map");
443LogicalResult AIGERExporter::analyzePorts(
hw::HWModuleOp hwModule) {
444 LLVM_DEBUG(llvm::dbgs() <<
"Analyzing module ports\n");
446 auto inputNames = hwModule.getInputNames();
447 auto outputNames = hwModule.getOutputNames();
450 for (
auto [index, arg] :
453 if (!arg.getType().isInteger())
458 if (!handler || handler->
valueCallback(arg, i, inputs.size()))
460 llvm::dyn_cast_or_null<StringAttr>(inputNames[index]));
463 LLVM_DEBUG(llvm::dbgs() <<
" Input " << index <<
": " << arg <<
"\n");
467 auto *outputOp = hwModule.getBodyBlock()->getTerminator();
468 for (
auto [operand, name] :
469 llvm::zip(outputOp->getOpOperands(), outputNames)) {
470 for (int64_t i = 0; i <
getBitWidth(operand.get()); ++i)
472 addOutput({operand.get(), i}, llvm::dyn_cast_or_null<StringAttr>(name));
473 LLVM_DEBUG(llvm::dbgs() <<
" Output: " << operand.get() <<
"\n");
476 LLVM_DEBUG(llvm::dbgs() <<
"Found " << getNumInputs() <<
" inputs, "
477 << getNumOutputs() <<
" outputs from ports\n");
481LogicalResult AIGERExporter::analyzeOperations(
hw::HWModuleOp hwModule) {
482 LLVM_DEBUG(llvm::dbgs() <<
"Analyzing operations\n");
485 auto result = hwModule.walk([&](Region *region) {
486 auto regionKindOp = dyn_cast<RegionKindInterface>(region->getParentOp());
488 regionKindOp.hasSSADominance(region->getRegionNumber()))
489 return WalkResult::advance();
492 for (
auto &block : *region) {
493 if (!sortTopologically(&block, [&](Value value, Operation *op) {
499 return WalkResult::interrupt();
501 return WalkResult::advance();
504 if (result.wasInterrupted())
505 return mlir::emitError(hwModule.getLoc(),
506 "failed to sort operations topologically");
509 for (Operation &op : hwModule.
getBodyBlock()->getOperations()) {
510 if (failed(visit(&op)))
514 LLVM_DEBUG(llvm::dbgs() <<
"Found " << getNumAnds() <<
" AND gates, "
515 << getNumLatches() <<
" latches\n");
519LogicalResult AIGERExporter::visit(Operation *op) {
520 return TypeSwitch<Operation *, LogicalResult>(op)
521 .Case<aig::AndInverterOp>([&](
auto op) {
return visit(op); })
522 .Case<seq::CompRegOp>([&](
auto op) {
return visit(op); })
523 .Case<comb::ConcatOp>([&](
auto op) {
return visit(op); })
524 .Case<comb::ExtractOp>([&](
auto op) {
return visit(op); })
525 .Case<comb::ReplicateOp>([&](
auto op) {
return visit(op); })
526 .Case<hw::HWModuleOp, hw::ConstantOp, hw::OutputOp>(
527 [](
auto) {
return success(); })
528 .Default([&](Operation *op) -> LogicalResult {
531 return mlir::emitError(op->getLoc(),
"unhandled operation: ") << *op;
534 for (mlir::OpOperand &operand : op->getOpOperands()) {
535 if (operand.get().getType().isInteger())
536 for (int64_t i = 0; i <
getBitWidth(operand.get()); ++i) {
538 addOutput({operand.get(), i});
542 for (mlir::OpResult result : op->getOpResults()) {
543 if (!result.getType().isInteger())
545 for (int64_t i = 0; i <
getBitWidth(result); ++i) {
547 addInput({result, i});
550 valueLiteralMap[{result, i}] = 0;
558LogicalResult AIGERExporter::visit(aig::AndInverterOp op) {
560 if (op.getInputs().size() == 1) {
563 LLVM_DEBUG(llvm::dbgs() <<
" Found inverter: " << op <<
"\n");
564 }
else if (op.getInputs().size() == 2) {
567 andGates.push_back({{op.getResult(), i},
568 {op.getInputs()[0], i},
569 {op.getInputs()[1], i}});
571 LLVM_DEBUG(llvm::dbgs() <<
" Found AND gate: " << op <<
"\n");
574 return mlir::emitError(op->getLoc(),
575 "variadic AND gates not supported, run "
576 "aig-lower-variadic pass first");
586 addLatch({op.getResult(), i}, {op.getInput(), i}, op.getNameAttr());
588 LLVM_DEBUG(llvm::dbgs() <<
" Found latch: " << op <<
"\n");
596 for (
auto operand :
llvm::reverse(op.getInputs()))
597 for (int64_t i = 0, e =
getBitWidth(operand); i < e; ++i)
598 valueEquivalence.unionSets({operand, i}, {op.getResult(), pos++});
603 for (int64_t i = 0, e =
getBitWidth(op); i < e; ++i)
604 valueEquivalence.unionSets({op.getInput(), op.getLowBit() + i},
605 {op.getResult(), i});
609LogicalResult AIGERExporter::visit(comb::ReplicateOp op) {
611 for (int64_t i = 0, e =
getBitWidth(op); i < e; ++i)
612 valueEquivalence.unionSets({op.getInput(), i % operandWidth},
613 {op.getResult(), i});
618 const AIGERExporter::Object &obj) {
619 return os << obj.first <<
"[" << obj.second <<
"]";
624 const std::pair<AIGERExporter::Object, StringAttr> &obj) {
625 return os << obj.first
626 << (obj.second ?
" (" + obj.second.getValue() +
")" :
"");
622llvm::raw_ostream & {
…}
629LogicalResult AIGERExporter::assignLiterals() {
630 LLVM_DEBUG(llvm::dbgs() <<
"Assigning literals\n");
632 unsigned nextLiteral =
636 for (
auto input : inputs) {
637 valueLiteralMap[input.first] = nextLiteral;
638 LLVM_DEBUG(llvm::dbgs()
639 <<
" Input literal " << nextLiteral <<
": " << input <<
"\n");
644 for (
auto [current, currentName, next] : latches) {
645 valueLiteralMap[current] = nextLiteral;
646 LLVM_DEBUG(llvm::dbgs()
647 <<
" Latch literal " << nextLiteral <<
": " << current <<
"\n");
649 auto clocked = current.first.getDefiningOp<seq::Clocked>();
652 clock = clocked.getClk();
653 else if (clock != clocked.getClk()) {
654 auto diag = mlir::emitError(clocked.getClk().getLoc(),
655 "multiple clocks found in the module");
656 diag.attachNote(clock->getLoc()) <<
"previous clock is here";
661 if (clock && handler)
664 for (
auto [lhs, rhs0, rhs1] : andGates) {
665 valueLiteralMap[lhs] = nextLiteral;
666 LLVM_DEBUG(llvm::dbgs()
667 <<
" AND gate literal " << nextLiteral <<
": " << lhs <<
"\n");
671 LLVM_DEBUG(llvm::dbgs() <<
"Assigned " << valueLiteralMap.size()
681 llvm::raw_ostream &os,
686 options = &defaultOptions;
688 AIGERExporter exporter(module, os, *options, handler);
689 return exporter.exportModule();
694 llvm::cl::desc(
"Export AIGER in text format"),
695 llvm::cl::init(
false));
699 llvm::cl::desc(
"Exclude symbol table from the output"),
700 llvm::cl::init(
false));
703 static mlir::TranslateFromMLIRRegistration toAIGER(
704 "export-aiger",
"Export AIG to AIGER format",
705 [](mlir::ModuleOp module, llvm::raw_ostream &os) -> LogicalResult {
706 auto ops =
module.getOps<hw::HWModuleOp>();
708 return module.emitError(
"no HW module found in the input");
709 if (std::next(ops.begin()) != ops.end())
710 return module.emitError(
711 "multiple HW modules found, expected single top module");
719 [](DialectRegistry ®istry) {
720 registry.insert<aig::AIGDialect, hw::HWDialect, seq::SeqDialect,
721 comb::CombDialect>();
726void AIGERExporter::writeUnsignedLEB128(
unsigned value) {
728 uint8_t
byte = value & 0x7f;
732 os.write(
reinterpret_cast<char *
>(&
byte), 1);
733 }
while (value != 0);
assert(baseType &&"element must be base type")
llvm::cl::opt< bool > includeSymbolTable("exclude-symbol-table", llvm::cl::desc("Exclude symbol table from the output"), llvm::cl::init(false))
llvm::cl::opt< bool > emitTextFormat("emit-text-format", llvm::cl::desc("Export AIGER in text format"), llvm::cl::init(false))
static Block * getBodyBlock(FModuleLike mod)
mlir::LogicalResult exportAIGER(hw::HWModuleOp module, llvm::raw_ostream &os, const ExportAIGEROptions *options=nullptr, ExportAIGERHandler *handler=nullptr)
Export an MLIR module containing AIG dialect operations to AIGER format.
void registerExportAIGERTranslation()
Register the export-aiger MLIR translation.
OS & operator<<(OS &os, const InnerSymTarget &target)
Printing InnerSymTarget's.
int64_t getBitWidth(mlir::Type type)
Return the hardware bit width of a type.
The InstanceGraph op interface, see InstanceGraphInterface.td for more details.
const char * getCirctVersion()
Handler for AIGER export.
virtual bool valueCallback(Value result, size_t bitPos, size_t inputIndex)
virtual void notifyClock(Value value)
virtual bool operandCallback(mlir::OpOperand &operand, size_t bitPos, size_t outputIndex)
virtual void notifyEmitted(Operation *op)
Options for AIGER export.
bool includeSymbolTable
Whether to include symbol table in the output.
bool binaryFormat
Whether to export in binary format (aig) or ASCII format (aag).