Loading [MathJax]/jax/output/HTML-CSS/config.js
CIRCT 22.0.0git
All Classes Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros Pages
ExportAIGER.cpp
Go to the documentation of this file.
1//===----------------------------------------------------------------------===//
2//
3// Part of the LLVM Project, under the Apache License v2.0 with LLVM Exceptions.
4// See https://llvm.org/LICENSE.txt for license information.
5// SPDX-License-Identifier: Apache-2.0 WITH LLVM-exception
6//
7//===----------------------------------------------------------------------===//
8//
9// This file implements the AIGER file export functionality. AIGER is a format
10// for representing sequential circuits as AIGs (And-Inverter Graphs). This
11// implementation supports both ASCII and binary AIGER formats.
12//
13//===----------------------------------------------------------------------===//
14
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"
40#include <string>
41
42using namespace mlir;
43using namespace circt;
44using namespace circt::hw;
45using namespace circt::aig;
46using namespace circt::seq;
47using namespace circt::aiger;
48
49#define DEBUG_TYPE "export-aiger"
50
51//===----------------------------------------------------------------------===//
52// Helper Functions
53//===----------------------------------------------------------------------===//
54
55/// Returns the bit width of a value.
56static int64_t getBitWidth(Value value) {
57 return hw::getBitWidth(value.getType());
58}
59
60//===----------------------------------------------------------------------===//
61// AIGERExporter Implementation
62//===----------------------------------------------------------------------===//
63
64namespace {
65
66/// Main AIGER exporter class that handles the conversion of MLIR modules to
67/// AIGER format. This class manages the state and provides methods for
68/// analyzing the module and writing the AIGER file.
69class AIGERExporter {
70public:
71 AIGERExporter(hw::HWModuleOp module, llvm::raw_ostream &os,
72 const ExportAIGEROptions &options, ExportAIGERHandler *handler)
73 : module(module), os(os), options(options), handler(handler) {}
74
75 /// Export the module to AIGER format.
76 LogicalResult exportModule();
77
78 // Data type for tracking values and their bit positions
79 using Object = std::pair<Value, int>;
80
81private:
82 hw::HWModuleOp module;
83 llvm::raw_ostream &os;
84 const ExportAIGEROptions &options;
85 ExportAIGERHandler *handler;
86
87 // Map of values to their literals
88 DenseMap<Object, unsigned> valueLiteralMap;
89
90 // AIGER file data
91 unsigned getNumInputs() { return inputs.size(); }
92 unsigned getNumLatches() { return latches.size(); }
93 unsigned getNumOutputs() { return outputs.size(); }
94 unsigned getNumAnds() { return andGates.size(); }
95
96 llvm::EquivalenceClasses<Object> valueEquivalence;
97 SmallVector<std::pair<Object, StringAttr>> inputs;
98 SmallVector<std::tuple<Object, StringAttr, Object>>
99 latches; // current, name, next
100 SmallVector<std::pair<Object, StringAttr>> outputs;
101 SmallVector<std::tuple<Object, Object, Object>> andGates; // lhs, rhs0, rhs1
102
103 std::optional<Value> clock;
104
105 /// Analyze the module and collect information
106 LogicalResult analyzeModule();
107
108 /// Get the index name for an object, handling bit positions
109 StringAttr getIndexName(Object obj, StringAttr name) {
110 if (!options.includeSymbolTable || !name || name.getValue().empty() ||
111 obj.first.getType().isInteger(1))
112 return name;
113
114 return StringAttr::get(name.getContext(),
115 name.getValue() + "[" + Twine(obj.second) + "]");
116 }
117
118 /// Add an input to the AIGER file
119 void addInput(Object obj, StringAttr name = {}) {
120 inputs.push_back({obj, getIndexName(obj, name)});
121 }
122
123 /// Add a latch to the AIGER file
124 void addLatch(Object current, Object next, StringAttr name = {}) {
125 latches.push_back({current, getIndexName(current, name), next});
126 }
127
128 /// Add an output to the AIGER file
129 void addOutput(Object obj, StringAttr name = {}) {
130 outputs.push_back({obj, getIndexName(obj, name)});
131 }
132
133 /// Analyze module ports (inputs/outputs)
134 LogicalResult analyzePorts(hw::HWModuleOp module);
135
136 /// Analyze operations in the module
137 LogicalResult analyzeOperations(hw::HWModuleOp module);
138
139 /// Assign literals to all values
140 LogicalResult assignLiterals();
141
142 /// Writers
143 LogicalResult writeHeader();
144 LogicalResult writeInputs();
145 LogicalResult writeLatches();
146 LogicalResult writeOutputs();
147 LogicalResult writeAndGates();
148 LogicalResult writeSymbolTable();
149 LogicalResult writeComments();
150
151 /// Visit an operation and process it
152 LogicalResult visit(Operation *op);
153
154 /// Visit specific operation types
155 LogicalResult visit(aig::AndInverterOp op);
156 LogicalResult visit(seq::CompRegOp op);
157 LogicalResult visit(comb::ConcatOp op);
158 LogicalResult visit(comb::ExtractOp op);
159 LogicalResult visit(comb::ReplicateOp op);
160
161 /// Get or assign a literal for a value
162 unsigned getLiteral(Object obj, bool inverted = false);
163
164 /// Helper method to write unsigned LEB128 encoded integers
165 void writeUnsignedLEB128(unsigned value);
166};
167
168} // anonymous namespace
169
170//===----------------------------------------------------------------------===//
171// AIGERExporter Implementation
172//===----------------------------------------------------------------------===//
173
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()))
180 return failure();
181
182 LLVM_DEBUG(llvm::dbgs() << "AIGER export completed successfully\n");
183 return success();
184}
185
186LogicalResult AIGERExporter::analyzeModule() {
187 LLVM_DEBUG(llvm::dbgs() << "Analyzing module\n");
188
189 auto topModule = module;
190 LLVM_DEBUG(llvm::dbgs() << "Found top module: " << topModule.getModuleName()
191 << "\n");
192
193 // Analyze module ports
194 if (failed(analyzePorts(topModule)))
195 return failure();
196
197 // Walk through all operations in the module body
198 if (failed(analyzeOperations(topModule)))
199 return failure();
200
201 // Assign literals to all values
202 if (failed(assignLiterals()))
203 return failure();
204
205 LLVM_DEBUG(llvm::dbgs() << "Analysis complete: M="
206 << getNumInputs() + getNumLatches() + getNumAnds()
207 << " I=" << getNumInputs() << " L=" << getNumLatches()
208 << " O=" << getNumOutputs() << " A=" << getNumAnds()
209 << "\n");
210
211 return success();
212}
213
214LogicalResult AIGERExporter::writeHeader() {
215 LLVM_DEBUG(llvm::dbgs() << "Writing AIGER header\n");
216
217 // Write format identifier
218 if (options.binaryFormat)
219 os << "aig";
220 else
221 os << "aag";
222
223 // Write M I L O A
224 os << " " << getNumInputs() + getNumLatches() + getNumAnds() << " "
225 << getNumInputs() << " " << getNumLatches() << " " << getNumOutputs()
226 << " " << getNumAnds() << "\n";
227
228 return success();
229}
230
231LogicalResult AIGERExporter::writeInputs() {
232 LLVM_DEBUG(llvm::dbgs() << "Writing inputs\n");
233
234 if (options.binaryFormat)
235 // In binary format, inputs are implicit
236 return success();
237
238 // Write input literals
239 for (auto [input, name] : inputs)
240 os << getLiteral(input) << "\n";
241
242 return success();
243}
244
245LogicalResult AIGERExporter::writeLatches() {
246 LLVM_DEBUG(llvm::dbgs() << "Writing latches\n");
247
248 // Write latch definitions
249 for (auto [current, currentName, next] : latches) {
250
251 // For next state, we need to handle potential inversions
252 // Check if next state comes from an inverter or has inversions
253 unsigned nextLiteral = getLiteral(next);
254
255 if (options.binaryFormat) {
256 // In binary format, current literal is not needed
257 os << nextLiteral << "\n";
258 } else {
259 os << getLiteral(current) << " " << nextLiteral << "\n";
260 }
261 }
262
263 return success();
264}
265
266LogicalResult AIGERExporter::writeOutputs() {
267 LLVM_DEBUG(llvm::dbgs() << "Writing outputs\n");
268
269 // Write output literals
270 for (auto [output, _] : outputs)
271 os << getLiteral(output) << "\n";
272
273 return success();
274}
275
276LogicalResult AIGERExporter::writeAndGates() {
277 LLVM_DEBUG(llvm::dbgs() << "Writing AND gates\n");
278
279 if (options.binaryFormat) {
280 // Implement binary format encoding for AND gates
281 for (auto [lhs, rhs0, rhs1] : andGates) {
282 unsigned lhsLiteral = getLiteral(lhs);
283
284 // Get the AND-inverter operation to check inversion flags
285 auto andInvOp = lhs.first.getDefiningOp<aig::AndInverterOp>();
286 assert(andInvOp && andInvOp.getInputs().size() == 2);
287
288 // Get operand literals with inversion
289 bool rhs0Inverted = andInvOp.getInverted()[0];
290 bool rhs1Inverted = andInvOp.getInverted()[1];
291
292 unsigned rhs0Literal = getLiteral(rhs0, rhs0Inverted);
293 unsigned rhs1Literal = getLiteral(rhs1, rhs1Inverted);
294
295 // Ensure rhs0 >= rhs1 as required by AIGER format
296 if (rhs0Literal < rhs1Literal) {
297 std::swap(rhs0Literal, rhs1Literal);
298 std::swap(rhs0, rhs1);
299 std::swap(rhs0Inverted, rhs1Inverted);
300 }
301
302 // In binary format, we need to write the delta values
303 // Delta0 = lhs - rhs0
304 // Delta1 = rhs0 - rhs1
305 unsigned delta0 = lhsLiteral - rhs0Literal;
306 unsigned delta1 = rhs0Literal - rhs1Literal;
307
308 LLVM_DEBUG(llvm::dbgs()
309 << "Writing AND gate: " << lhsLiteral << " = " << rhs0Literal
310 << " & " << rhs1Literal << " (deltas: " << delta0 << ", "
311 << delta1 << ")\n");
312 assert(lhsLiteral >= rhs0Literal && "lhsLiteral >= rhs0Literal");
313 assert(rhs0Literal >= rhs1Literal && "rhs0Literal >= rhs1Literal");
314
315 // Write deltas using variable-length encoding
316 writeUnsignedLEB128(delta0);
317 writeUnsignedLEB128(delta1);
318 }
319 } else {
320 // ASCII format - no need for structural hashing
321 for (auto [lhs, rhs0, rhs1] : andGates) {
322 unsigned lhsLiteral = getLiteral(lhs);
323
324 // Get the AND-inverter operation to check inversion flags
325 auto andInvOp = lhs.first.getDefiningOp<aig::AndInverterOp>();
326
327 assert(andInvOp && andInvOp.getInputs().size() == 2);
328
329 // Get operand literals with inversion
330 bool rhs0Inverted = andInvOp.getInverted()[0];
331 bool rhs1Inverted = andInvOp.getInverted()[1];
332
333 unsigned rhs0Literal = getLiteral(rhs0, rhs0Inverted);
334 unsigned rhs1Literal = getLiteral(rhs1, rhs1Inverted);
335
336 os << lhsLiteral << " " << rhs0Literal << " " << rhs1Literal << "\n";
337 }
338 }
339
340 return success();
341}
342
343LogicalResult AIGERExporter::writeSymbolTable() {
344 LLVM_DEBUG(llvm::dbgs() << "Writing symbol table\n");
345
346 if (!options.includeSymbolTable)
347 return success();
348
349 for (auto [index, elem] : llvm::enumerate(inputs)) {
350 auto [obj, name] = elem;
351 // Don't write inputs without a name
352 if (!name)
353 continue;
354 os << "i" << index << " " << name.getValue() << "\n";
355 }
356
357 for (auto [index, elem] : llvm::enumerate(latches)) {
358 auto [current, currentName, next] = elem;
359 // Don't write latches without a name
360 if (!currentName)
361 continue;
362 os << "l" << index << " " << currentName.getValue() << "\n";
363 }
364
365 for (auto [index, elem] : llvm::enumerate(outputs)) {
366 auto [obj, name] = elem;
367 // Don't write outputs without a name
368 if (!name)
369 continue;
370 os << "o" << index << " " << name.getValue() << "\n";
371 }
372
373 return success();
374}
375
376LogicalResult AIGERExporter::writeComments() {
377 LLVM_DEBUG(llvm::dbgs() << "Writing comments\n");
378
379 // Write comment section
380 os << "c\n";
381 os << "Generated by " << circt::getCirctVersion() << "\n";
382 os << "module: " << module.getModuleName() << "\n";
383
384 return success();
385}
386
387unsigned AIGERExporter::getLiteral(Object obj, bool inverted) {
388 // Get the leader value from the equivalence class
389 obj = valueEquivalence.getOrInsertLeaderValue(obj);
390
391 // Handle constants
392 auto value = obj.first;
393 auto pos = obj.second;
394 {
395 auto it = valueLiteralMap.find({value, pos});
396 if (it != valueLiteralMap.end()) {
397 unsigned literal = it->second;
398 return inverted ? literal ^ 1 : literal;
399 }
400 }
401
402 if (auto constOp = value.getDefiningOp<hw::ConstantOp>()) {
403 APInt constValue = constOp.getValue();
404 if (constValue[obj.second])
405 // TRUE constant = literal 1, inverted = literal 0 (FALSE)
406 return inverted ? 0 : 1;
407 // FALSE constant = literal 0, inverted = literal 1 (TRUE)
408 return inverted ? 1 : 0;
409 }
410
411 // Handle single-input AND-inverter (pure inverter)
412 if (auto andInvOp = value.getDefiningOp<aig::AndInverterOp>()) {
413 if (andInvOp.getInputs().size() == 1) {
414 // This is a pure inverter - we need to find the input's literal
415 Value input = andInvOp.getInputs()[0];
416 bool inputInverted = andInvOp.getInverted()[0];
417 unsigned inputLiteral = getLiteral({input, pos}, inputInverted);
418 // Apply additional inversion if requested
419 valueLiteralMap[{value, pos}] = inputLiteral;
420 return inverted ? inputLiteral ^ 1 : inputLiteral;
421 }
422 }
423
424 // Concatenation, replication, and extraction
425 assert((!isa_and_nonnull<comb::ConcatOp, comb::ExtractOp, comb::ReplicateOp>(
426 value.getDefiningOp())) &&
427 "Unhandled operation type");
428
429 // Look up in the literal map
430 auto it = valueLiteralMap.find({value, pos});
431 if (it != valueLiteralMap.end()) {
432 unsigned literal = it->second;
433 return inverted ? literal ^ 1 : literal;
434 }
435
436 llvm::errs() << "Unhandled: Value not found in literal map: " << value << "["
437 << pos << "]\n";
438
439 // This should not happen if analysis was done correctly
440 assert(false && "Value not found in literal map");
441}
442
443LogicalResult AIGERExporter::analyzePorts(hw::HWModuleOp hwModule) {
444 LLVM_DEBUG(llvm::dbgs() << "Analyzing module ports\n");
445
446 auto inputNames = hwModule.getInputNames();
447 auto outputNames = hwModule.getOutputNames();
448
449 // Analyze input ports
450 for (auto [index, arg] :
451 llvm::enumerate(hwModule.getBodyBlock()->getArguments())) {
452 // Skip non integer inputs.
453 if (!arg.getType().isInteger())
454 continue;
455
456 // All other inputs should be i1 (1-bit assumption)
457 for (int64_t i = 0; i < getBitWidth(arg); ++i) {
458 if (!handler || handler->valueCallback(arg, i, inputs.size()))
459 addInput({arg, i},
460 llvm::dyn_cast_or_null<StringAttr>(inputNames[index]));
461 }
462
463 LLVM_DEBUG(llvm::dbgs() << " Input " << index << ": " << arg << "\n");
464 }
465
466 // Analyze output ports by looking at hw.output operation
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)
471 if (!handler || handler->operandCallback(operand, i, outputs.size()))
472 addOutput({operand.get(), i}, llvm::dyn_cast_or_null<StringAttr>(name));
473 LLVM_DEBUG(llvm::dbgs() << " Output: " << operand.get() << "\n");
474 }
475
476 LLVM_DEBUG(llvm::dbgs() << "Found " << getNumInputs() << " inputs, "
477 << getNumOutputs() << " outputs from ports\n");
478 return success();
479}
480
481LogicalResult AIGERExporter::analyzeOperations(hw::HWModuleOp hwModule) {
482 LLVM_DEBUG(llvm::dbgs() << "Analyzing operations\n");
483
484 // Sort the operations topologically
485 auto result = hwModule.walk([&](Region *region) {
486 auto regionKindOp = dyn_cast<RegionKindInterface>(region->getParentOp());
487 if (!regionKindOp ||
488 regionKindOp.hasSSADominance(region->getRegionNumber()))
489 return WalkResult::advance();
490
491 // Graph region.
492 for (auto &block : *region) {
493 if (!sortTopologically(&block, [&](Value value, Operation *op) {
494 // Topologically sort AND-inverters and purely dataflow ops. Other
495 // operations can be scheduled.
496 return !(isa<aig::AndInverterOp, comb::ExtractOp, comb::ReplicateOp,
497 comb::ConcatOp>(op));
498 }))
499 return WalkResult::interrupt();
500 }
501 return WalkResult::advance();
502 });
503
504 if (result.wasInterrupted())
505 return mlir::emitError(hwModule.getLoc(),
506 "failed to sort operations topologically");
507
508 // Visit each operation in the module
509 for (Operation &op : hwModule.getBodyBlock()->getOperations()) {
510 if (failed(visit(&op)))
511 return failure();
512 }
513
514 LLVM_DEBUG(llvm::dbgs() << "Found " << getNumAnds() << " AND gates, "
515 << getNumLatches() << " latches\n");
516 return success();
517}
518
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 {
529 // Handle unknown operations if handler is set
530 if (!handler)
531 return mlir::emitError(op->getLoc(), "unhandled operation: ") << *op;
532
533 // Handle unknown operations through the handler
534 for (mlir::OpOperand &operand : op->getOpOperands()) {
535 if (operand.get().getType().isInteger())
536 for (int64_t i = 0; i < getBitWidth(operand.get()); ++i) {
537 if (handler->operandCallback(operand, i, outputs.size()))
538 addOutput({operand.get(), i});
539 }
540 }
541
542 for (mlir::OpResult result : op->getOpResults()) {
543 if (!result.getType().isInteger())
544 continue;
545 for (int64_t i = 0; i < getBitWidth(result); ++i) {
546 if (handler->valueCallback(result, i, inputs.size()))
547 addInput({result, i});
548 else
549 // Treat it as a constant
550 valueLiteralMap[{result, i}] = 0;
551 }
552 }
553
554 return success();
555 });
556}
557
558LogicalResult AIGERExporter::visit(aig::AndInverterOp op) {
559 // Handle AIG AND-inverter operations
560 if (op.getInputs().size() == 1) {
561 // Single input = inverter (not counted as AND gate in AIGER)
562 // Inversion flag is looked at in getLiteral()
563 LLVM_DEBUG(llvm::dbgs() << " Found inverter: " << op << "\n");
564 } else if (op.getInputs().size() == 2) {
565 // Two inputs = AND gate
566 for (int64_t i = 0; i < getBitWidth(op); ++i)
567 andGates.push_back({{op.getResult(), i},
568 {op.getInputs()[0], i},
569 {op.getInputs()[1], i}});
570
571 LLVM_DEBUG(llvm::dbgs() << " Found AND gate: " << op << "\n");
572 } else {
573 // Variadic AND gates need to be lowered first
574 return mlir::emitError(op->getLoc(),
575 "variadic AND gates not supported, run "
576 "aig-lower-variadic pass first");
577 }
578 if (handler)
579 handler->notifyEmitted(op);
580 return success();
581}
582
583LogicalResult AIGERExporter::visit(seq::CompRegOp op) {
584 // Handle registers (latches in AIGER)
585 for (int64_t i = 0; i < getBitWidth(op); ++i)
586 addLatch({op.getResult(), i}, {op.getInput(), i}, op.getNameAttr());
587
588 LLVM_DEBUG(llvm::dbgs() << " Found latch: " << op << "\n");
589 if (handler)
590 handler->notifyEmitted(op);
591 return success();
592}
593
594LogicalResult AIGERExporter::visit(comb::ConcatOp op) {
595 size_t pos = 0;
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++});
599 return success();
600}
601
602LogicalResult AIGERExporter::visit(comb::ExtractOp op) {
603 for (int64_t i = 0, e = getBitWidth(op); i < e; ++i)
604 valueEquivalence.unionSets({op.getInput(), op.getLowBit() + i},
605 {op.getResult(), i});
606 return success();
607}
608
609LogicalResult AIGERExporter::visit(comb::ReplicateOp op) {
610 auto operandWidth = getBitWidth(op.getInput());
611 for (int64_t i = 0, e = getBitWidth(op); i < e; ++i)
612 valueEquivalence.unionSets({op.getInput(), i % operandWidth},
613 {op.getResult(), i});
614 return success();
615}
616
617llvm::raw_ostream &operator<<(llvm::raw_ostream &os,
618 const AIGERExporter::Object &obj) {
619 return os << obj.first << "[" << obj.second << "]";
620}
621
622llvm::raw_ostream &
623operator<<(llvm::raw_ostream &os,
624 const std::pair<AIGERExporter::Object, StringAttr> &obj) {
625 return os << obj.first
626 << (obj.second ? " (" + obj.second.getValue() + ")" : "");
627}
628
629LogicalResult AIGERExporter::assignLiterals() {
630 LLVM_DEBUG(llvm::dbgs() << "Assigning literals\n");
631
632 unsigned nextLiteral =
633 2; // Start from 2 (literal 0 = FALSE, literal 1 = TRUE)
634
635 // Assign literals to inputs first
636 for (auto input : inputs) {
637 valueLiteralMap[input.first] = nextLiteral;
638 LLVM_DEBUG(llvm::dbgs()
639 << " Input literal " << nextLiteral << ": " << input << "\n");
640 nextLiteral += 2; // Even literals only (odd = inverted)
641 }
642
643 // Assign literals to latches (current state)
644 for (auto [current, currentName, next] : latches) {
645 valueLiteralMap[current] = nextLiteral;
646 LLVM_DEBUG(llvm::dbgs()
647 << " Latch literal " << nextLiteral << ": " << current << "\n");
648 nextLiteral += 2;
649 auto clocked = current.first.getDefiningOp<seq::Clocked>();
650 assert(clocked);
651 if (!clock)
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";
657 return diag;
658 }
659 }
660
661 if (clock && handler)
662 handler->notifyClock(*clock);
663
664 for (auto [lhs, rhs0, rhs1] : andGates) {
665 valueLiteralMap[lhs] = nextLiteral;
666 LLVM_DEBUG(llvm::dbgs()
667 << " AND gate literal " << nextLiteral << ": " << lhs << "\n");
668 nextLiteral += 2;
669 }
670
671 LLVM_DEBUG(llvm::dbgs() << "Assigned " << valueLiteralMap.size()
672 << " literals\n");
673 return success();
674}
675
676//===----------------------------------------------------------------------===//
677// Public API Implementation
678//===----------------------------------------------------------------------===//
679
681 llvm::raw_ostream &os,
682 const ExportAIGEROptions *options,
683 ExportAIGERHandler *handler) {
684 ExportAIGEROptions defaultOptions;
685 if (!options)
686 options = &defaultOptions;
687
688 AIGERExporter exporter(module, os, *options, handler);
689 return exporter.exportModule();
690}
691
693 emitTextFormat("emit-text-format",
694 llvm::cl::desc("Export AIGER in text format"),
695 llvm::cl::init(false));
696
698 includeSymbolTable("exclude-symbol-table",
699 llvm::cl::desc("Exclude symbol table from the output"),
700 llvm::cl::init(false));
701
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>();
707 if (ops.empty())
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");
712
713 ExportAIGEROptions options;
714 options.binaryFormat = !emitTextFormat;
716
717 return exportAIGER(*ops.begin(), os, &options);
718 },
719 [](DialectRegistry &registry) {
720 registry.insert<aig::AIGDialect, hw::HWDialect, seq::SeqDialect,
721 comb::CombDialect>();
722 });
723}
724
725// Helper method to write unsigned LEB128 encoded integers
726void AIGERExporter::writeUnsignedLEB128(unsigned value) {
727 do {
728 uint8_t byte = value & 0x7f;
729 value >>= 7;
730 if (value != 0)
731 byte |= 0x80; // Set high bit if more bytes follow
732 os.write(reinterpret_cast<char *>(&byte), 1);
733 } while (value != 0);
734}
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.
Definition HWTypes.cpp:110
The InstanceGraph op interface, see InstanceGraphInterface.td for more details.
const char * getCirctVersion()
Handler for AIGER export.
Definition ExportAIGER.h:35
virtual bool valueCallback(Value result, size_t bitPos, size_t inputIndex)
Definition ExportAIGER.h:51
virtual void notifyClock(Value value)
Definition ExportAIGER.h:59
virtual bool operandCallback(mlir::OpOperand &operand, size_t bitPos, size_t outputIndex)
Definition ExportAIGER.h:43
virtual void notifyEmitted(Operation *op)
Definition ExportAIGER.h:56
Options for AIGER export.
Definition ExportAIGER.h:63
bool includeSymbolTable
Whether to include symbol table in the output.
Definition ExportAIGER.h:70
bool binaryFormat
Whether to export in binary format (aig) or ASCII format (aag).
Definition ExportAIGER.h:66