mirror of https://github.com/llvm/circt.git
[AIG][AIGER] Add AIGER Importer (#8567)
This commit implements a complete AIGER parser that supports both ASCII (.aag) and binary (.aig) formats following the AIGER format specification from https://fmv.jku.at/aiger/FORMAT.aiger. AIGER is a popular format widely used by the ABC synthesis tool and serves as a standard for logic synthesis benchmarks, making it essential for integrating with efficient solvers and verification tools. The parser handles all core AIGER components including inputs, latches, outputs, and AND gates, with support for binary format delta compression for AND gates. It parses optional symbol tables and comments sections, creating MLIR modules using HW, AIG, and Seq dialects with BackedgeBuilder for handling forward references.
This commit is contained in:
Hideto Ueno
GitHub
parent
6070285643
commit
3418d7d242
|
|
@ -0,0 +1,48 @@
|
|||
//===----------------------------------------------------------------------===//
|
||||
//
|
||||
// Part of the LLVM Project, under the Apache License v2.0 with LLVM Exceptions.
|
||||
// See https://llvm.org/LICENSE.txt for license information.
|
||||
// SPDX-License-Identifier: Apache-2.0 WITH LLVM-exception
|
||||
//
|
||||
//===----------------------------------------------------------------------===//
|
||||
//
|
||||
// This file defines the interface for importing AIGER files.
|
||||
//
|
||||
//===----------------------------------------------------------------------===//
|
||||
|
||||
#ifndef CIRCT_CONVERSION_IMPORTAIGER_H
|
||||
#define CIRCT_CONVERSION_IMPORTAIGER_H
|
||||
|
||||
#include "circt/Support/LLVM.h"
|
||||
#include "mlir/IR/BuiltinOps.h"
|
||||
#include "llvm/Support/SourceMgr.h"
|
||||
|
||||
namespace mlir {
|
||||
class MLIRContext;
|
||||
class TimingScope;
|
||||
} // namespace mlir
|
||||
|
||||
namespace circt {
|
||||
namespace aiger {
|
||||
|
||||
/// Options for AIGER import.
|
||||
struct ImportAIGEROptions {
|
||||
/// The name to use for the top-level module. If empty, a default name
|
||||
/// will be generated.
|
||||
std::string topLevelModule = "aiger_top";
|
||||
};
|
||||
|
||||
/// Parse an AIGER file and populate the given MLIR module with corresponding
|
||||
/// AIG dialect operations.
|
||||
mlir::LogicalResult importAIGER(llvm::SourceMgr &sourceMgr,
|
||||
mlir::MLIRContext *context,
|
||||
mlir::TimingScope &ts, mlir::ModuleOp module,
|
||||
const ImportAIGEROptions *options = nullptr);
|
||||
|
||||
/// Register the `import-aiger` MLIR translation.
|
||||
void registerImportAIGERTranslation();
|
||||
} // namespace aiger
|
||||
|
||||
} // namespace circt
|
||||
|
||||
#endif // CIRCT_CONVERSION_IMPORTAIGER_H
|
||||
|
|
@ -37,6 +37,7 @@
|
|||
#include "circt/Conversion/HWToSystemC.h"
|
||||
#include "circt/Conversion/HandshakeToDC.h"
|
||||
#include "circt/Conversion/HandshakeToHW.h"
|
||||
#include "circt/Conversion/ImportAIGER.h"
|
||||
#include "circt/Conversion/LTLToCore.h"
|
||||
#include "circt/Conversion/LoopScheduleToCalyx.h"
|
||||
#include "circt/Conversion/MooreToCore.h"
|
||||
|
|
|
|||
|
|
@ -11,6 +11,7 @@
|
|||
//
|
||||
//===----------------------------------------------------------------------===//
|
||||
|
||||
#include "circt/Conversion/ImportAIGER.h"
|
||||
#include "circt/Dialect/Arc/ModelInfoExport.h"
|
||||
#include "circt/Dialect/Calyx/CalyxEmitter.h"
|
||||
#include "circt/Dialect/ESI/ESIDialect.h"
|
||||
|
|
@ -38,6 +39,7 @@ inline void registerAllTranslations() {
|
|||
mlir::smt::registerExportSMTLIBTranslation();
|
||||
ExportSystemC::registerExportSystemCTranslation();
|
||||
debug::registerTranslations();
|
||||
aiger::registerImportAIGERTranslation();
|
||||
return true;
|
||||
}();
|
||||
(void)initOnce;
|
||||
|
|
|
|||
|
|
@ -21,6 +21,7 @@ add_subdirectory(HWToLLVM)
|
|||
add_subdirectory(HWToSMT)
|
||||
add_subdirectory(HWToSV)
|
||||
add_subdirectory(HWToSystemC)
|
||||
add_subdirectory(ImportAIGER)
|
||||
add_subdirectory(LoopScheduleToCalyx)
|
||||
add_subdirectory(MooreToCore)
|
||||
add_subdirectory(PipelineToHW)
|
||||
|
|
|
|||
|
|
@ -0,0 +1,19 @@
|
|||
add_circt_translation_library(CIRCTImportAIGER
|
||||
ImportAIGER.cpp
|
||||
|
||||
DEPENDS
|
||||
CIRCTConversionPassIncGen
|
||||
|
||||
LINK_COMPONENTS
|
||||
Support
|
||||
|
||||
LINK_LIBS PUBLIC
|
||||
CIRCTAIG
|
||||
CIRCTHW
|
||||
CIRCTComb
|
||||
CIRCTSeq
|
||||
CIRCTSupport
|
||||
MLIRIR
|
||||
MLIRSupport
|
||||
MLIRTranslateLib
|
||||
)
|
||||
|
|
@ -0,0 +1,971 @@
|
|||
//===----------------------------------------------------------------------===//
|
||||
//
|
||||
// Part of the LLVM Project, under the Apache License v2.0 with LLVM Exceptions.
|
||||
// See https://llvm.org/LICENSE.txt for license information.
|
||||
// SPDX-License-Identifier: Apache-2.0 WITH LLVM-exception
|
||||
//
|
||||
//===----------------------------------------------------------------------===//
|
||||
//
|
||||
// This file implements the AIGER file import functionality.
|
||||
//
|
||||
//===----------------------------------------------------------------------===//
|
||||
|
||||
#include "circt/Conversion/ImportAIGER.h"
|
||||
#include "circt/Dialect/AIG/AIGOps.h"
|
||||
#include "circt/Dialect/HW/HWOps.h"
|
||||
#include "circt/Dialect/Seq/SeqOps.h"
|
||||
#include "circt/Support/BackedgeBuilder.h"
|
||||
#include "mlir/IR/Builders.h"
|
||||
#include "mlir/IR/BuiltinOps.h"
|
||||
#include "mlir/IR/Diagnostics.h"
|
||||
#include "mlir/IR/Location.h"
|
||||
#include "mlir/IR/MLIRContext.h"
|
||||
#include "mlir/Support/FileUtilities.h"
|
||||
#include "mlir/Support/LogicalResult.h"
|
||||
#include "mlir/Support/Timing.h"
|
||||
#include "mlir/Tools/mlir-translate/Translation.h"
|
||||
#include "llvm/ADT/DenseMap.h"
|
||||
#include "llvm/ADT/StringExtras.h"
|
||||
#include "llvm/ADT/StringRef.h"
|
||||
#include "llvm/Support/Debug.h"
|
||||
#include "llvm/Support/ErrorHandling.h"
|
||||
#include "llvm/Support/SourceMgr.h"
|
||||
#include "llvm/Support/raw_ostream.h"
|
||||
#include <cctype>
|
||||
#include <string>
|
||||
|
||||
using namespace mlir;
|
||||
using namespace circt;
|
||||
using namespace circt::hw;
|
||||
using namespace circt::aig;
|
||||
using namespace circt::seq;
|
||||
using namespace circt::aiger;
|
||||
|
||||
#define DEBUG_TYPE "import-aiger"
|
||||
|
||||
namespace {
|
||||
|
||||
/// AIGER token types for lexical analysis
|
||||
enum class AIGERTokenKind {
|
||||
// Literals
|
||||
Number,
|
||||
Identifier,
|
||||
|
||||
// Special characters
|
||||
Newline,
|
||||
EndOfFile,
|
||||
|
||||
// Error
|
||||
Error
|
||||
};
|
||||
|
||||
/// Represents a token in the AIGER file
|
||||
struct AIGERToken {
|
||||
AIGERTokenKind kind;
|
||||
StringRef spelling;
|
||||
SMLoc location;
|
||||
|
||||
AIGERToken(AIGERTokenKind kind, StringRef spelling, SMLoc location)
|
||||
: kind(kind), spelling(spelling), location(location) {}
|
||||
};
|
||||
|
||||
/// Simple lexer for AIGER files
|
||||
///
|
||||
/// This lexer handles both ASCII (.aag) and binary (.aig) AIGER formats.
|
||||
/// It provides basic tokenization for header parsing and symbol tables,
|
||||
/// while also supporting byte-level reading for binary format.
|
||||
class AIGERLexer {
|
||||
public:
|
||||
AIGERLexer(const llvm::SourceMgr &sourceMgr, MLIRContext *context)
|
||||
: sourceMgr(sourceMgr),
|
||||
bufferNameIdentifier(getMainBufferNameIdentifier(sourceMgr, context)),
|
||||
curBuffer(
|
||||
sourceMgr.getMemoryBuffer(sourceMgr.getMainFileID())->getBuffer()),
|
||||
curPtr(curBuffer.begin()) {}
|
||||
|
||||
/// Get the next token
|
||||
AIGERToken nextToken();
|
||||
|
||||
/// Lex the current position as a symbol (used for symbol table parsing)
|
||||
AIGERToken lexAsSymbol();
|
||||
|
||||
/// Peek at the current token without consuming it
|
||||
AIGERToken peekToken();
|
||||
|
||||
/// Check if we're at end of file
|
||||
bool isAtEOF() const { return curPtr >= curBuffer.end(); }
|
||||
|
||||
/// Read a single byte for binary parsing
|
||||
ParseResult readByte(unsigned char &byte) {
|
||||
if (curPtr >= curBuffer.end())
|
||||
return failure();
|
||||
byte = *curPtr++;
|
||||
return success();
|
||||
}
|
||||
|
||||
/// Get current location
|
||||
SMLoc getCurrentLoc() const { return SMLoc::getFromPointer(curPtr); }
|
||||
|
||||
/// Encode the specified source location information into a Location object
|
||||
/// for attachment to the IR or error reporting.
|
||||
Location translateLocation(llvm::SMLoc loc) {
|
||||
assert(loc.isValid());
|
||||
unsigned mainFileID = sourceMgr.getMainFileID();
|
||||
auto lineAndColumn = sourceMgr.getLineAndColumn(loc, mainFileID);
|
||||
return FileLineColLoc::get(bufferNameIdentifier, lineAndColumn.first,
|
||||
lineAndColumn.second);
|
||||
}
|
||||
|
||||
/// Emit an error message and return an error token.
|
||||
AIGERToken emitError(const char *loc, const Twine &message) {
|
||||
mlir::emitError(translateLocation(SMLoc::getFromPointer(loc)), message);
|
||||
return AIGERToken(AIGERTokenKind::Error, StringRef(loc, 1),
|
||||
SMLoc::getFromPointer(loc));
|
||||
}
|
||||
|
||||
private:
|
||||
const llvm::SourceMgr &sourceMgr;
|
||||
StringAttr bufferNameIdentifier;
|
||||
StringRef curBuffer;
|
||||
const char *curPtr;
|
||||
|
||||
/// Get the main buffer name identifier
|
||||
static StringAttr
|
||||
getMainBufferNameIdentifier(const llvm::SourceMgr &sourceMgr,
|
||||
MLIRContext *context) {
|
||||
auto mainBuffer = sourceMgr.getMemoryBuffer(sourceMgr.getMainFileID());
|
||||
StringRef bufferName = mainBuffer->getBufferIdentifier();
|
||||
if (bufferName.empty())
|
||||
bufferName = "<unknown>";
|
||||
return StringAttr::get(context, bufferName);
|
||||
}
|
||||
|
||||
/// Skip whitespace (except newlines)
|
||||
void skipWhitespace();
|
||||
|
||||
/// Skip to end of line (for comment handling)
|
||||
void skipUntilNewline();
|
||||
|
||||
/// Lex a number
|
||||
AIGERToken lexNumber();
|
||||
|
||||
/// Lex an identifier
|
||||
AIGERToken lexIdentifier();
|
||||
|
||||
/// Create a token
|
||||
AIGERToken makeToken(AIGERTokenKind kind, const char *start) {
|
||||
return AIGERToken(kind, StringRef(start, curPtr - start),
|
||||
SMLoc::getFromPointer(start));
|
||||
}
|
||||
};
|
||||
|
||||
/// Main AIGER parser class
|
||||
///
|
||||
/// This parser implements the complete AIGER format specification including:
|
||||
/// - ASCII (.aag) and binary (.aig) formats
|
||||
/// - Basic AIGER components (inputs, latches, outputs, AND gates)
|
||||
/// - Optional sections (bad states, constraints, justice, fairness)
|
||||
/// - Symbol tables and comments
|
||||
///
|
||||
/// The parser creates MLIR modules using the HW, AIG, and Seq dialects.
|
||||
class AIGERParser {
|
||||
public:
|
||||
AIGERParser(const llvm::SourceMgr &sourceMgr, MLIRContext *context,
|
||||
ModuleOp module, const ImportAIGEROptions &options)
|
||||
: lexer(sourceMgr, context), context(context), module(module),
|
||||
options(options), builder(context) {}
|
||||
|
||||
/// Parse the AIGER file and populate the MLIR module
|
||||
ParseResult parse();
|
||||
|
||||
private:
|
||||
AIGERLexer lexer;
|
||||
MLIRContext *context;
|
||||
ModuleOp module;
|
||||
const ImportAIGEROptions &options;
|
||||
OpBuilder builder;
|
||||
|
||||
// AIGER file data
|
||||
unsigned maxVarIndex = 0;
|
||||
unsigned numInputs = 0;
|
||||
unsigned numLatches = 0;
|
||||
unsigned numOutputs = 0;
|
||||
unsigned numAnds = 0;
|
||||
bool isBinaryFormat = false;
|
||||
|
||||
// A mapping from {kind, index} -> symbol where kind is 0 for inputs, 1 for
|
||||
// latches, and 2 for outputs.
|
||||
enum SymbolKind : unsigned { Input, Latch, Output };
|
||||
DenseMap<std::pair<SymbolKind, unsigned>, StringAttr> symbolTable;
|
||||
|
||||
// Parsed data storage
|
||||
SmallVector<unsigned> inputLiterals;
|
||||
SmallVector<std::tuple<unsigned, unsigned, SMLoc>>
|
||||
latchDefs; // current, next, loc
|
||||
SmallVector<std::pair<unsigned, SMLoc>> outputLiterals; // literal, loc
|
||||
SmallVector<std::tuple<unsigned, unsigned, unsigned, SMLoc>>
|
||||
andGateDefs; // lhs, rhs0, rhs1
|
||||
|
||||
/// Parse the header line (format and counts)
|
||||
ParseResult parseHeader();
|
||||
|
||||
/// Parse inputs section
|
||||
ParseResult parseInputs();
|
||||
|
||||
/// Parse latches section
|
||||
ParseResult parseLatches();
|
||||
|
||||
/// Parse outputs section
|
||||
ParseResult parseOutputs();
|
||||
|
||||
/// Parse AND gates section (dispatches to ASCII or binary)
|
||||
ParseResult parseAndGates();
|
||||
|
||||
/// Parse AND gates in ASCII format
|
||||
ParseResult parseAndGatesASCII();
|
||||
|
||||
/// Parse AND gates in binary format with delta compression
|
||||
ParseResult parseAndGatesBinary();
|
||||
|
||||
/// Parse symbol table (optional)
|
||||
ParseResult parseSymbolTable();
|
||||
|
||||
/// Parse comments (optional)
|
||||
ParseResult parseComments();
|
||||
|
||||
/// Convert AIGER literal to MLIR value using backedges
|
||||
///
|
||||
/// \param literal The AIGER literal (variable * 2 + inversion)
|
||||
/// \param backedges Map from literals to backedge values
|
||||
/// \param loc Location for created operations
|
||||
/// \return The MLIR value corresponding to the literal, or nullptr on error
|
||||
Value getLiteralValue(unsigned literal,
|
||||
DenseMap<unsigned, Backedge> &backedges, Location loc);
|
||||
|
||||
/// Create the top-level HW module from parsed data
|
||||
ParseResult createModule();
|
||||
|
||||
InFlightDiagnostic emitError(llvm::SMLoc loc, const Twine &message) {
|
||||
return mlir::emitError(lexer.translateLocation(loc), message);
|
||||
}
|
||||
|
||||
/// Emit error at current location
|
||||
InFlightDiagnostic emitError(const Twine &message) {
|
||||
return emitError(lexer.getCurrentLoc(), message);
|
||||
}
|
||||
|
||||
/// Expect and consume a specific token kind
|
||||
ParseResult expectToken(AIGERTokenKind kind, const Twine &message);
|
||||
|
||||
/// Parse a number token into result
|
||||
ParseResult parseNumber(unsigned &result);
|
||||
|
||||
/// Parse a binary encoded number (variable-length encoding)
|
||||
ParseResult parseBinaryNumber(unsigned &result);
|
||||
|
||||
/// Expect and consume a newline token
|
||||
ParseResult parseNewLine();
|
||||
};
|
||||
|
||||
} // anonymous namespace
|
||||
|
||||
//===----------------------------------------------------------------------===//
|
||||
// AIGERLexer Implementation
|
||||
//===----------------------------------------------------------------------===//
|
||||
|
||||
void AIGERLexer::skipWhitespace() {
|
||||
while (curPtr < curBuffer.end()) {
|
||||
// NOTE: Don't use llvm::isSpace here because it also skips '\n'.
|
||||
if (*curPtr == ' ' || *curPtr == '\t' || *curPtr == '\r') {
|
||||
++curPtr;
|
||||
continue;
|
||||
}
|
||||
|
||||
// Treat "//" as whitespace. This is not part of the AIGER format, but we
|
||||
// support it for FileCheck tests.
|
||||
if (*curPtr == '/' &&
|
||||
(curPtr + 1 < curBuffer.end() && *(curPtr + 1) == '/')) {
|
||||
skipUntilNewline();
|
||||
continue;
|
||||
}
|
||||
break;
|
||||
}
|
||||
}
|
||||
|
||||
void AIGERLexer::skipUntilNewline() {
|
||||
while (curPtr < curBuffer.end() && *curPtr != '\n')
|
||||
++curPtr;
|
||||
if (curPtr < curBuffer.end() && *curPtr == '\n')
|
||||
++curPtr;
|
||||
}
|
||||
|
||||
AIGERToken AIGERLexer::lexNumber() {
|
||||
const char *start = curPtr;
|
||||
while (curPtr < curBuffer.end() && llvm::isDigit(*curPtr))
|
||||
++curPtr;
|
||||
return makeToken(AIGERTokenKind::Number, start);
|
||||
}
|
||||
|
||||
AIGERToken AIGERLexer::lexIdentifier() {
|
||||
const char *start = curPtr;
|
||||
while (curPtr < curBuffer.end() && (llvm::isAlnum(*curPtr) || *curPtr == '_'))
|
||||
++curPtr;
|
||||
|
||||
StringRef spelling(start, curPtr - start);
|
||||
AIGERTokenKind kind = AIGERTokenKind::Identifier;
|
||||
|
||||
return makeToken(kind, start);
|
||||
}
|
||||
|
||||
AIGERToken AIGERLexer::nextToken() {
|
||||
skipWhitespace();
|
||||
|
||||
auto impl = [this]() {
|
||||
if (curPtr >= curBuffer.end())
|
||||
return makeToken(AIGERTokenKind::EndOfFile, curPtr);
|
||||
|
||||
const char *start = curPtr;
|
||||
char c = *curPtr++;
|
||||
|
||||
switch (c) {
|
||||
case '\n':
|
||||
return makeToken(AIGERTokenKind::Newline, start);
|
||||
case '\r':
|
||||
case ' ':
|
||||
case '\t':
|
||||
llvm_unreachable("Whitespace should have been skipped");
|
||||
return makeToken(AIGERTokenKind::Error, start);
|
||||
default:
|
||||
if (llvm::isDigit(c)) {
|
||||
--curPtr; // Back up to re-lex the number
|
||||
return lexNumber();
|
||||
}
|
||||
if (llvm::isAlpha(c) || c == '_') {
|
||||
--curPtr; // Back up to re-lex the identifier
|
||||
return lexIdentifier();
|
||||
}
|
||||
assert((c != '/' || *curPtr != '/') && "// should have been skipped");
|
||||
return makeToken(AIGERTokenKind::Error, start);
|
||||
}
|
||||
};
|
||||
|
||||
auto token = impl();
|
||||
skipWhitespace();
|
||||
return token;
|
||||
}
|
||||
|
||||
AIGERToken AIGERLexer::lexAsSymbol() {
|
||||
skipWhitespace();
|
||||
const char *start = curPtr;
|
||||
while (curPtr < curBuffer.end() &&
|
||||
(llvm::isPrint(*curPtr) && !llvm::isSpace(*curPtr)))
|
||||
++curPtr;
|
||||
return makeToken(AIGERTokenKind::Identifier, start);
|
||||
}
|
||||
|
||||
AIGERToken AIGERLexer::peekToken() {
|
||||
const char *savedPtr = curPtr;
|
||||
AIGERToken token = nextToken();
|
||||
curPtr = savedPtr;
|
||||
return token;
|
||||
}
|
||||
|
||||
//===----------------------------------------------------------------------===//
|
||||
// AIGERParser Implementation
|
||||
//===----------------------------------------------------------------------===//
|
||||
|
||||
ParseResult AIGERParser::parse() {
|
||||
if (parseHeader() || parseInputs() || parseLatches() || parseOutputs() ||
|
||||
parseAndGates() || parseSymbolTable() || parseComments())
|
||||
return failure();
|
||||
// Create the final module
|
||||
return createModule();
|
||||
}
|
||||
|
||||
ParseResult AIGERParser::expectToken(AIGERTokenKind kind,
|
||||
const Twine &message) {
|
||||
AIGERToken token = lexer.nextToken();
|
||||
if (token.kind != kind)
|
||||
return emitError(message);
|
||||
return success();
|
||||
}
|
||||
|
||||
ParseResult AIGERParser::parseNumber(unsigned &result) {
|
||||
auto startLoc = lexer.getCurrentLoc();
|
||||
auto token = lexer.nextToken();
|
||||
|
||||
if (token.kind != AIGERTokenKind::Number)
|
||||
return emitError(startLoc, "expected number");
|
||||
|
||||
if (token.spelling.getAsInteger(10, result))
|
||||
return emitError(startLoc, "invalid number format");
|
||||
|
||||
return success();
|
||||
}
|
||||
|
||||
ParseResult AIGERParser::parseBinaryNumber(unsigned &result) {
|
||||
// AIGER binary format uses variable-length encoding
|
||||
// Each byte has 7 data bits and 1 continuation bit (MSB)
|
||||
// If continuation bit is set, more bytes follow
|
||||
|
||||
result = 0;
|
||||
unsigned shift = 0;
|
||||
|
||||
while (true) {
|
||||
unsigned char byte;
|
||||
if (lexer.readByte(byte))
|
||||
return emitError("unexpected end of file in binary number");
|
||||
|
||||
LLVM_DEBUG(llvm::dbgs() << "Read byte: 0x" << llvm::utohexstr(byte) << " ("
|
||||
<< (unsigned)byte << ")\n");
|
||||
|
||||
result |= (byte & 0x7F) << shift;
|
||||
|
||||
if ((byte & 0x80) == 0) { // No continuation bit
|
||||
LLVM_DEBUG(llvm::dbgs() << "Decoded binary number: " << result << "\n");
|
||||
break;
|
||||
}
|
||||
|
||||
shift += 7;
|
||||
if (shift >= 32) // Prevent overflow
|
||||
return emitError("binary number too large");
|
||||
}
|
||||
|
||||
return success();
|
||||
}
|
||||
|
||||
ParseResult AIGERParser::parseHeader() {
|
||||
LLVM_DEBUG(llvm::dbgs() << "Parsing AIGER header\n");
|
||||
|
||||
// Parse format identifier (aag or aig)
|
||||
while (lexer.peekToken().kind != AIGERTokenKind::Identifier)
|
||||
lexer.nextToken();
|
||||
|
||||
auto startLoc = lexer.getCurrentLoc();
|
||||
auto formatToken = lexer.nextToken();
|
||||
if (formatToken.spelling == "aag") {
|
||||
isBinaryFormat = false;
|
||||
LLVM_DEBUG(llvm::dbgs() << "Format: aag (ASCII)\n");
|
||||
} else if (formatToken.spelling == "aig") {
|
||||
isBinaryFormat = true;
|
||||
LLVM_DEBUG(llvm::dbgs() << "Format: aig (binary)\n");
|
||||
} else {
|
||||
return emitError(startLoc, "expected 'aag' or 'aig' format identifier");
|
||||
}
|
||||
|
||||
// Parse M I L O A (numbers separated by spaces)
|
||||
if (parseNumber(maxVarIndex))
|
||||
return emitError("failed to parse M (max variable index)");
|
||||
|
||||
if (parseNumber(numInputs))
|
||||
return emitError("failed to parse I (number of inputs)");
|
||||
|
||||
if (parseNumber(numLatches))
|
||||
return emitError("failed to parse L (number of latches)");
|
||||
|
||||
if (parseNumber(numOutputs))
|
||||
return emitError("failed to parse O (number of outputs)");
|
||||
|
||||
if (parseNumber(numAnds))
|
||||
return emitError("failed to parse A (number of AND gates)");
|
||||
|
||||
LLVM_DEBUG(llvm::dbgs() << "Header: M=" << maxVarIndex << " I=" << numInputs
|
||||
<< " L=" << numLatches << " O=" << numOutputs
|
||||
<< " A=" << numAnds << "\n");
|
||||
|
||||
// Expect newline after header
|
||||
return parseNewLine();
|
||||
}
|
||||
|
||||
ParseResult AIGERParser::parseNewLine() {
|
||||
auto token = lexer.nextToken();
|
||||
if (token.kind != AIGERTokenKind::Newline)
|
||||
return emitError("expected newline");
|
||||
|
||||
return success();
|
||||
}
|
||||
|
||||
ParseResult AIGERParser::parseInputs() {
|
||||
LLVM_DEBUG(llvm::dbgs() << "Parsing " << numInputs << " inputs\n");
|
||||
if (isBinaryFormat) {
|
||||
// In binary format, inputs are implicit (literals 2, 4, 6, ...)
|
||||
for (unsigned i = 0; i < numInputs; ++i)
|
||||
inputLiterals.push_back(2 * (i + 1));
|
||||
return success();
|
||||
}
|
||||
|
||||
for (unsigned i = 0; i < numInputs; ++i) {
|
||||
unsigned literal;
|
||||
auto startLoc = lexer.getCurrentLoc();
|
||||
if (parseNumber(literal) || parseNewLine())
|
||||
return emitError(startLoc, "failed to parse input literal");
|
||||
inputLiterals.push_back(literal);
|
||||
}
|
||||
|
||||
return success();
|
||||
}
|
||||
|
||||
ParseResult AIGERParser::parseLatches() {
|
||||
LLVM_DEBUG(llvm::dbgs() << "Parsing " << numLatches << " latches\n");
|
||||
auto startLoc = lexer.getCurrentLoc();
|
||||
if (isBinaryFormat) {
|
||||
// In binary format, latches are implicit (literals 2, 4, 6, ...)
|
||||
for (unsigned i = 0; i < numLatches; ++i) {
|
||||
unsigned literal;
|
||||
if (parseNumber(literal))
|
||||
return emitError(startLoc, "failed to parse latch next state literal");
|
||||
|
||||
latchDefs.push_back({2 * (i + 1 + numInputs), literal, startLoc});
|
||||
|
||||
// Expect newline after each latch next state
|
||||
if (parseNewLine())
|
||||
return failure();
|
||||
}
|
||||
return success();
|
||||
}
|
||||
|
||||
// Parse latch definitions: current_state next_state
|
||||
for (unsigned i = 0; i < numLatches; ++i) {
|
||||
unsigned currentState, nextState;
|
||||
if (parseNumber(currentState) || parseNumber(nextState) || parseNewLine())
|
||||
return emitError(startLoc, "failed to parse latch definition");
|
||||
|
||||
LLVM_DEBUG(llvm::dbgs() << "Latch " << i << ": " << currentState << " -> "
|
||||
<< nextState << "\n");
|
||||
|
||||
// Validate current state literal (should be even and positive)
|
||||
if (currentState % 2 != 0 || currentState == 0)
|
||||
return emitError(startLoc, "invalid latch current state literal");
|
||||
|
||||
latchDefs.push_back({currentState, nextState, startLoc});
|
||||
}
|
||||
|
||||
return success();
|
||||
}
|
||||
|
||||
ParseResult AIGERParser::parseOutputs() {
|
||||
LLVM_DEBUG(llvm::dbgs() << "Parsing " << numOutputs << " outputs\n");
|
||||
// NOTE: Parsing is same for binary and ASCII formats
|
||||
auto startLoc = lexer.getCurrentLoc();
|
||||
|
||||
// Parse output literals
|
||||
for (unsigned i = 0; i < numOutputs; ++i) {
|
||||
unsigned literal;
|
||||
if (parseNumber(literal) || parseNewLine())
|
||||
return emitError(startLoc, "failed to parse output literal");
|
||||
|
||||
LLVM_DEBUG(llvm::dbgs() << "Output " << i << ": " << literal << "\n");
|
||||
|
||||
// Output literals can be any valid literal (including inverted)
|
||||
outputLiterals.push_back({literal, startLoc});
|
||||
}
|
||||
|
||||
return success();
|
||||
}
|
||||
|
||||
ParseResult AIGERParser::parseAndGates() {
|
||||
LLVM_DEBUG(llvm::dbgs() << "Parsing " << numAnds << " AND gates\n");
|
||||
|
||||
if (isBinaryFormat) {
|
||||
return parseAndGatesBinary();
|
||||
}
|
||||
return parseAndGatesASCII();
|
||||
}
|
||||
|
||||
ParseResult AIGERParser::parseAndGatesASCII() {
|
||||
auto startLoc = lexer.getCurrentLoc();
|
||||
// Parse AND gate definitions: lhs rhs0 rhs1
|
||||
for (unsigned i = 0; i < numAnds; ++i) {
|
||||
unsigned lhs, rhs0, rhs1;
|
||||
if (parseNumber(lhs) || parseNumber(rhs0) || parseNumber(rhs1) ||
|
||||
parseNewLine())
|
||||
return emitError(startLoc, "failed to parse AND gate definition");
|
||||
|
||||
LLVM_DEBUG(llvm::dbgs() << "AND Gate " << i << ": " << lhs << " = " << rhs0
|
||||
<< " & " << rhs1 << "\n");
|
||||
|
||||
// Validate LHS (should be even and positive)
|
||||
if (lhs % 2 != 0 || lhs == 0)
|
||||
return emitError(startLoc, "invalid AND gate LHS literal");
|
||||
|
||||
// Validate literal bounds
|
||||
if (lhs / 2 > maxVarIndex || rhs0 / 2 > maxVarIndex ||
|
||||
rhs1 / 2 > maxVarIndex)
|
||||
return emitError(startLoc,
|
||||
"AND gate literal exceeds maximum variable index");
|
||||
|
||||
andGateDefs.push_back({lhs, rhs0, rhs1, startLoc});
|
||||
}
|
||||
|
||||
return success();
|
||||
}
|
||||
|
||||
ParseResult AIGERParser::parseAndGatesBinary() {
|
||||
// In binary format, AND gates are encoded with delta compression
|
||||
// Each AND gate is encoded as: delta0 delta1
|
||||
// where: rhs0 = lhs - delta0, rhs1 = rhs0 - delta1
|
||||
auto startLoc = lexer.getCurrentLoc();
|
||||
|
||||
LLVM_DEBUG(llvm::dbgs() << "Starting binary AND gate parsing\n");
|
||||
|
||||
// First AND gate LHS starts after inputs and latches
|
||||
// Variables are numbered: 1, 2, ..., maxVarIndex
|
||||
// Literals are: 2, 4, 6, ..., 2*maxVarIndex
|
||||
// Inputs: 2, 4, ..., 2*numInputs
|
||||
// Latches: 2*(numInputs+1), 2*(numInputs+2), ..., 2*(numInputs+numLatches)
|
||||
// AND gates: 2*(numInputs+numLatches+1), 2*(numInputs+numLatches+2), ...
|
||||
auto currentLHS = 2 * (numInputs + numLatches + 1);
|
||||
|
||||
LLVM_DEBUG(llvm::dbgs() << "First AND gate LHS should be: " << currentLHS
|
||||
<< "\n");
|
||||
|
||||
for (unsigned i = 0; i < numAnds; ++i) {
|
||||
unsigned delta0, delta1;
|
||||
if (parseBinaryNumber(delta0) || parseBinaryNumber(delta1))
|
||||
return emitError("failed to parse binary AND gate deltas");
|
||||
|
||||
auto lhs = static_cast<int64_t>(currentLHS);
|
||||
|
||||
// Check for underflow before subtraction
|
||||
if (delta0 > lhs || delta1 > (lhs - delta0)) {
|
||||
LLVM_DEBUG(llvm::dbgs() << "Delta underflow: lhs=" << lhs << ", delta0="
|
||||
<< delta0 << ", delta1=" << delta1 << "\n");
|
||||
return emitError("invalid binary AND gate: delta causes underflow");
|
||||
}
|
||||
|
||||
auto rhs0 = lhs - delta0;
|
||||
auto rhs1 = rhs0 - delta1;
|
||||
|
||||
LLVM_DEBUG(llvm::dbgs() << "Binary AND Gate " << i << ": " << lhs << " = "
|
||||
<< rhs0 << " & " << rhs1 << " (deltas: " << delta0
|
||||
<< ", " << delta1 << ")\n");
|
||||
|
||||
if (lhs / 2 > maxVarIndex || rhs0 / 2 > maxVarIndex ||
|
||||
rhs1 / 2 > maxVarIndex)
|
||||
return emitError(
|
||||
"binary AND gate literal exceeds maximum variable index");
|
||||
|
||||
assert(lhs > rhs0 && rhs0 >= rhs1 &&
|
||||
"invalid binary AND gate: ordering constraint violated");
|
||||
|
||||
andGateDefs.push_back({static_cast<unsigned>(lhs),
|
||||
static_cast<unsigned>(rhs0),
|
||||
static_cast<unsigned>(rhs1), startLoc});
|
||||
currentLHS += 2; // Next AND gate LHS
|
||||
}
|
||||
|
||||
return success();
|
||||
}
|
||||
|
||||
ParseResult AIGERParser::parseSymbolTable() {
|
||||
// Symbol table is optional and starts with 'i', 'l', or 'o' followed by
|
||||
// position
|
||||
while (!lexer.isAtEOF()) {
|
||||
auto token = lexer.peekToken();
|
||||
if (token.kind != AIGERTokenKind::Identifier)
|
||||
break;
|
||||
(void)lexer.nextToken();
|
||||
|
||||
char symbolType = token.spelling.front();
|
||||
if (symbolType != 'i' && symbolType != 'l' && symbolType != 'o')
|
||||
break;
|
||||
|
||||
unsigned literal;
|
||||
if (token.spelling.drop_front().getAsInteger(10, literal))
|
||||
return emitError("failed to parse symbol position");
|
||||
|
||||
SymbolKind kind;
|
||||
switch (symbolType) {
|
||||
case 'i':
|
||||
kind = SymbolKind::Input;
|
||||
break;
|
||||
case 'l':
|
||||
kind = SymbolKind::Latch;
|
||||
break;
|
||||
case 'o':
|
||||
kind = SymbolKind::Output;
|
||||
break;
|
||||
}
|
||||
|
||||
auto nextToken = lexer.lexAsSymbol();
|
||||
if (nextToken.kind != AIGERTokenKind::Identifier)
|
||||
return emitError("expected symbol name");
|
||||
|
||||
LLVM_DEBUG(llvm::dbgs()
|
||||
<< "Symbol " << literal << ": " << nextToken.spelling << "\n");
|
||||
|
||||
symbolTable[{kind, literal}] = StringAttr::get(context, nextToken.spelling);
|
||||
if (parseNewLine())
|
||||
return failure();
|
||||
}
|
||||
|
||||
return success();
|
||||
}
|
||||
|
||||
ParseResult AIGERParser::parseComments() {
|
||||
// Comments start with 'c' and continue to end of file
|
||||
auto token = lexer.peekToken();
|
||||
if (token.kind == AIGERTokenKind::Identifier && token.spelling == "c") {
|
||||
// Skip comments for now
|
||||
return success();
|
||||
}
|
||||
|
||||
return success();
|
||||
}
|
||||
|
||||
Value AIGERParser::getLiteralValue(unsigned literal,
|
||||
DenseMap<unsigned, Backedge> &backedges,
|
||||
Location loc) {
|
||||
LLVM_DEBUG(llvm::dbgs() << "Getting value for literal " << literal << "\n");
|
||||
|
||||
// Handle constants
|
||||
if (literal == 0) {
|
||||
// FALSE constant
|
||||
return builder.create<hw::ConstantOp>(
|
||||
loc, builder.getI1Type(),
|
||||
builder.getIntegerAttr(builder.getI1Type(), 0));
|
||||
}
|
||||
|
||||
if (literal == 1) {
|
||||
// TRUE constant
|
||||
return builder.create<hw::ConstantOp>(
|
||||
loc, builder.getI1Type(),
|
||||
builder.getIntegerAttr(builder.getI1Type(), 1));
|
||||
}
|
||||
|
||||
// Extract variable and inversion
|
||||
unsigned variable = literal / 2;
|
||||
bool inverted = literal % 2;
|
||||
unsigned baseLiteral = variable * 2;
|
||||
|
||||
LLVM_DEBUG(llvm::dbgs() << " Variable: " << variable
|
||||
<< ", inverted: " << inverted
|
||||
<< ", baseLiteral: " << baseLiteral << "\n");
|
||||
|
||||
// Validate literal bounds
|
||||
if (variable > maxVarIndex) {
|
||||
LLVM_DEBUG(llvm::dbgs() << " ERROR: Variable " << variable
|
||||
<< " exceeds maxVarIndex " << maxVarIndex << "\n");
|
||||
return nullptr;
|
||||
}
|
||||
|
||||
// Look up the backedge for this literal
|
||||
auto backedgeIt = backedges.find(baseLiteral);
|
||||
if (backedgeIt == backedges.end()) {
|
||||
LLVM_DEBUG(llvm::dbgs() << " ERROR: No backedge found for literal "
|
||||
<< baseLiteral << "\n");
|
||||
return nullptr; // Error: undefined literal
|
||||
}
|
||||
|
||||
Value baseValue = backedgeIt->second;
|
||||
if (!baseValue) {
|
||||
LLVM_DEBUG(llvm::dbgs() << " ERROR: Backedge value is null for literal "
|
||||
<< baseLiteral << "\n");
|
||||
return nullptr;
|
||||
}
|
||||
|
||||
// Apply inversion if needed
|
||||
if (inverted) {
|
||||
// Create an inverter using aig.and_inv with single input
|
||||
SmallVector<bool> inverts = {true};
|
||||
return builder.create<aig::AndInverterOp>(loc, builder.getI1Type(),
|
||||
ValueRange{baseValue}, inverts);
|
||||
}
|
||||
|
||||
return baseValue;
|
||||
}
|
||||
|
||||
ParseResult AIGERParser::createModule() {
|
||||
|
||||
// Create the top-level module
|
||||
std::string moduleName = options.topLevelModule;
|
||||
if (moduleName.empty())
|
||||
moduleName = "aiger_top";
|
||||
|
||||
// Set insertion point to the provided module
|
||||
builder.setInsertionPointToStart(module.getBody());
|
||||
|
||||
// Build input/output port info
|
||||
SmallVector<hw::PortInfo> ports;
|
||||
|
||||
// Add input ports
|
||||
for (unsigned i = 0; i < numInputs; ++i) {
|
||||
hw::PortInfo port;
|
||||
auto name = symbolTable.lookup({SymbolKind::Input, i});
|
||||
port.name =
|
||||
name ? name : builder.getStringAttr("input_" + std::to_string(i));
|
||||
port.type = builder.getI1Type();
|
||||
port.dir = hw::ModulePort::Direction::Input;
|
||||
port.argNum = i;
|
||||
ports.push_back(port);
|
||||
}
|
||||
|
||||
// Add output ports
|
||||
for (unsigned i = 0; i < numOutputs; ++i) {
|
||||
hw::PortInfo port;
|
||||
auto name = symbolTable.lookup({SymbolKind::Output, i});
|
||||
port.name =
|
||||
name ? name : builder.getStringAttr("output_" + std::to_string(i));
|
||||
port.type = builder.getI1Type();
|
||||
port.dir = hw::ModulePort::Direction::Output;
|
||||
port.argNum = numInputs + i;
|
||||
ports.push_back(port);
|
||||
}
|
||||
|
||||
// Add clock port if we have latches
|
||||
if (numLatches > 0) {
|
||||
hw::PortInfo clockPort;
|
||||
clockPort.name = builder.getStringAttr("clock");
|
||||
clockPort.type = seq::ClockType::get(builder.getContext());
|
||||
clockPort.dir = hw::ModulePort::Direction::Input;
|
||||
clockPort.argNum = numInputs + numOutputs;
|
||||
ports.push_back(clockPort);
|
||||
}
|
||||
|
||||
// Create the HW module
|
||||
auto hwModule = builder.create<hw::HWModuleOp>(
|
||||
builder.getUnknownLoc(), builder.getStringAttr(moduleName), ports);
|
||||
|
||||
// Set insertion point inside the module
|
||||
builder.setInsertionPointToStart(hwModule.getBodyBlock());
|
||||
|
||||
// Get clock value if we have latches
|
||||
Value clockValue;
|
||||
if (numLatches > 0)
|
||||
clockValue = hwModule.getBodyBlock()->getArgument(numInputs);
|
||||
|
||||
// Use BackedgeBuilder to handle all values uniformly
|
||||
BackedgeBuilder bb(builder, builder.getUnknownLoc());
|
||||
DenseMap<unsigned, Backedge> backedges;
|
||||
|
||||
// Create backedges for all literals (inputs, latches, AND gates)
|
||||
for (unsigned i = 0; i < numInputs; ++i) {
|
||||
auto literal = inputLiterals[i];
|
||||
backedges[literal] = bb.get(builder.getI1Type());
|
||||
}
|
||||
for (auto [currentState, nextState, _] : latchDefs)
|
||||
backedges[currentState] = bb.get(builder.getI1Type());
|
||||
|
||||
for (auto [lhs, rhs0, rhs1, loc] : andGateDefs)
|
||||
backedges[lhs] = bb.get(builder.getI1Type());
|
||||
|
||||
// Set input values
|
||||
for (unsigned i = 0; i < numInputs; ++i) {
|
||||
auto inputValue = hwModule.getBodyBlock()->getArgument(i);
|
||||
auto literal = inputLiterals[i];
|
||||
backedges[literal].setValue(inputValue);
|
||||
}
|
||||
|
||||
// Create latches (registers) with backedges for next state
|
||||
for (auto [i, latchDef] : llvm::enumerate(latchDefs)) {
|
||||
auto [currentState, nextState, loc] = latchDef;
|
||||
// Get the backedge for the next state value
|
||||
auto nextBackedge = bb.get(builder.getI1Type());
|
||||
|
||||
// Create the register with the backedge as input
|
||||
auto regValue = builder.create<seq::CompRegOp>(
|
||||
lexer.translateLocation(loc), (Value)nextBackedge, clockValue);
|
||||
if (auto name = symbolTable.lookup({SymbolKind::Latch, i}))
|
||||
regValue.setNameAttr(name);
|
||||
|
||||
// Set the backedge for this latch's current state
|
||||
backedges[currentState].setValue(regValue);
|
||||
}
|
||||
|
||||
// Build AND gates using backedges to handle forward references
|
||||
for (auto [lhs, rhs0, rhs1, loc] : andGateDefs) {
|
||||
// Get or create backedges for operands
|
||||
auto location = lexer.translateLocation(loc);
|
||||
auto rhs0Value = getLiteralValue(rhs0 & ~1u, backedges, location);
|
||||
auto rhs1Value = getLiteralValue(rhs1 & ~1u, backedges, location);
|
||||
|
||||
if (!rhs0Value || !rhs1Value)
|
||||
return emitError(loc, "failed to get operand values for AND gate");
|
||||
|
||||
// Determine inversion for inputs
|
||||
SmallVector<bool> inverts = {static_cast<bool>(rhs0 % 2),
|
||||
static_cast<bool>(rhs1 % 2)};
|
||||
|
||||
// Create AND gate with potential inversions
|
||||
auto andResult = builder.create<aig::AndInverterOp>(
|
||||
location, builder.getI1Type(), ValueRange{rhs0Value, rhs1Value},
|
||||
inverts);
|
||||
|
||||
// Set the backedge for this AND gate's result
|
||||
backedges[lhs].setValue(andResult);
|
||||
}
|
||||
|
||||
// Now resolve the latch next state connections.
|
||||
// We need to update the CompRegOp operations with their actual next state
|
||||
// values
|
||||
for (auto [currentState, nextState, sourceLoc] : latchDefs) {
|
||||
auto loc = lexer.translateLocation(sourceLoc);
|
||||
auto nextValue = getLiteralValue(nextState, backedges, loc);
|
||||
if (!nextValue)
|
||||
return emitError(sourceLoc, "undefined literal in latch next state");
|
||||
|
||||
// Find the register operation for this latch and update its input
|
||||
Value currentValue = backedges[currentState];
|
||||
if (auto regOp = currentValue.getDefiningOp<seq::CompRegOp>())
|
||||
regOp.getInputMutable().assign(nextValue);
|
||||
else
|
||||
return emitError(sourceLoc, "failed to find register for latch");
|
||||
}
|
||||
|
||||
// Create output values
|
||||
SmallVector<Value> outputValues;
|
||||
for (auto [literal, sourceLoc] : outputLiterals) {
|
||||
auto loc = lexer.translateLocation(sourceLoc);
|
||||
auto outputValue = getLiteralValue(literal, backedges, loc);
|
||||
if (!outputValue)
|
||||
return emitError(sourceLoc, "undefined literal in output");
|
||||
outputValues.push_back(outputValue);
|
||||
}
|
||||
|
||||
// Create output operation
|
||||
auto *outputOp = hwModule.getBodyBlock()->getTerminator();
|
||||
outputOp->setOperands(outputValues);
|
||||
|
||||
return success();
|
||||
}
|
||||
|
||||
//===----------------------------------------------------------------------===//
|
||||
// Public API Implementation
|
||||
//===----------------------------------------------------------------------===//
|
||||
|
||||
LogicalResult circt::aiger::importAIGER(llvm::SourceMgr &sourceMgr,
|
||||
MLIRContext *context,
|
||||
mlir::TimingScope &ts, ModuleOp module,
|
||||
const ImportAIGEROptions *options) {
|
||||
// Load required dialects
|
||||
context->loadDialect<hw::HWDialect>();
|
||||
context->loadDialect<aig::AIGDialect>();
|
||||
context->loadDialect<seq::SeqDialect>();
|
||||
|
||||
// Use default options if none provided
|
||||
ImportAIGEROptions defaultOptions;
|
||||
if (!options)
|
||||
options = &defaultOptions;
|
||||
|
||||
// Create parser and parse the file
|
||||
AIGERParser parser(sourceMgr, context, module, *options);
|
||||
return parser.parse();
|
||||
}
|
||||
|
||||
//===----------------------------------------------------------------------===//
|
||||
// Translation Registration
|
||||
//===----------------------------------------------------------------------===//
|
||||
|
||||
void circt::aiger::registerImportAIGERTranslation() {
|
||||
static mlir::TranslateToMLIRRegistration fromAIGER(
|
||||
"import-aiger", "import AIGER file",
|
||||
[](llvm::SourceMgr &sourceMgr, MLIRContext *context) {
|
||||
mlir::TimingScope ts;
|
||||
OwningOpRef<ModuleOp> module(
|
||||
ModuleOp::create(UnknownLoc::get(context)));
|
||||
ImportAIGEROptions options;
|
||||
if (failed(importAIGER(sourceMgr, context, ts, module.get(), &options)))
|
||||
module = {};
|
||||
return module;
|
||||
});
|
||||
}
|
||||
|
|
@ -0,0 +1,7 @@
|
|||
aig 8199 8196 1 2 2
|
||||
16398
|
||||
16396
|
||||
16394
|
||||
'¹E
|
||||
ûc
|
||||
Generated by CIRCT unknown git version
|
||||
|
|
@ -0,0 +1,18 @@
|
|||
// RUN: circt-translate --import-aiger %S/basic-binary.aig --split-input-file --verify-diagnostics | FileCheck %s
|
||||
// Test is generated from the following MLIR:
|
||||
// TODO: After the AIGER exporter is upstreamed, generate AIG file from this MLIR.
|
||||
// hw.module @aiger_top(in %input_0 : i8196, out output_0 : i1, out output_1 : i1, in %clock: !seq.clock) {
|
||||
// %0 = comb.extract %input from 1234 : (i8196) -> i1
|
||||
// %1 = comb.extract %input from 5678 : (i8196) -> i1
|
||||
// %2 = comb.extract %input from 3 : (i8196) -> i1
|
||||
// %3 = comb.extract %input from 8193 : (i8196) -> i1
|
||||
// %and1 = aig.and_inv not %1, %0 : i1
|
||||
// %and2 = aig.and_inv %3, not %2 : i1
|
||||
// %reg = seq.compreg %clock, %and1 : i1
|
||||
// hw.output %and1, %and2, %reg : i1, i1
|
||||
// }
|
||||
// CHECK-LABEL: @aiger_top
|
||||
// CHECK-NEXT: %[[REG:.+]] = seq.compreg %[[VAL1:.+]], %clock : i1
|
||||
// CHECK-NEXT: %[[VAL0:.+]] = aig.and_inv not %input_5678, %input_1234 : i1
|
||||
// CHECK-NEXT: %[[VAL1]] = aig.and_inv %input_8193, not %input_3 : i1
|
||||
// CHECK-NEXT: hw.output %[[VAL0]], %[[REG]] : i1, i1
|
||||
|
|
@ -0,0 +1,210 @@
|
|||
// RUN: circt-translate --import-aiger %s --split-input-file | FileCheck %s
|
||||
|
||||
// Test basic AND gate
|
||||
// CHECK-LABEL: hw.module @aiger_top
|
||||
// CHECK-SAME: (in %[[INPUT0:.+]] : i1, in %[[INPUT1:.+]] : i1, out [[OUTPUT0:.+]] : i1) {
|
||||
// CHECK-NEXT: %[[AND:.+]] = aig.and_inv %[[INPUT1]], %[[INPUT0]] : i1
|
||||
// CHECK-NEXT: hw.output %[[AND]] : i1
|
||||
// CHECK-NEXT: }
|
||||
aag 3 2 0 1 1
|
||||
2
|
||||
4
|
||||
6
|
||||
6 4 2
|
||||
|
||||
// -----
|
||||
// Test invert
|
||||
// CHECK-LABEL: hw.module @aiger_top
|
||||
// CHECK-SAME: (in %[[INPUT0:.+]] : i1, in %[[INPUT1:.+]] : i1, out [[OUTPUT0:.+]] : i1) {
|
||||
// CHECK-NEXT: %[[AND:.+]] = aig.and_inv not %[[INPUT1]], not %[[INPUT0]] : i1
|
||||
// CHECK-NEXT: hw.output %[[AND]] : i1
|
||||
// CHECK-NEXT: }
|
||||
aag 3 2 0 1 1
|
||||
2
|
||||
4
|
||||
6
|
||||
6 5 3
|
||||
|
||||
// -----
|
||||
// Test multiple outputs
|
||||
// CHECK-LABEL: hw.module @aiger_top
|
||||
// CHECK-SAME: (in %[[INPUT0:.+]] : i1, in %[[INPUT1:.+]] : i1, out [[OUTPUT0:.+]] : i1, out [[OUTPUT1:.+]] : i1) {
|
||||
// CHECK-NEXT: %[[VAL0:.+]] = aig.and_inv %[[INPUT1]], %[[INPUT0]] : i1
|
||||
// CHECK-NEXT: %[[VAL1:.+]] = aig.and_inv %[[VAL0]], %[[INPUT1]] : i1
|
||||
// CHECK-NEXT: hw.output %[[VAL0]], %[[VAL1]] : i1, i1
|
||||
// CHECK-NEXT: }
|
||||
aag 4 2 0 2 2
|
||||
2
|
||||
4
|
||||
6
|
||||
8
|
||||
6 4 2
|
||||
8 6 4
|
||||
|
||||
// -----
|
||||
// Test latch
|
||||
// CHECK-LABEL: hw.module @aiger_top
|
||||
// CHECK-SAME: (in %[[INPUT0:.+]] : i1, out [[OUTPUT0:.+]] : i1, in %[[CLOCK:.+]] : !seq.clock) {
|
||||
// CHECK-NEXT: %[[REG:.+]] = seq.compreg %[[AND:.+]], %[[CLOCK]] : i1
|
||||
// CHECK-NEXT: %[[AND]] = aig.and_inv %[[REG]], %[[INPUT0]] : i1
|
||||
// CHECK-NEXT: hw.output %[[REG]] : i1
|
||||
// CHECK-NEXT: }
|
||||
aag 3 1 1 1 1
|
||||
2
|
||||
4 6
|
||||
4
|
||||
6 4 2
|
||||
|
||||
// -----
|
||||
// Test with comments
|
||||
// CHECK-LABEL: hw.module @aiger_top
|
||||
// CHECK-SAME: (in %[[INPUT0:.+]] : i1, in %[[INPUT1:.+]] : i1, out [[OUTPUT0:.+]] : i1) {
|
||||
// CHECK-NEXT: %[[VAL:.+]] = aig.and_inv %[[INPUT1]], %[[INPUT0]] : i1
|
||||
// CHECK-NEXT: hw.output %[[VAL]] : i1
|
||||
// CHECK-NEXT: }
|
||||
aag 3 2 0 1 1
|
||||
2
|
||||
4
|
||||
6
|
||||
6 4 2
|
||||
c
|
||||
This is a comment line
|
||||
|
||||
// -----
|
||||
// Test symbol table
|
||||
// CHECK-LABEL: hw.module @aiger_top
|
||||
// CHECK-SAME: (in %[[IN1:in1]] : i1, in %[[IN2:in2]] : i1, out out : i1, in %[[CLOCK:.+]] : !seq.clock) {
|
||||
// CHECK-NEXT: %[[LATCH:latch]] = seq.compreg %[[AND:.+]], %[[CLOCK]] : i1
|
||||
// CHECK-NEXT: %[[AND]] = aig.and_inv %[[IN2]], %[[IN1]] : i1
|
||||
// CHECK-NEXT: hw.output %[[AND]] : i1
|
||||
// CHECK-NEXT: }
|
||||
aag 3 2 1 1 1
|
||||
2
|
||||
4
|
||||
8 6
|
||||
6
|
||||
6 4 2
|
||||
i0 in1
|
||||
i1 in2
|
||||
l0 latch
|
||||
o0 out
|
||||
|
||||
// -----
|
||||
// Test constant FALSE output
|
||||
// CHECK-LABEL: hw.module @aiger_top
|
||||
// CHECK-SAME: (out [[OUTPUT0:.+]] : i1) {
|
||||
// CHECK-NEXT: %[[FALSE:.+]] = hw.constant false
|
||||
// CHECK-NEXT: hw.output %[[FALSE]] : i1
|
||||
// CHECK-NEXT: }
|
||||
aag 0 0 0 1 0
|
||||
0
|
||||
|
||||
// -----
|
||||
// Test constant TRUE output
|
||||
// CHECK-LABEL: hw.module @aiger_top
|
||||
// CHECK-SAME: (out [[OUTPUT0:.+]] : i1) {
|
||||
// CHECK-NEXT: %[[TRUE:.+]] = hw.constant true
|
||||
// CHECK-NEXT: hw.output %[[TRUE]] : i1
|
||||
// CHECK-NEXT: }
|
||||
aag 0 0 0 1 0
|
||||
1
|
||||
|
||||
// -----
|
||||
// Test buffer (identity function)
|
||||
// CHECK-LABEL: hw.module @aiger_top
|
||||
// CHECK-SAME: (in %[[INPUT0:.+]] : i1, out [[OUTPUT0:.+]] : i1) {
|
||||
// CHECK-NEXT: hw.output %[[INPUT0]] : i1
|
||||
// CHECK-NEXT: }
|
||||
aag 1 1 0 1 0
|
||||
2
|
||||
2
|
||||
|
||||
// -----
|
||||
// Test inverter (NOT gate)
|
||||
// CHECK-LABEL: hw.module @aiger_top
|
||||
// CHECK-SAME: (in %[[INPUT0:.+]] : i1, out [[OUTPUT0:.+]] : i1) {
|
||||
// CHECK-NEXT: %[[VAL:.+]] = aig.and_inv not %[[INPUT0]] : i1
|
||||
// CHECK-NEXT: hw.output %[[VAL]] : i1
|
||||
// CHECK-NEXT: }
|
||||
aag 1 1 0 1 0
|
||||
2
|
||||
3
|
||||
|
||||
// -----
|
||||
// Test complex combinational logic (half adder)
|
||||
// CHECK-LABEL: hw.module @aiger_top
|
||||
// CHECK-SAME: (in %[[X:.+]] : i1, in %[[Y:.+]] : i1, out sum : i1, out carry : i1) {
|
||||
// CHECK-NEXT: %[[VAL0:.+]] = aig.and_inv not %[[Y]], not %[[X]] : i1
|
||||
// CHECK-NEXT: %[[VAL1:.+]] = aig.and_inv %[[X]], %[[Y]] : i1
|
||||
// CHECK-NEXT: %[[VAL2:.+]] = aig.and_inv not %[[VAL1]], not %[[VAL0]] : i1
|
||||
// CHECK-NEXT: hw.output %[[VAL0]], %[[VAL1]] : i1, i1
|
||||
// CHECK-NEXT: }
|
||||
aag 7 2 0 2 3
|
||||
2
|
||||
4
|
||||
6
|
||||
12
|
||||
6 5 3
|
||||
12 2 4
|
||||
14 13 7
|
||||
i0 x
|
||||
i1 y
|
||||
o0 sum
|
||||
o1 carry
|
||||
|
||||
// -----
|
||||
// Test multiple latches with different next states
|
||||
// CHECK-LABEL: hw.module @aiger_top
|
||||
// CHECK-SAME: (in %[[INPUT0:.+]] : i1, out [[OUTPUT0:.+]] : i1, out [[OUTPUT1:.+]] : i1, in %[[CLOCK:.+]] : !seq.clock) {
|
||||
// CHECK-NEXT: %[[Q1:q1]] = seq.compreg %[[VAL1:.+]], %[[CLOCK]] : i1
|
||||
// CHECK-NEXT: %[[Q2:q2]] = seq.compreg %[[VAL0:.+]], %[[CLOCK]] : i1
|
||||
// CHECK-NEXT: %[[VAL0]] = aig.and_inv %[[Q1]], %[[INPUT0]] : i1
|
||||
// CHECK-NEXT: %[[FALSE:.+]] = hw.constant false
|
||||
// CHECK-NEXT: %[[VAL1]] = aig.and_inv not %[[Q2]], %[[FALSE]] : i1
|
||||
// CHECK-NEXT: hw.output %[[Q1]], %[[Q2]] : i1, i1
|
||||
// CHECK-NEXT: }
|
||||
aag 5 1 2 2 2
|
||||
2
|
||||
4 10
|
||||
6 8
|
||||
4
|
||||
6
|
||||
8 4 2
|
||||
10 7 0
|
||||
l0 q1
|
||||
l1 q2
|
||||
|
||||
// -----
|
||||
// Test chain of AND gates
|
||||
// CHECK-LABEL: hw.module @aiger_top
|
||||
// CHECK-SAME: (in %[[INPUT0:.+]] : i1, in %[[INPUT1:.+]] : i1, in %[[INPUT2:.+]] : i1, out [[OUTPUT0:.+]] : i1) {
|
||||
// CHECK-NEXT: %[[VAL0:.+]] = aig.and_inv %[[INPUT1]], %[[INPUT0]] : i1
|
||||
// CHECK-NEXT: %[[VAL1:.+]] = aig.and_inv %[[INPUT2]], %[[VAL0]] : i1
|
||||
// CHECK-NEXT: hw.output %[[VAL1]] : i1
|
||||
// CHECK-NEXT: }
|
||||
aag 5 3 0 1 2
|
||||
2
|
||||
4
|
||||
6
|
||||
10
|
||||
8 4 2
|
||||
10 6 8
|
||||
|
||||
// -----
|
||||
// Test empty circuit (no inputs, no outputs)
|
||||
// CHECK-LABEL: hw.module @aiger_top() {
|
||||
// CHECK-NEXT: hw.output
|
||||
// CHECK-NEXT: }
|
||||
aag 0 0 0 0 0
|
||||
|
||||
// -----
|
||||
// Test circuit with only inputs (no logic)
|
||||
// CHECK-LABEL: hw.module @aiger_top
|
||||
// CHECK-SAME: (in %[[INPUT0:.+]] : i1, in %[[INPUT1:.+]] : i1, out [[OUTPUT0:.+]] : i1, out [[OUTPUT1:.+]] : i1) {
|
||||
// CHECK-NEXT: hw.output %[[INPUT0]], %[[INPUT1]] : i1, i1
|
||||
// CHECK-NEXT: }
|
||||
aag 2 2 0 2 0
|
||||
2
|
||||
4
|
||||
2
|
||||
4
|
||||
|
|
@ -0,0 +1,3 @@
|
|||
aig 3 2 0 1 1
|
||||
6
|
||||
|
||||
|
|
@ -0,0 +1,2 @@
|
|||
// RUN: not circt-translate --import-aiger %S/delta-underflow.aig --split-input-file 2>&1 | FileCheck %s
|
||||
// CHECK: invalid binary AND gate: delta causes underflow
|
||||
|
|
@ -0,0 +1,41 @@
|
|||
// RUN: circt-translate --import-aiger %s --split-input-file --verify-diagnostics
|
||||
|
||||
// Test invalid format identifier
|
||||
// expected-error @below {{expected 'aag' or 'aig' format identifier}}
|
||||
xyz 1 1 0 1 0
|
||||
|
||||
// -----
|
||||
// Test invalid header with missing numbers
|
||||
// expected-error @below {{expected number}}
|
||||
// expected-error @below {{failed to parse L (number of latches)}}
|
||||
aag 3 2 a
|
||||
|
||||
// -----
|
||||
// Test literal bound checking
|
||||
aag 2 1 0 1 1
|
||||
2
|
||||
4
|
||||
// expected-error @below {{AND gate literal exceeds maximum variable index}}
|
||||
6 4 2
|
||||
|
||||
// -----
|
||||
// Test invalid latch literal (odd number)
|
||||
aag 2 0 1 1 0
|
||||
// expected-error @below {{invalid latch current state literal}}
|
||||
3 2
|
||||
3
|
||||
|
||||
// -----
|
||||
// Test output referencing non-existent variable
|
||||
aag 1 1 0 1 0
|
||||
2
|
||||
// expected-error @below {{undefined literal in output}}
|
||||
4
|
||||
|
||||
// -----
|
||||
// Test invalid symbol table entry
|
||||
aag 1 1 0 1 0
|
||||
2
|
||||
2
|
||||
// expected-error @below {{failed to parse symbol position}}
|
||||
i0x invalid_symbol
|
||||
|
|
@ -22,7 +22,7 @@ config.name = 'CIRCT'
|
|||
config.test_format = lit.formats.ShTest(not llvm_config.use_lit_shell)
|
||||
|
||||
# suffixes: A list of file extensions to treat as test files.
|
||||
config.suffixes = ['.td', '.mlir', '.ll', '.fir', '.sv', '.test']
|
||||
config.suffixes = ['.aag', '.td', '.mlir', '.ll', '.fir', '.sv', '.test']
|
||||
|
||||
# test_source_root: The root path where tests are located.
|
||||
config.test_source_root = os.path.dirname(__file__)
|
||||
|
|
|
|||
Loading…
Reference in New Issue