From 93f3791fbe24a34d105fa493001504ddc805b531 Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Wed, 22 Oct 2025 11:15:07 -0700 Subject: [PATCH 01/17] Command "&dg" contributed by Jiun-Hao Chen from NTU. --- src/aig/gia/gia.h | 4 + src/aig/gia/giaDecGraph.cpp | 2216 +++++++++++++++++++++++++++++++++++ src/aig/gia/module.make | 3 +- src/base/abci/abc.c | 76 ++ 4 files changed, 2298 insertions(+), 1 deletion(-) create mode 100644 src/aig/gia/giaDecGraph.cpp diff --git a/src/aig/gia/gia.h b/src/aig/gia/gia.h index 1d0290c04..45f2329cb 100644 --- a/src/aig/gia/gia.h +++ b/src/aig/gia/gia.h @@ -1827,6 +1827,10 @@ extern void Tas_ManSatPrintStats( Tas_Man_t * p ); extern int Tas_ManSolve( Tas_Man_t * p, Gia_Obj_t * pObj, Gia_Obj_t * pObj2 ); extern int Tas_ManSolveArray( Tas_Man_t * p, Vec_Ptr_t * vObjs ); +/*=== giaDecGraph.c ===========================================================*/ +extern Gia_Man_t* Gia_ManDecGraph( Gia_Man_t* p ); +extern Gia_Man_t* Gia_ManDecGraphFromFile( char* pFileName ); + /*=== giaBound.c ===========================================================*/ typedef struct Bnd_Man_t_ Bnd_Man_t; diff --git a/src/aig/gia/giaDecGraph.cpp b/src/aig/gia/giaDecGraph.cpp new file mode 100644 index 000000000..01a7101c6 --- /dev/null +++ b/src/aig/gia/giaDecGraph.cpp @@ -0,0 +1,2216 @@ +/**CFile**************************************************************** + + FileName [giaDecGraph.c] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [Scalable AIG package.] + + Synopsis [Implementation of circuit learning.] + + Author [Jiun-Hao Chen] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - 2025.] + + Revision [$Id: giaDecGraph.c,v 1.00 2025/01/01 00:00:00 Exp $] + +***********************************************************************/ + +#ifdef _WIN32 + +#ifndef __MINGW32__ +#pragma warning(disable : 4786) // warning C4786: identifier was truncated to '255' characters in the browser information +#endif +#endif + +#include +#include +#include +#include +#include +#include +#include +#include +#include +#include +#include +#include +#include + +#include "gia.h" +#include "misc/vec/vecHash.h" + +ABC_NAMESPACE_IMPL_START + +namespace DecGraph { + +template::value, int>::type = 0> +struct integer_iterator { + using iterator_category = std::input_iterator_tag; + using value_type = I; + using difference_type = I; + using pointer = I*; + using reference = I&; + + explicit integer_iterator(I value) + : value(value) { + } + + I operator*() const { + return value; + } + + I const* operator->() const { + return &value; + } + + integer_iterator& operator++() { + ++value; + return *this; + } + + integer_iterator operator++(int) { + const auto copy = *this; + ++*this; + return copy; + } + + bool operator==(const integer_iterator& other) const { + return value == other.value; + } + + bool operator!=(const integer_iterator& other) const { + return value != other.value; + } + +protected: + I value; +}; + +template::value, + bool>::type + = true> +struct integer_range { +public: + integer_range(I begin, I end) + : begin_(begin), end_(end) { + } + integer_iterator begin() const { + return begin_; + } + integer_iterator end() const { + return end_; + } + +private: + integer_iterator begin_; + integer_iterator end_; +}; + +template::value, + bool>::type + = true, + typename std::enable_if::value, + bool>::type + = true> +integer_range irange(Integer1 begin, Integer2 end) { + return {static_cast(begin), + std::max(static_cast(begin), end)}; +} + +template::value, + bool>::type + = true> +integer_range irange(Integer end) { + return {Integer(), std::max(Integer(), end)}; +} +// End Iterger Iterator + +static int IdToLit(int id, bool fCompl) { + return (id << 1) | (fCompl ? 1 : 0); +} + +static int LitToId(int lit) { + return lit >> 1; +} + +static int LitNot(int lit) { + return lit ^ 1; +} +static int LitNotCond(int lit, bool cond) { + return lit ^ (int)cond; +} + +static int LitIsComplement(int lit) { + return (lit & 1); +} + +#ifdef _MSC_VER +#include +#define __builtin_popcount __popcnt +#endif + +#ifdef DECTHREAD +#else +static int decGraphXadd(int* addr, int delta) { + int temp = *addr; + *addr += delta; + return temp; +} +#endif + +static int neededWords(int num_variables) { + return num_variables <= 6 ? 1 : 1 << (num_variables - 6); +} + +static inline const uint64_t permutation_mask[5][3] = { + {0x9999999999999999, 0x2222222222222222, 0x4444444444444444}, + {0xC3C3C3C3C3C3C3C3, 0x0C0C0C0C0C0C0C0C, 0x3030303030303030}, + {0xF00FF00FF00FF00F, 0x00F000F000F000F0, 0x0F000F000F000F00}, + {0xFF0000FFFF0000FF, 0x0000FF000000FF00, 0x00FF000000FF0000}, + {0xFFFF00000000FFFF, 0x00000000FFFF0000, 0x0000FFFF00000000}}; +static inline const uint64_t swap_mask[6][6] = { + {0x2222222222222222, 0x0A0A0A0A0A0A0A0A, 0x00AA00AA00AA00AA, 0x0000AAAA0000AAAA, 0x00000000AAAAAAAA, 0xAAAAAAAAAAAAAAAA}, + {0x0000000000000000, 0x0C0C0C0C0C0C0C0C, 0x00CC00CC00CC00CC, 0x0000CCCC0000CCCC, 0x00000000CCCCCCCC, 0xCCCCCCCCCCCCCCCC}, + {0x0000000000000000, 0x0000000000000000, 0x00F000F000F000F0, 0x0000F0F00000F0F0, 0x00000000F0F0F0F0, 0xF0F0F0F0F0F0F0F0}, + {0x0000000000000000, 0x0000000000000000, 0x0000000000000000, 0x0000FF000000FF00, 0x00000000FF00FF00, 0xFF00FF00FF00FF00}, + {0x0000000000000000, 0x0000000000000000, 0x0000000000000000, 0x0000000000000000, 0x00000000FFFF0000, 0xFFFF0000FFFF0000}, + {0x0000000000000000, 0x0000000000000000, 0x0000000000000000, 0x0000000000000000, 0x0000000000000000, 0xFFFFFFFF00000000}}; +static inline const uint64_t elementary_mask[6] = { + 0xAAAAAAAAAAAAAAAA, + 0xCCCCCCCCCCCCCCCC, + 0xF0F0F0F0F0F0F0F0, + 0xFF00FF00FF00FF00, + 0xFFFF0000FFFF0000, + 0xFFFFFFFF00000000}; +static inline const uint64_t extend_mask[5] = { + 0xC000000000000000, + 0xF000000000000000, + 0xFF00000000000000, + 0xFFFF000000000000, + 0xFFFFFFFF00000000}; +static inline const uint64_t ones_mask[7]{ + 0x0000000000000001, + 0x0000000000000003, + 0x000000000000000f, + 0x00000000000000ff, + 0x000000000000ffff, + 0x00000000ffffffff, + 0xffffffffffffffff}; + +struct TruthTableData { + int refcount; + std::vector data; + std::vector place_to_variable; + std::vector variable_to_place; +}; + +class TruthTable { +public: + // empty + TruthTable(); + // release + ~TruthTable(); + // copy + TruthTable(const TruthTable& m); + // assign + TruthTable& operator=(const TruthTable& m); + // deep copy + TruthTable clone(void) const; + // deep copy from other truth table, inplace + void clone_from(const TruthTable& tt); + +public: + // build from bits + TruthTable(uint64_t bits); + +public: + // allocate truth table + void create(uint64_t bits); + +public: + // refcount++ + void addref(); + // refcount-- + void release(); + +public: + bool operator[](int index); + bool operator==(const TruthTable& rhs) const; + bool operator!=(const TruthTable& rhs) const; + TruthTable operator~(void); + +public: + uint8_t nVars() const; + uint64_t nBits() const; + uint32_t nWords() const; + bool empty() const; + +public: + uint64_t* data() const; + void set(int index, bool value); + void rand(); + void readBinary(std::string bitstream); + void readBinaryReverse(std::string bitstream); + void readHex(std::string bitstream); + void readHexReverse(std::string bitstream); + +public: + void resetPosition(void); + void moveTo(uint32_t variable, uint8_t place, bool adjecent = false); + void swapVariable(int variable1, int variable2); + void extend(int nVariable, std::vector variableOrder = {}); + int countCofactor(int nBoundSet, std::vector& cofactors, std::vector& boundSetFunctions, bool derive = false); + TruthTable cofactor(uint32_t variable, bool negative); + uint64_t countOne(void); + bool hasVariable(uint32_t variable); + int supportSize(void); + int isAndorOr(void); + void variablePartition(int nMSB, std::vector& MSB, std::vector& LSB); + uint32_t getVariable(int place); + void swapAdjacent(uint64_t* rdata, uint64_t* data, int index); + float cost(void); + +public: + std::string hash_str(void); + +private: + void assign(int offset, uint64_t value); + void assign(uint64_t value); + +public: + enum class Format { + BIN, + HEX + }; + void print(Format format = Format::BIN); + void printReverse(Format format = Format::BIN); + void printPosition(void); + std::string str(Format format = Format::BIN); + std::string strReverse(Format format = Format::BIN); + +private: + std::vector fourierTransform_rec(uint64_t begin, uint64_t end); + +public: + std::vector fourierTransform(void); + std::vector fourierWeight(void); + float fourierCost(void); + +private: + // pointer to the read data + TruthTableData* _data; + + // reference counter + int* _refcount; + + // number of variables + uint8_t _vars; + // number of bits + uint64_t _bits; +}; + +inline TruthTable::TruthTable() + : _data(nullptr), _refcount(nullptr), _vars(0), _bits(0) { +} + +inline TruthTable::~TruthTable() { + release(); +} + +inline TruthTable::TruthTable(const TruthTable& m) + : _data(m._data), _refcount(m._refcount), _vars(m._vars), _bits(m._bits) { + addref(); +} + +inline TruthTable& TruthTable::operator=(const TruthTable& m) { + if (this == &m) + return *this; + + if (m._refcount) + decGraphXadd(m._refcount, 1); + + release(); + + _data = m._data; + _refcount = m._refcount; + _vars = m._vars; + _bits = m._bits; + + return *this; +} + +inline TruthTable::TruthTable(uint64_t bits) + : _data(nullptr), _refcount(nullptr), _vars(0), _bits(0) { + create(bits); +} + +inline void TruthTable::addref(void) { + if (_refcount) + decGraphXadd(_refcount, 1); +} + +inline void TruthTable::release(void) { + if (_refcount && decGraphXadd(_refcount, -1) == 1) { + delete _data; + } + + _data = nullptr; + _refcount = nullptr; + _vars = 0; + _bits = 0; +} + +inline uint8_t TruthTable::nVars() const { + return _vars; +} + +inline uint64_t TruthTable::nBits() const { + return _bits; +} + +inline uint32_t TruthTable::nWords() const { + return _data ? _data->data.size() : 0; +} + +inline bool TruthTable::empty() const { + return (_data == nullptr) || (_bits == 0); +} + +inline uint64_t* TruthTable::data() const { + if (_data) + return _data->data.data(); + return nullptr; +} + +inline bool TruthTable::operator[](int index) { + if (empty()) + return false; + return (_data->data[index / (sizeof(uint64_t) * 8)] << (index % (sizeof(uint64_t) * 8))) & 0x8000000000000000; +} + +TruthTable TruthTable::clone(void) const { + if (empty()) + return TruthTable(); + + TruthTable tt; + + tt.create(_bits); + + if (tt.empty()) { + return tt; + } + + *tt._data = *this->_data; + *tt._refcount = 1; + + return tt; +} + +void TruthTable::clone_from(const TruthTable &tt) { + *this = tt.clone(); + return; +} + +void TruthTable::create(uint64_t bits) { + if (_bits == bits) { + resetPosition(); + return; + } + + release(); + + _bits = bits; + _vars = std::log2(bits); + + _data = new TruthTableData; + + if (_data) { + _data->data.resize(std::max((uint64_t)(bits / (sizeof(uint64_t) * 8)), (uint64_t)1), 0); + resetPosition(); + _refcount = &_data->refcount; + *_refcount = 1; + } + return; +} + +bool TruthTable::operator==(const TruthTable &rhs) const { + if (this->_data == rhs._data) + return true; + if (nBits() != rhs.nBits()) + return false; + + uint64_t *ldata = this->data(); + uint64_t *rdata = rhs.data(); + for (const auto &i : irange(nWords())) { + if (ldata[i] != rdata[i]) + return false; + } + return true; +} + +bool TruthTable::operator!=(const TruthTable &rhs) const { + return !(*this == rhs); +} + +TruthTable TruthTable::operator~(void) { + TruthTable rtt(nBits()); + uint64_t *ldata = this->data(); + uint64_t *rdata = rtt.data(); + for (const auto &i : irange(nWords())) { + rdata[i] = ~ldata[i]; + } + if (nBits() < 64) { + for (const auto &i : irange(nBits(), 64)) { + rtt.set(i, false); + } + } + return rtt; +} + +void TruthTable::set(int index, bool value) { + if (empty()) + return; + + uint64_t *data = &_data->data[0]; + if (value) { + data[index / (sizeof(uint64_t) * 8)] |= (uint64_t)0x8000000000000000 >> (index % (sizeof(uint64_t) * 8)); + } else { + data[index / (sizeof(uint64_t) * 8)] &= ~((uint64_t)0x8000000000000000 >> (index % (sizeof(uint64_t) * 8))); + } + return; +} + +void TruthTable::rand(void) { + if (empty()) + return; + + uint64_t *data = this->data(); + for (const auto &i : irange(nWords())) { + data[i] = ((uint64_t)std::rand() << 32) | ((uint64_t)std::rand()); + } + for (const auto &i : irange(nBits(), ((uint64_t)64 * nWords()))) { + set(i, false); + } + return; +} + +void TruthTable::readBinary(std::string bitstream) { + create(bitstream.size()); + for (const auto &i : irange(nBits())) { + set(i, bitstream[i] == '1'); + } + return; +} + +void TruthTable::readBinaryReverse(std::string bitstream_reverse) { + std::reverse(bitstream_reverse.begin(), bitstream_reverse.end()); + readBinary(bitstream_reverse); + return; +} + +static char hexToBin(char ch) { + if (ch >= '0' && ch <= '9') return ch - '0'; + if (ch >= 'A' && ch <= 'F') return ch - 'A' + 10; + if (ch >= 'a' && ch <= 'f') return ch - 'a' + 10; + return 0; +} + +void TruthTable::readHex(std::string bitstream) { + create(bitstream.size() * 4); + for (const auto &i : irange(nBits() / 4)) { + char value = hexToBin(bitstream[i]); + for (const auto &j : irange(4)) { + set(i * 4 + j, (value >> (3 - j)) & 1); + } + } + return; +} + +void TruthTable::readHexReverse(std::string bitstream) { + create(bitstream.size() * 4); + for (const auto &i : irange(nBits() / 4)) { + char value = hexToBin(bitstream[i]); + for (const auto &j : irange(4)) { + set(nBits() - (i * 4 + j) - 1, (value << j) & 0x8); + } + } + return; +} + +void TruthTable::resetPosition(void) { + if (empty()) + return; + + auto &place_to_variable = _data->place_to_variable; + auto &variable_to_place = _data->variable_to_place; + place_to_variable.resize(nVars()); + variable_to_place.resize(nVars()); + for (const auto &i : irange(nVars())) { + place_to_variable[i] = variable_to_place[i] = i; + } + return; +} + +void TruthTable::moveTo(uint32_t variable, uint8_t place, bool adjecent) { + if (empty()) + return; + + auto &place_to_variable = _data->place_to_variable; + auto &variable_to_place = _data->variable_to_place; + + if (!adjecent) { + swapVariable(variable_to_place[variable], place); + } + + TruthTable temp(nBits()); + uint64_t *pData = this->data(); + uint64_t *pOut = temp.data(); + uint64_t *pTemp = nullptr; + uint32_t iPlace0, iPlace1, Count = 0; + while (variable_to_place[variable] < place) { + iPlace0 = variable_to_place[variable]; + iPlace1 = variable_to_place[variable] + 1; + this->swapAdjacent(pOut, pData, iPlace0); + pTemp = pData; + pData = pOut, pOut = pTemp; + variable_to_place[place_to_variable[iPlace0]]++; + variable_to_place[place_to_variable[iPlace1]]--; + std::swap(place_to_variable[iPlace0], place_to_variable[iPlace1]); + Count++; + } + while (variable_to_place[variable] > place) { + iPlace0 = variable_to_place[variable] - 1; + iPlace1 = variable_to_place[variable]; + this->swapAdjacent(pOut, pData, iPlace0); + pTemp = pData; + pData = pOut, pOut = pTemp; + variable_to_place[place_to_variable[iPlace0]]++; + variable_to_place[place_to_variable[iPlace1]]--; + std::swap(place_to_variable[iPlace0], place_to_variable[iPlace1]); + Count++; + } + uint64_t *data = this->data(); + if (Count & 1) { + for (const auto &i : irange(nWords())) { + data[i] = pData[i]; + } + } + return; +} + +void TruthTable::swapVariable(int variable1, int variable2) { + if (empty()) + return; + + int nWord = nWords(); + + if (variable1 == variable2) { + return; + } + if (variable2 < variable1) { + std::swap(variable1, variable2); + } + + auto &place_to_variable = _data->place_to_variable; + auto &variable_to_place = _data->variable_to_place; + uint64_t *data = this->data(); + if (variable1 < 6 && variable2 < 6) { + int nShift = (1 << variable2) - (1 << variable1); + for (const auto &w : irange(nWord)) { + uint64_t low2High = (data[w] & swap_mask[variable1][variable2 - 1]) << nShift; + data[w] &= ~swap_mask[variable1][variable2 - 1]; + uint64_t high2Low = (data[w] & (swap_mask[variable1][variable2 - 1] << nShift)) >> nShift; + data[w] &= ~(swap_mask[variable1][variable2 - 1] << nShift); + data[w] = data[w] | low2High | high2Low; + } + } else if (variable1 < 6 && variable2 >= 6) { + int nStep = neededWords(variable2 + 1) / 2; + int nShift = 1 << variable1; + for (int w = 0; w < nWord; w += 2 * nStep) { + for (int j = 0; j < nStep; j++) { + uint64_t low2High = (data[w + j] & (swap_mask[variable1][5] >> nShift)) << nShift; + data[w + j] &= ~(swap_mask[variable1][5] >> nShift); + uint64_t high2Low = (data[w + nStep + j] & (swap_mask[variable1][5])) >> nShift; + data[w + nStep + j] &= ~(swap_mask[variable1][5]); + data[w + j] |= high2Low; + data[w + nStep + j] |= low2High; + } + } + } else { + int nStep1 = neededWords(variable1 + 1) / 2; + int nStep2 = neededWords(variable2 + 1) / 2; + for (int w = 0; w < nWord; w += 2 * nStep2) { + for (int i = 0; i < nStep2; i += 2 * nStep1) { + for (int j = 0; j < nStep1; j++) { + std::swap(data[w + nStep1 + i + j], data[w + nStep2 + i + j]); + } + } + } + } + + variable_to_place[place_to_variable[variable1]] = variable2; + variable_to_place[place_to_variable[variable2]] = variable1; + std::swap(place_to_variable[variable1], place_to_variable[variable2]); + return; +} + +void TruthTable::extend(int nExtend, std::vector variable_order) { + if (empty()) + return; + + TruthTable temp(this->nBits() * (((uint64_t)1) << nExtend)); + + int vars = this->nVars(); + int bits = this->nBits(); + uint64_t *data = this->data(); + uint64_t *temp_data = temp.data(); + if (vars < 6) { + for (const auto &i : irange(std::min((((uint64_t)1) << nExtend), (uint64_t)64))) { + temp_data[0] |= (data[0] & extend_mask[vars - 1]) >> (i * bits); + } + if (temp.nWords() > 1) { + for (const auto &i : irange(1, temp.nWords())) { + temp_data[i] = temp_data[0]; + } + } + } else { + int nSize = nWords(); + for (const auto &i : irange((((uint64_t)1) << nExtend))) { + for (const auto &j : irange(nSize)) { + temp_data[i * nSize + j] = data[j]; + } + } + } + for (const auto &i : irange(variable_order.size())) { + temp.moveTo(i, variable_order[i]); + } + temp.resetPosition(); + this->clone_from(temp); + return; +} + +int TruthTable::countCofactor(int nBoundSet, std::vector &cofactors, std::vector &boundSetFunctions, bool derive) { + if (empty()) + return 0; + + uint64_t nFreeSet = nVars() - nBoundSet; + uint64_t nMinterm = ((uint64_t)1 << nBoundSet); + if (derive) { + cofactors.clear(); + boundSetFunctions.clear(); + } + if (nFreeSet == 0) { + if (derive) { + cofactors.emplace_back(*this); + } + return 1; + } + + std::vector iCofactor(128, 0); + uint64_t iShift = 0; + uint64_t i, c, w; + uint64_t nCofactor; + + uint64_t *data = this->data(); + if (nFreeSet < 6) { + uint64_t sCofactor = ((uint64_t)1 << nFreeSet); + uint64_t mCofactor = (((uint64_t)1) << sCofactor) - 1; + for (nCofactor = i = 0; i < nMinterm; ++i) { + uint64_t cofactor = (data[(iShift + i * sCofactor) / 64] >> ((64 - (iShift + (i + 1) * sCofactor)) % 64)) & mCofactor; + for (c = 0; c < nCofactor; ++c) { + if (cofactor == iCofactor[c]) { + break; + } + } + // record the unique cofactor + if (c == nCofactor) { + iCofactor[nCofactor++] = cofactor; + if (derive) { + boundSetFunctions.emplace_back(TruthTable(nMinterm)); + } + } + if (derive) { + // record the bound set function + for (c = 0; c < nCofactor; ++c) { + if (cofactor == iCofactor[c]) { + boundSetFunctions[c].set(i, true); + } + } + } + } + if (derive) { + for (c = 0; c < nCofactor; ++c) { + TruthTable cofactor(((uint64_t)1 << nFreeSet)); + cofactor.assign(iCofactor[c]); + cofactors.emplace_back(cofactor); + } + } + } else { + uint32_t nWords = neededWords(nFreeSet); + for (nCofactor = i = 0; i < nMinterm; ++i) { + uint64_t *cofactor_begin = data + (iShift + i * nWords); + for (c = 0; c < nCofactor; ++c) { + uint64_t *cofactor_compare = data + (iShift + iCofactor[c] * nWords); + for (w = 0; w < nWords; ++w) { + if (cofactor_begin[w] != cofactor_compare[w]) { + break; + } + } + if (w == nWords) { + break; + } + } + // record the index of the unique cofactor + if (c == nCofactor) { + iCofactor[nCofactor++] = i; + if (derive) { + boundSetFunctions.emplace_back(TruthTable(nMinterm)); + } + } + // record the bound set function + if (derive) { + for (c = 0; c < nCofactor; ++c) { + uint64_t *cofactor_compare = data + (iShift + iCofactor[c] * nWords); + for (w = 0; w < nWords; ++w) { + if (cofactor_begin[w] != cofactor_compare[w]) { + break; + } + } + if (w == nWords) { + boundSetFunctions[c].set(i, true); + } + } + } + } + if (derive) { + for (c = 0; c < nCofactor; ++c) { + TruthTable cofactor(((uint64_t)1 << nFreeSet)); + for (w = 0; w < nWords; ++w) { + cofactor.assign(w, data[iShift + iCofactor[c] * nWords + w]); + } + cofactors.emplace_back(cofactor); + } + } + } + + return nCofactor; +} + +TruthTable TruthTable::cofactor(uint32_t variable, bool negative) { + if (empty()) + return TruthTable(); + + TruthTable rtt(nBits()); + + if (variable >= nVars()) { + fprintf(stderr, "[Error] TruthTable::cofactor: variable (%d) must be less than %d\n", variable, nVars()); + exit(-1); + } + + uint64_t *pdata = this->data(); + uint64_t *rdata = rtt.data(); + if (variable < 6) { + for (const auto &i : irange(nWords())) { + uint64_t mask = 0; + uint64_t data = pdata[i]; + if (negative) { + mask = (data & elementary_mask[variable]) | ((data & elementary_mask[variable]) >> (1 << variable)); + } else { + mask = (data & ~elementary_mask[variable]) | ((data & ~elementary_mask[variable]) << (1 << variable)); + } + rdata[i] = mask; + } + } else { + int nSize = nWords(); + int nMove = 1 << (variable - 6); + int nLength = 1 << (variable - 5); + int nSegment = nSize / nLength; + if (negative) { + for (const auto &s : irange(nSegment)) { + int offset = s * nLength; + for (const auto &i : irange(nMove)) { + rdata[offset + i] = rdata[offset + i + nMove] = pdata[offset + i]; + } + } + } else { + for (const auto &s : irange(nSegment)) { + int offset = s * nLength; + for (const auto &i : irange(nMove)) { + rdata[offset + i] = rdata[offset + i + nMove] = pdata[offset + i + nMove]; + } + } + } + } + + return rtt; +} + +uint64_t TruthTable::countOne(void) { + if (empty()) + return 0; + + uint64_t *data = this->data(); + uint64_t count = 0; + for (const auto &i : irange(nWords())) { + count += __builtin_popcount(data[i]); + } + return count; +} + +bool TruthTable::hasVariable(uint32_t variable) { + if (empty()) + return false; + + int nSize = nWords(); + uint64_t *data = this->data(); + + if (variable < 6) { + int nShift = 1 << variable; + for (const auto &i : irange(nSize)) { + if ((data[i] & ~elementary_mask[variable]) != ((data[i] & elementary_mask[variable]) >> nShift)) + return true; + } + } else { + int nStep = (1 << (variable - 6)); + for (int k = 0; k < nSize; k += 2 * nStep) { + for (const auto &i : irange(nStep)) { + if (data[i] != data[i + nStep]) + return true; + } + data += 2 * nStep; + } + } + return false; +} + +int TruthTable::supportSize(void) { + if (empty()) + return 0; + + int nSupport = 0; + for (const auto &i : irange(nVars())) { + nSupport += hasVariable(i); + } + return nSupport; +} + +int TruthTable::isAndorOr(void) { + if (empty()) + return 0; + + int supportSize = this->supportSize(); + int onSet = this->countOne(); + int offSet = this->nBits() - onSet; + int condition = ((uint64_t)1 << (nVars() - supportSize)); + if (onSet == condition || offSet == condition) { + return supportSize - 1; + } + return 0; +} + +void TruthTable::variablePartition(int nMSB, std::vector &MSB, std::vector &LSB) { + if (empty()) + return; + + MSB.clear(); + LSB.clear(); + for (const auto &i : irange(nVars())) { + if (i < nVars() - nMSB) { + LSB.push_back(getVariable(i)); + } else { + MSB.push_back(getVariable(i)); + } + } + return; +} + +uint32_t TruthTable::getVariable(int place) { + if (empty()) + return 0; + + return _data->place_to_variable[place]; +} + +void TruthTable::swapAdjacent(uint64_t *rdata, uint64_t *data, int variable) { + int nSize = nWords(); + + if (variable < 5) { + int shift = 1 << variable; + for (const auto &i : irange(nSize)) { + rdata[i] = (data[i] & permutation_mask[variable][0]) | ((data[i] & permutation_mask[variable][1]) << shift) | ((data[i] & permutation_mask[variable][2]) >> shift); + } + } else if (variable == 5) { + for (const auto &i : irange(nSize / 2)) { + rdata[i * 2 + 0] = (data[i * 2 + 0] & 0x00000000FFFFFFFF) | ((data[i * 2 + 1] & 0x00000000FFFFFFFF) << 32); + rdata[i * 2 + 1] = (data[i * 2 + 1] & 0xFFFFFFFF00000000) | ((data[i * 2 + 0] & 0xFFFFFFFF00000000) >> 32); + } + } else { + int nMove = (1 << (variable - 6)); + for (int i = 0; i < nSize; i += 4 * nMove) { + for (const auto &j : irange(nMove)) { + rdata[j + nMove * 0] = data[j + nMove * 0]; + rdata[j + nMove * 1] = data[j + nMove * 2]; + rdata[j + nMove * 2] = data[j + nMove * 1]; + rdata[j + nMove * 3] = data[j + nMove * 3]; + } + data += 4 * nMove; + rdata += 4 * nMove; + } + } +} + +template< typename T > +std::string int_to_hex( T i ) +{ + std::stringstream stream; + stream << "0x" + << std::setfill ('0') << std::setw(sizeof(T)*2) + << std::hex << i; + return stream.str(); +} + +std::string TruthTable::hash_str(void) { + if (empty()) { + return ""; + } + + std::string hash_str = ""; + uint64_t *data = this->data(); + for (const auto &i : irange(nWords())) { + hash_str += std::to_string(data[i]); + // hash_str += int_to_hex(data[i]); + } + return hash_str; +} + +void TruthTable::assign(uint64_t value) { + if (empty()) + return; + _data->data[0] = (_bits < 64) ? value << (64 - _bits) : value; + return; +} + +void TruthTable::assign(int offset, uint64_t value) { + if (empty()) + return; + _data->data[offset] = value; + return; +} + +void TruthTable::print(Format format) { + if (empty()) { + printf("Empty TruthTable\n"); + return; + } + + if (format == Format::BIN) { + printf("0b"); + } else if (format == Format::HEX) { + printf("0x"); + } + printf("%s\n", str(format).c_str()); + return; +} + +void TruthTable::printReverse(Format format) { + if (empty()) { + printf("Empty TruthTable\n"); + return; + } + + if (format == Format::BIN) { + printf("0b"); + } else if (format == Format::HEX) { + printf("0x"); + } + printf("%s\n", strReverse(format).c_str()); + return; +} + +void TruthTable::printPosition(void) { + if (empty()) { + printf("Empty TruthTable\n"); + return; + } + + for (const auto &i : irange(nVars())) { + printf("Place: %d -> Var[%ld]\n", i, _data->place_to_variable[i]); + } +} + +std::string TruthTable::str(Format format) { + std::string str = ""; + if (format == Format::BIN) { + for (const auto &i : irange(nBits())) { + str += (*this)[i] ? "1" : "0"; + } + } else if (format == Format::HEX) { + for (const auto &i : irange(nBits() / 4)) { + char value = 0; + for (const auto &j : irange(4)) { + value |= (*this)[i * 4 + j] << (3 - j); + } + char buf[2]; + sprintf(buf, "%X", value); + str += buf[0]; + } + } + return str; +} + +std::string TruthTable::strReverse(Format format) { + std::string str; + int bits = nBits(); + if (format == Format::BIN) { + for (const auto &i : irange(bits)) { + str += (*this)[bits - i - 1] ? "1" : "0"; + } + } else if (format == Format::HEX) { + for (const auto &i : irange(bits / 4)) { + char value = 0; + for (const auto &j : irange(4)) { + value |= (*this)[bits - (i * 4 + j) - 1] << (3 - j); + } + char buf[2]; + sprintf(buf, "%X", value); + str += buf[0]; + } + } + + return str; +} + +std::vector TruthTable::fourierTransform_rec(uint64_t begin, uint64_t end) { + if (begin == end) { + return {operator[](begin) ? 1 : -1}; + } + + int length = end - begin + 1; + auto mid = begin + length / 2; + auto left = fourierTransform_rec(begin, mid - 1); + auto right = fourierTransform_rec(mid, end); + std::vector result(length); + for (const auto &i : irange(length / 2)) { + result[i] = left[i] + right[i]; + result[i + length / 2] = left[i] - right[i]; + } + return result; +} + +std::vector TruthTable::fourierTransform(void) { + int bits = nBits(); + auto result = fourierTransform_rec(0, bits - 1); + std::vector result_norm(bits); + + for (const auto &i : irange(bits)) { + result_norm[i] = (float)result[i] / bits; + } + return result_norm; +} + +std::vector TruthTable::fourierWeight(void) { + uint64_t bits = nBits(); + auto coeffs = this->fourierTransform(); + std::vector weights(nVars() + 1); + + weights[0] = std::pow(coeffs[0], 2); + std::vector index(1, 1); + for (uint64_t i = 1; i < bits;) { + for (const auto &j : irange(index.size())) { + weights[index[j]] += std::pow(coeffs[i++], 2); + } + for (const auto &j : irange(index.size())) { + index.push_back(index[j] + 1); + } + } + + return weights; +} + +float TruthTable::fourierCost(void) { + uint64_t bits = nBits(); + auto coeffs = this->fourierTransform(); + std::vector weights(nVars() + 1); + + weights[0] = std::pow(coeffs[0], 2); + std::vector index(1, 1); + for (uint64_t i = 1; i < bits;) { + for (const auto &j : irange(index.size())) { + weights[index[j]] += std::pow(coeffs[i++], 2); + } + for (const auto &j : irange(index.size())) { + index.push_back(index[j] + 1); + } + } + + int sparsity_of_coeffs = 0; + for (const auto &i : irange(nBits())) { + sparsity_of_coeffs += coeffs[i] != 0; + } + int sparsity_of_weights = 0; + for (const auto &i : irange(nVars() + 1)) { + sparsity_of_weights += weights[i] != 0; + } + + // ::print(weights); + float cost = 0; + for (const auto &i : irange(nVars() + 1)) { + // cost += weights[i] * ((i + 1) * 3); + cost += weights[i] * ((i) * 3); + // cost += weights[i] * ((i)); + } + cost += (float)sparsity_of_coeffs / sparsity_of_weights; + return cost; +} + +uint64_t reverseBits(uint64_t n) { + uint64_t rev = 0; + + for (int i = 0; i < 64; i++) + rev = (rev << (uint64_t)1) | ((n >> i) & (uint64_t)1); + + return rev; +} + +float TruthTable::cost(void) { + if (nVars() == 4) { + // return func2node[reverseBits(data()[0])]; + } + return fourierCost(); +} + +class Combination { +public: + Combination(int n, int r); + bool next(void); + void next(int n); + std::vector& get(void); + std::vector get_reverse(void); + std::vector get_reverse(int n); + int count(void); + int getN(void); + int getR(void); + +private: + int n; + int r; + std::vector data; +}; + +inline Combination::Combination(int n, int r) + : n(n), r(r), data(r) { + for (const auto& i : irange(r)) { + data[i] = i; + } +} + +inline std::vector& Combination::get(void) { + return data; +} + +inline int Combination::getN(void) { + return n; +} + +inline int Combination::getR(void) { + return r; +} + +bool Combination::next(void) { + for (int i = r - 1; i >= 0; i--) { + if (data[i] < n - r + i) { + data[i]++; + for (int j = i + 1; j < r; j++) { + data[j] = data[j - 1] + 1; + } + return true; + } + } + return false; +} + +void Combination::next(int n) { + for (const auto& i : irange(n)) { + (void)i; + next(); + } +} + +int Combination::count(void) { + if (r > n - r) r = n - r; + int ans = 1; + + for (const auto& i : irange(1, r + 1)) { + ans *= n - r + i; + ans /= i; + } + + return ans; +} + +std::vector Combination::get_reverse(void) { + std::vector reverse_data = data; + for (const auto& i : irange(r)) { + reverse_data[i] = n - 1 - data[i]; + } + return reverse_data; +} + +std::vector Combination::get_reverse(int n) { + next(n); + return get_reverse(); +} + +void doDecomposition(TruthTable tt_, int nBoundSet, std::vector& supportSet, std::vector& record, std::vector >& recordCof) { + assert(nBoundSet <= supportSet.size()); + TruthTable tt = tt_.clone(); + Combination generator(supportSet.size(), nBoundSet); + + int genIndex = 0; + do { + std::vector combination = generator.get_reverse(); + // move bound set to MSB + for (const auto& i : irange(nBoundSet)) { + tt.moveTo(supportSet[combination[i]], tt.nVars() - i - 1); + } + std::vector cofactors; + std::vector boundSetFunctions; + int nCofactors = tt.countCofactor(nBoundSet, cofactors, boundSetFunctions, true); + for (auto& cofactor : cofactors) { + recordCof[genIndex].insert(cofactor.hash_str()); + recordCof[genIndex].insert((~cofactor).hash_str()); + } + record[genIndex++] += nCofactors; + } while (generator.next()); +} + +class DecisionDiagram; + +class DecisionNode { + friend class DecisionDiagram; + +public: + DecisionNode(); + void buildWithDecisionVariable(DecisionDiagram* mgr, int decisionVariable, bool shared = true, int fInv = 0); + +public: + TruthTable& getTruthTable(void); + +private: + static std::vector computeEntropyCost(DecisionDiagram* mgr, TruthTable& tt, std::set& invalid_variables); + std::set getInvalidVariables(DecisionDiagram* mgr, std::vector& available_variables); + +private: + int decisionVariable; + TruthTable tt; + int left; + int right; +}; + +inline DecisionNode::DecisionNode() + : decisionVariable(-1), left(-1), right(-1) { +} + +inline TruthTable& DecisionNode::getTruthTable(void) { + return tt; +} + +class DecisionDiagram { + friend class DecisionNode; + +public: + DecisionDiagram(); + +public: + unsigned randomInt(int fReset); + unsigned randomNum(int nSeed); + void addOutput(TruthTable& tt); + + void build(void); + void buildWithDecisionVariable(int node_id, int variable, std::set& newWaitingNodes, int fInv = 0); + void buildOneCluster(std::vector& cluster); + std::vector > buildClusters(std::vector waitingNodes); + std::vector computeSupportSet(std::vector& nodes); + std::vector buildWithTheseSupportWithEntropyAndFourier(std::vector& waitingNodes, std::set& supportSet); + +private: + void init(int nVars); + DecisionNode& getNode(int id) { + return node_pool[id]; + } + void prepareSpace(void); + int newNode(void); + int newNode(TruthTable& tt, bool shared = true, int fInv = 0); + int const0Node(void); + int const1Node(void); + float getEntropyCost(TruthTable& tt); + float getFourierCost(TruthTable& tt); + +public: + void writeVerilog(const char* filename); + void buildAig(Gia_Man_t *pAig); + +private: + void topoRec(int node, std::set& visited, std::vector& nodes); + void topoSort(int root, std::vector& nodes); + +private: + void printRec(int node, int space); + +public: + void print(void); + int nVars(void); + int nDecomp(void); + int nNodeAllocated(void) { return _num_node_allocated; } + +private: + int _nVars; + int _nDecomp; + int const0; + int _num_node_allocated; + std::vector node_pool; + std::vector roots; + std::unordered_map hash2node; + std::unordered_map hash2cost; + std::vector sortedNodes; +}; + +inline DecisionDiagram::DecisionDiagram() + : _nVars(0), _nDecomp(0), const0(0), _num_node_allocated(0) { + randomNum(1); +} + +inline int DecisionDiagram::nVars(void) { + return _nVars; +} + +inline int DecisionDiagram::nDecomp(void) { + return _nDecomp; +} + +inline int DecisionDiagram::const0Node(void) { + return const0; +} +inline int DecisionDiagram::const1Node(void) { + return LitNot(const0); +} + +void DecisionDiagram::init(int nVars) { + _nVars = nVars; + const0 = newNode(); + getNode(LitToId(const0)).decisionVariable = 0; + getNode(LitToId(const0)).right = -1; + getNode(LitToId(const0)).left = -1; + getNode(LitToId(const0)).tt = TruthTable(((uint64_t)1 << nVars)); + hash2node[getNode(LitToId(const0)).getTruthTable().hash_str()] = const0; + hash2node[(~(getNode(LitToId(const0)).getTruthTable())).hash_str()] = LitNot(const0); +} + +void DecisionDiagram::prepareSpace(void) { + if (_num_node_allocated + 2 > node_pool.size() / 2) { + // printf("\n\nPrepare node pool\n\n"); + node_pool.resize(node_pool.size() * 2); + } +} + +int DecisionDiagram::newNode(void) { + if (_num_node_allocated > node_pool.size() / 2) { + // printf("\n\nResizing node pool\n\n"); + node_pool.resize(node_pool.size() * 2); + } + + // printf("\n\nNEW NODE Allocating node %d\n\n", _num_node_allocated); + + return IdToLit(_num_node_allocated++, false); +} + +int DecisionDiagram::newNode(TruthTable& tt, bool shared, int fInv) { + (void)shared; + std::string hash_pos = tt.hash_str(); + auto iter = hash2node.begin(); + if ((iter = hash2node.find(hash_pos)) != hash2node.end()) { + return iter->second; + } + + int new_node = newNode(); + // printf("New node %d for TT ", LitToId(new_node)); + // tt.print(TruthTable::Format::BIN); + + if (fInv && tt.countOne() > tt.nBits() / 2) { + hash2node[hash_pos] = LitNot(new_node); + hash2node[(~tt).hash_str()] = new_node; + getNode(LitToId(new_node)).tt = ~tt; + return LitNot(new_node); + } else { + hash2node[hash_pos] = new_node; + hash2node[(~tt).hash_str()] = LitNot(new_node); + getNode(LitToId(new_node)).tt = tt; + return new_node; + } + return const0; +} + +void DecisionDiagram::addOutput(TruthTable& tt) { + if (node_pool.empty()) { + node_pool.resize((uint64_t)1 << tt.nVars()); + this->init(tt.nVars()); + } + roots.emplace_back(newNode(tt)); +} + +unsigned DecisionDiagram::randomInt(int fReset) { + static unsigned int m_z = 3716960521u; + static unsigned int m_w = 2174103536u; + if (fReset) { + m_z = 3716960521u; + m_w = 2174103536u; + } + m_z = 36969 * (m_z & 65535) + (m_z >> 16); + m_w = 18000 * (m_w & 65535) + (m_w >> 16); + return (m_z << 16) + m_w; +} + +unsigned DecisionDiagram::randomNum(int Seed) { + static unsigned RandMask = 0; + if (Seed == 0) + return RandMask ^ randomInt(0); + RandMask = randomInt(1); + for (int i = 0; i < Seed; i++) + RandMask = randomInt(0); + return RandMask; +} + +float DecisionDiagram::getFourierCost(TruthTable& tt) { + std::string hash_str = tt.hash_str(); + std::string neg_hash_str = (~tt).hash_str(); + if (hash2node.find(hash_str) != hash2node.end()) { + return 0; + } else if (hash2node.find(neg_hash_str) != hash2node.end()) { + return 0; + } + auto iter = hash2cost.begin(); + if ((iter = hash2cost.find(hash_str)) != hash2cost.end()) { + return iter->second; + } else if ((iter = hash2cost.find(neg_hash_str)) != hash2cost.end()) { + return iter->second; + } + + return hash2cost[hash_str] = tt.fourierCost(); +} + +float DecisionDiagram::getEntropyCost(TruthTable& tt) { + int out1 = tt.countOne(); + float p1 = (float)out1 / tt.nBits(); + float p0 = 1 - p1; + float entropy = -(((p0 != 0) ? p0 * log2(p0) : 0) + ((p1 != 0) ? p1 * log2(p1) : 0)); + + return entropy; +} + +std::set getInvalidVariables(DecisionDiagram* mgr, std::vector& available_variables) { + std::vector all_variable(mgr->nVars()); + std::iota(all_variable.begin(), all_variable.end(), 0); + std::set all_variable_set(all_variable.begin(), all_variable.end()); + std::set invalid_variables; + std::set_difference(all_variable_set.begin(), all_variable_set.end(), available_variables.begin(), available_variables.end(), std::inserter(invalid_variables, invalid_variables.begin())); + + return invalid_variables; +} + +std::vector DecisionNode::computeEntropyCost(DecisionDiagram* mgr, TruthTable& tt, std::set& invalid_variables) { + (void)mgr; + float oriInfo = mgr->getEntropyCost(tt); + + std::vector costs(tt.nVars(), 1024); + for (const auto& i : irange(tt.nVars())) { + if (invalid_variables.count(i)) continue; + auto cofactor0 = tt.cofactor(i, 1); + auto cofactor1 = tt.cofactor(i, 0); + if (cofactor0 == tt || cofactor1 == tt) { + continue; + } + int out1_0 = cofactor0.countOne(); + int out0_0 = cofactor0.nBits() - out1_0; + int out1_1 = cofactor1.countOne(); + int out0_1 = cofactor1.nBits() - out1_1; + float p1_0 = (float)out1_0 / (out1_0 + out0_0 + 1e-8); + float p0_0 = (float)out0_0 / (out1_0 + out0_0 + 1e-8); + float p1_1 = (float)out1_1 / (out1_1 + out0_1 + 1e-8); + float p0_1 = (float)out0_1 / (out1_1 + out0_1 + 1e-8); + int n0 = out1_0 + out0_0; + int n1 = out1_1 + out0_1; + int nAll = n0 + n1; + float info0 = ((float)n0 / nAll) * -(((p0_0 != 0) ? p0_0 * log2(p0_0) : 0) + ((p1_0 != 0) ? p1_0 * log2(p1_0) : 0)); + float info1 = ((float)n1 / nAll) * -(((p0_1 != 0) ? p0_1 * log2(p0_1) : 0) + ((p1_1 != 0) ? p1_1 * log2(p1_1) : 0)); + // printf("Decision variable: %d\n", i); + // printf("Ori: %f, Info0: %f, Info1: %f\n", oriInfo, info0, info1); + // printf("p0_0: %f, p1_0: %f, p0_1: %f, p1_1: %f\n", p0_0, p1_0, p0_1, p1_1); + costs[i] = -(oriInfo - info0 - info1); + } + + return costs; +} + +double jaccardSimilarity(const std::unordered_set& a, const std::unordered_set& b) { + std::unordered_set intersection, unionSet = a; + for (int num : b) { + if (a.count(num)) intersection.insert(num); + unionSet.insert(num); + } + return (double)intersection.size() / unionSet.size(); +} + +std::vector > autoClusterIndex(std::vector >& sequences, double threshold = 0.95) { + int n = sequences.size(); + std::vector > sets(n); + + for (int i = 0; i < n; i++) { + sets[i] = std::unordered_set(sequences[i].begin(), sequences[i].end()); + } + + std::vector > graph(n); + for (int i = 0; i < n; i++) { + for (int j = i + 1; j < n; j++) { + if (jaccardSimilarity(sets[i], sets[j]) >= threshold) { + graph[i].push_back(j); + graph[j].push_back(i); + } + } + } + + std::vector visited(n, false); + std::vector > clusters; + + std::function&)> dfs = [&](int node, std::vector& cluster) { + visited[node] = true; + cluster.push_back(node); + for (int neighbor : graph[node]) { + if (!visited[neighbor]) { + dfs(neighbor, cluster); + } + } + }; + + for (int i = 0; i < n; i++) { + if (!visited[i]) { + std::vector cluster; + dfs(i, cluster); + clusters.push_back(cluster); + } + } + + return clusters; +} + +std::vector > DecisionDiagram::buildClusters(std::vector waitingNodes) { + int nVars = getNode(waitingNodes[0]).getTruthTable().nVars(); + // compute support set + std::set supportSet; + std::vector supportCount(nVars, 0); + std::vector > supportSetVec(waitingNodes.size()); + for (const auto& i : irange(waitingNodes.size())) { + auto& node = getNode(waitingNodes[i]); + for (const auto& var : irange(nVars)) { + if (node.getTruthTable().hasVariable(var)) { + supportSet.insert(var); + supportCount[var]++; + supportSetVec[i].push_back(var); + } + } + } + + auto clustersIndex = autoClusterIndex(supportSetVec); + std::vector > clusters; + for (const auto& cluster : clustersIndex) { + std::vector newCluster; + for (const auto& index : cluster) { + if (waitingNodes[index] == LitToId(const0Node())) { // FIX + continue; + } + newCluster.push_back(waitingNodes[index]); + } + if (newCluster.empty()) { // FIX + continue; + } + clusters.push_back(newCluster); + } + + return clusters; +} + +void DecisionNode::buildWithDecisionVariable(DecisionDiagram* mgr, int decisionVariable, bool shared, int fInv) { + auto& tt = this->tt; + // terminate condition + if (this->left != -1 || this->right != -1) { + return; + } + + // set the decision variable and calculate the cofactor + // printf(" with decision variable %d\n", decisionVariable); + this->decisionVariable = decisionVariable; + auto ltt = tt.cofactor(decisionVariable, 0); + auto rtt = tt.cofactor(decisionVariable, 1); + // printf(" left: "); ltt.print(TruthTable::Format::BIN); + // printf(" right: "); rtt.print(TruthTable::Format::BIN); + if (tt == rtt || tt == ltt) { + return; + } + + // build the left and right child + left = mgr->newNode(ltt, shared, fInv); + right = mgr->newNode(rtt, shared, fInv); + // printf(" left id: %d, right id: %d\n", LitToId(left), LitToId(right)); + // printf(" left check: "); if (LitToId(left) != 0) { mgr->getNode(LitToId(left)).getTruthTable().print(TruthTable::Format::BIN); } else { printf("NULL\n"); } + // printf(" right check: "); if (LitToId(right) != 0) { mgr->getNode(LitToId(right)).getTruthTable().print(TruthTable::Format::BIN); } else { printf("NULL\n"); } +} + +void DecisionDiagram::buildWithDecisionVariable(int node_id, int variable, std::set& newWaitingNodes, int fInv) { + prepareSpace(); + auto& node = getNode(node_id); + if (node.left != -1 || node.right != -1) { + return; + } + // printf("Build node %d: ", node_id); node.getTruthTable().print(TruthTable::Format::BIN); + node.buildWithDecisionVariable(this, variable, true, fInv); + if (node.left == -1 && node.right == -1) { + newWaitingNodes.insert(node_id); + return; + } + if (!fInv) { + if (!LitIsComplement(node.left) && (node.left != const0Node())) { + // printf("Insert left node id %d\n", LitToId(node.left)); + newWaitingNodes.insert(LitToId(node.left)); + } + if (!LitIsComplement(node.right) && (node.right != const0Node())) { + // printf("Insert right node id %d\n", LitToId(node.right)); + newWaitingNodes.insert(LitToId(node.right)); + } + } else { + if (node.left != const0Node() && node.left != const1Node()) { + newWaitingNodes.insert(LitToId(node.left)); + } + if (node.right != const0Node() && node.right != const1Node()) { + newWaitingNodes.insert(LitToId(node.right)); + } + } + + // printf(" newWaitingNodes: \n"); + // for (const auto& n : newWaitingNodes) { + // printf("%d ", n); + // getNode(n).getTruthTable().print(TruthTable::Format::BIN); + // } + // printf("\n"); +} + +std::vector DecisionDiagram::computeSupportSet(std::vector& nodes) { + std::set supportSet; + for (const auto& node_id : nodes) { + auto& node = getNode(node_id); + for (const auto& var : irange(node.getTruthTable().nVars())) { + if (node.getTruthTable().hasVariable(var)) { + supportSet.insert(var); + } + } + } + return std::vector(supportSet.begin(), supportSet.end()); +} + +template +float min(std::vector& array) { + return *std::min_element(array.begin(), array.end()); +} + +void DecisionDiagram::build(void) { + std::vector trueNodeIds; + for (const auto& root : roots) { + int root_id = LitToId(root); + if (std::find(trueNodeIds.begin(), trueNodeIds.end(), root) == trueNodeIds.end()) + trueNodeIds.emplace_back(root_id); + } + std::vector waitingNodes = trueNodeIds; + + auto clusters = buildClusters(waitingNodes); + for (auto& cluster : clusters) { + // printf("cluster: "); + // for (auto& c : cluster) { + // printf("%d ", c); + // } + // printf("\n"); + buildOneCluster(cluster); + } + + // topo sort + std::set visited; + for (const auto& root : roots) { + this->topoRec(LitToId(root), visited, this->sortedNodes); + } +} + +std::vector DecisionDiagram::buildWithTheseSupportWithEntropyAndFourier(std::vector& waitingNodes, std::set& supportSet) { + int nVars = getNode(waitingNodes[0]).getTruthTable().nVars(); + std::set invalid_variables; + for (const auto& i : irange(nVars)) { + if (supportSet.find(i) == supportSet.end()) { + invalid_variables.insert(i); + } + } + while (!waitingNodes.empty() && !supportSet.empty()) { + // compute gain + std::vector costs(nVars, 1024); + for (const auto& nodeId : waitingNodes) { + auto& node = getNode(nodeId); + auto cost = DecisionNode::computeEntropyCost(this, node.getTruthTable(), invalid_variables); + // ::print(cost); + for (const auto& i : irange(nVars)) { + costs[i] += (cost[i] == 1024) ? 0 : cost[i]; + } + } + + // find decision variable + std::vector decisionSet; + int decisionVariable = std::distance(costs.begin(), std::min_element(costs.begin(), costs.end())); + float decisionCost = costs[decisionVariable]; + for (const auto& i : irange(nVars)) { + if (costs[i] == decisionCost && !invalid_variables.count(i)) { + decisionSet.push_back(i); + } + } + if (min(costs) == 1024) { + decisionVariable = *supportSet.begin(); + } + if (decisionSet.size() > 1) { + std::vector fouerierCost(decisionSet.size(), 0); + for (const auto& nodeId : waitingNodes) { + auto& node = getNode(nodeId); + std::vector cost(decisionSet.size(), 8192); + for (const auto& i : irange(decisionSet.size())) { + if (invalid_variables.find(decisionSet[i]) != invalid_variables.end()) continue; + // consider two childs + auto cofactor0 = node.getTruthTable().cofactor(decisionSet[i], 1); + auto cofactor1 = node.getTruthTable().cofactor(decisionSet[i], 0); + if (cofactor0 == node.getTruthTable() || cofactor1 == node.getTruthTable()) { + continue; + } + cost[i] = getFourierCost(cofactor0) + getFourierCost(cofactor1); + } + for (const auto& i : irange(decisionSet.size())) { + fouerierCost[i] += cost[i]; + } + } + int decisionIndex = std::distance(fouerierCost.begin(), std::min_element(fouerierCost.begin(), fouerierCost.end())); + decisionVariable = decisionSet[decisionIndex]; + } + std::set new_waiting_nodes; + for (const auto& nodeId : waitingNodes) { + buildWithDecisionVariable(nodeId, decisionVariable, new_waiting_nodes); + } + waitingNodes = std::vector(new_waiting_nodes.begin(), new_waiting_nodes.end()); + invalid_variables.insert(decisionVariable); + supportSet.erase(decisionVariable); + } + return waitingNodes; +} + +void DecisionDiagram::buildOneCluster(std::vector& cluster) { + int enableFourier = 1; + int enableDecompose = 1; + + std::vector waiting_nodes = cluster; + + int nVars = getNode(cluster[0]).getTruthTable().nVars(); + while (!waiting_nodes.empty()) { + // printf("=========================\n"); + // printf("construct nodes: \n"); + // for (auto node : waiting_nodes) { + // printf("Node %d: ", node); + // getNode(node).getTruthTable().print(TruthTable::Format::BIN); + // } + // printf("-------------------------\n"); + // compute support set + std::vector supportSet = computeSupportSet(waiting_nodes); + std::set invalid_variables = getInvalidVariables(this, supportSet); + // printf("Support set: "); + // for (const auto& var : supportSet) { + // printf("%d ", var); + // } + // printf("\n"); + // printf("Invalid set: "); + // for (const auto& var : invalid_variables) { + // printf("%d ", var); + // } + // printf("\n"); + + // compute multi-output decomposition + // if the multi-output decomposition exist, then build the nodes + int nBoundSet = std::max(2, std::min(4, (int)supportSet.size())); + if (supportSet.size() > nBoundSet && enableDecompose) { + // printf("Try to decompose with bound set size %d\n", nBoundSet); + std::vector record(Combination(supportSet.size(), nBoundSet).count(), 0); + std::vector > recordCofoactor(Combination(supportSet.size(), nBoundSet).count()); + for (const auto& nodeIndex : waiting_nodes) { + auto& node = getNode(nodeIndex); + doDecomposition(node.getTruthTable(), nBoundSet, supportSet, record, recordCofoactor); + } + auto record_copy = record; + for (const auto& i : irange(recordCofoactor.size())) { + record[i] = recordCofoactor[i].size(); + } + int minRecord = *std::min_element(record.begin(), record.end()); + if (minRecord < (1 << nBoundSet) * 3 / 4) { + std::vector minRecordIndex; + std::vector ref; + for (const auto& i : irange(record.size())) { + if (record[i] == minRecord) { + minRecordIndex.push_back(i); + ref.push_back(record_copy[i]); + } + } + std::set unionSet; + for (const auto& index : minRecordIndex) { + auto comb = Combination(supportSet.size(), nBoundSet).get_reverse(index); + for (const auto& i : comb) { + unionSet.insert(supportSet[i]); + } + } + if (unionSet.size() == nBoundSet && min(ref) > nBoundSet) { + waiting_nodes = buildWithTheseSupportWithEntropyAndFourier(waiting_nodes, unionSet); + continue; + } + supportSet = std::vector(unionSet.begin(), unionSet.end()); + } + } + + int decisionVariable = 0; + // compute gain + std::vector costs(nVars, 1024); + for (const auto& nodeId : waiting_nodes) { + auto& node = getNode(nodeId); + auto cost = DecisionNode::computeEntropyCost(this, node.getTruthTable(), invalid_variables); + for (const auto& i : irange(nVars)) { + costs[i] += (cost[i] == 1024) ? 0 : cost[i]; + } + } + // printf("Costs: "); + // for (const auto& cost : costs) { + // printf("%f ", cost); + // } + // printf("\n"); + + // find decision variable + std::vector decisionSet; + decisionVariable = std::distance(costs.begin(), std::min_element(costs.begin(), costs.end())); + float decisionCost = costs[decisionVariable]; + for (const auto& i : irange(nVars)) { + if (costs[i] == decisionCost && !invalid_variables.count(i)) { + decisionSet.push_back(i); + } + } + if (min(costs) == 1024) { + decisionVariable = supportSet[0]; + } + // printf("First decision variable: %d\n", decisionVariable); + if (decisionSet.size() > 1 && enableFourier) { + std::vector fouerierCost(decisionSet.size(), 0); + for (const auto& nodeId : waiting_nodes) { + auto& node = getNode(nodeId); + std::vector cost(decisionSet.size(), 8192); + for (const auto& i : irange(decisionSet.size())) { + if (invalid_variables.find(decisionSet[i]) != invalid_variables.end()) continue; + // consider two childs + auto cofactor0 = node.getTruthTable().cofactor(decisionSet[i], 1); + auto cofactor1 = node.getTruthTable().cofactor(decisionSet[i], 0); + if (cofactor0 == node.getTruthTable() || cofactor1 == node.getTruthTable()) { + continue; + } + cost[i] = getFourierCost(cofactor0) + getFourierCost(cofactor1); + } + for (const auto& i : irange(decisionSet.size())) { + fouerierCost[i] += cost[i]; + } + } + int decisionIndex = std::distance(fouerierCost.begin(), std::min_element(fouerierCost.begin(), fouerierCost.end())); + decisionVariable = decisionSet[decisionIndex]; + // printf("Second decision variable: %d\n", decisionVariable); + } + + std::set next_waiting_nodes; + for (const auto& nodeId : waiting_nodes) { + buildWithDecisionVariable(nodeId, decisionVariable, next_waiting_nodes, 0); + + // printf("Check every nodes:\n"); + // for (int i = 0; i < _num_node_allocated; i++) { + // printf("Node id %d: left %d right %d\n", i, getNode(i).left, getNode(i).right); + // getNode(i).getTruthTable().print(TruthTable::Format::BIN); + // } + // printf("\n"); + + } + // for (auto next_node : next_waiting_nodes) { + // printf("Next waiting node: "); + // getNode(next_node).getTruthTable().print(TruthTable::Format::BIN); + // } + + waiting_nodes = std::vector(next_waiting_nodes.begin(), next_waiting_nodes.end()); + // printf("=========================\n\n"); + } +} + +void DecisionDiagram::topoRec(int node, std::set& visited, std::vector& nodes) { + if (visited.find(node) != visited.end() || node == const0) { + return; + } + visited.insert(node); + if (getNode(node).left != -1) { + topoRec(LitToId(getNode(node).left), visited, nodes); + } + if (getNode(node).right != -1) { + topoRec(LitToId(getNode(node).right), visited, nodes); + } + nodes.push_back(node); +} + +void DecisionDiagram::topoSort(int root, std::vector& nodes) { + std::set visited; + topoRec(root, visited, nodes); +} + +void DecisionDiagram::printRec(int root_, int space) { + int root = LitToId(root_); + bool is_complement = LitIsComplement(root_); + // Base case + if (root == const0) + return; + + // Increase distance between levels + space += 11; + + // Process right child first + if (getNode(root).right == -1) return; + printRec(getNode(root).right, space); + + // Print current node after space + printf("\n"); + for (int i = 11; i < space; i++) + printf(" "); + if (root == const0Node()) { + if (is_complement) { + printf("CONST1\n"); + } else { + printf("CONST0\n"); + } + } else { + printf("%sMUX[%2d](%2d)\n", (is_complement) ? "~" : "", getNode(root).decisionVariable, root); + } + + // Process left child + if (getNode(root).left == root) return; + printRec(getNode(root).left, space); +} + +void DecisionDiagram::print(void) { + // Pass initial space count as 0 + for (const auto& root : roots) + printRec(root, 0); +} + +void DecisionDiagram::writeVerilog(const char* filename) { + if (roots.size() == 0) { + printf("[ERROR] Empty network\n"); + return; + } + FILE* f = fopen(filename, "w"); + if (f == NULL) { + printf("[ERROR] Cannot open file %s\n", filename); + return; + } + fprintf(f, "module decision_diagram("); + for (const auto& i : irange(getNode(LitToId(roots[0])).tt.nVars())) { + fprintf(f, "in_%u, ", i); + } + for (const auto& i : irange(roots.size() - 1)) { + fprintf(f, "output_%lu, ", i); + } + fprintf(f, "output_%zu);\n", roots.size() - 1); + for (const auto& i : irange(getNode(LitToId(roots[0])).tt.nVars())) { + fprintf(f, "input in_%d;\n", i); + } + for (const auto& i : irange(roots.size())) { + fprintf(f, "output output_%lu;\n", i); + } + fprintf(f, "wire node_%d = 0;\n", const0); + for (const auto& node : sortedNodes) { + fprintf(f, "wire node_%d;\n", node); + } + + for (const auto& node : sortedNodes) { + std::string decisionVariable = "in_" + std::to_string(getNode(node).decisionVariable); + + if (getNode(node).left == -1 || getNode(node).right == -1) continue; + + int lhs = LitToId(getNode(node).left); + bool is_lhs_const = (lhs == const0); + bool is_lhs_complement = LitIsComplement(getNode(node).left); + int rhs = LitToId(getNode(node).right); + bool is_rhs_const = (rhs == const0); + bool is_rhs_complement = LitIsComplement(getNode(node).right); + if (is_lhs_const && !is_lhs_complement && is_rhs_const && !is_rhs_complement) { + fprintf(f, "assign node_%d = 0;\n", node); + } else if (is_lhs_const && is_lhs_complement && is_rhs_const && is_rhs_complement) { + fprintf(f, "assign node_%d = 1;\n", node); + } else if (is_lhs_const && is_lhs_complement && is_rhs_const && !is_rhs_complement) { + fprintf(f, "assign node_%d = %s;\n", node, decisionVariable.c_str()); + } else if (is_lhs_const && !is_lhs_complement && is_rhs_const && is_rhs_complement) { + fprintf(f, "assign node_%d = ~%s;\n", node, decisionVariable.c_str()); + } else if (!is_lhs_const && is_rhs_const && !is_rhs_complement) { + fprintf(f, "assign node_%d = %s & %snode_%d;\n", node, decisionVariable.c_str(), (is_lhs_complement) ? "~" : "", lhs); + } else if (!is_rhs_const && is_lhs_const && !is_lhs_complement) { + fprintf(f, "assign node_%d = ~%s & %snode_%d;\n", node, decisionVariable.c_str(), (is_rhs_complement) ? "~" : "", rhs); + } else if (is_lhs_const && is_lhs_complement && !is_rhs_const) { + fprintf(f, "assign node_%d = %s | %snode_%d;\n", node, decisionVariable.c_str(), (is_rhs_complement) ? "~" : "", rhs); + } else if (is_rhs_const && is_rhs_complement && !is_lhs_const) { + fprintf(f, "assign node_%d = ~%s | %snode_%d;\n", node, decisionVariable.c_str(), (is_lhs_complement) ? "~" : "", lhs); + } else { + fprintf(f, "assign node_%d = (%s) ? %snode_%d : %snode_%d;\n", node, decisionVariable.c_str(), (is_lhs_complement) ? "~" : "", lhs, (is_rhs_complement) ? "~" : "", rhs); + } + } + + for (const auto& i : irange(roots.size())) { + int root = LitToId(roots[i]); + bool is_complement = LitIsComplement(roots[i]); + fprintf(f, "assign output_%lu = %snode_%d;\n", i, (is_complement) ? "~" : "", root); + } + + fprintf(f, "endmodule\n"); + fclose(f); +} + +void DecisionDiagram::buildAig(Gia_Man_t *pAig) { + if (roots.size() == 0) { + printf("[ERROR] Empty network\n"); + return; + } + + std::vector copy(sortedNodes.size() + 1, -1); + copy[const0] = Gia_ManConst0Lit(); + for (const auto& node : sortedNodes) { + // printf("node id %d: left %d right %d\n", node, getNode(node).left, getNode(node).right); + if (getNode(node).left == -1 || getNode(node).right == -1) continue; + + int lhs = LitToId(getNode(node).left); + bool is_lhs_const = (lhs == const0); + bool is_lhs_complement = LitIsComplement(getNode(node).left); + int rhs = LitToId(getNode(node).right); + bool is_rhs_const = (rhs == const0); + bool is_rhs_complement = LitIsComplement(getNode(node).right); + // printf("lhs: %s%d rhs: %s%d\n", (is_lhs_complement) ? "~" : "", lhs, (is_rhs_complement) ? "~" : "", rhs); + if (is_lhs_const && !is_lhs_complement && is_rhs_const && !is_rhs_complement) { + copy[node] = Gia_ManConst0Lit(); + } else if (is_lhs_const && is_lhs_complement && is_rhs_const && is_rhs_complement) { + copy[node] = Gia_ManConst1Lit(); + } else if (is_lhs_const && is_lhs_complement && is_rhs_const && !is_rhs_complement) { + copy[node] = Gia_ManCiLit(pAig, getNode(node).decisionVariable); + } else if (is_lhs_const && !is_lhs_complement && is_rhs_const && is_rhs_complement) { + copy[node] = LitNot(Gia_ManCiLit(pAig, getNode(node).decisionVariable)); + } else if (!is_lhs_const && is_rhs_const && !is_rhs_complement) { + copy[node] = Gia_ManHashAnd(pAig, Gia_ManCiLit(pAig, getNode(node).decisionVariable), LitNotCond(copy[lhs], is_lhs_complement)); + } else if (!is_rhs_const && is_lhs_const && !is_lhs_complement) { + copy[node] = Gia_ManHashAnd(pAig, LitNot(Gia_ManCiLit(pAig, getNode(node).decisionVariable)), LitNotCond(copy[rhs], is_rhs_complement)); + } else if (is_lhs_const && is_lhs_complement && !is_rhs_const) { + copy[node] = Gia_ManHashOr(pAig, Gia_ManCiLit(pAig, getNode(node).decisionVariable), LitNotCond(copy[rhs], is_rhs_complement)); + } else if (is_rhs_const && is_rhs_complement && !is_lhs_const) { + copy[node] = Gia_ManHashOr(pAig, LitNot(Gia_ManCiLit(pAig, getNode(node).decisionVariable)), LitNotCond(copy[lhs], is_lhs_complement)); + } else { + copy[node] = Gia_ManHashMux(pAig, Gia_ManCiLit(pAig, getNode(node).decisionVariable), LitNotCond(copy[lhs], is_lhs_complement), LitNotCond(copy[rhs], is_rhs_complement)); + } + } + + for (const auto& i : irange(roots.size())) { + int root_id = LitToId(roots[i]); + bool is_complement = LitIsComplement(roots[i]); + Gia_ManAppendCo(pAig, LitNotCond(copy[root_id], is_complement)); + } +} + +} // namespace DecGraph + +Gia_Man_t* Gia_ManDecGraph(Gia_Man_t* p) { + int nIns = Gia_ManCiNum(p); + int nOuts = Gia_ManCoNum(p); + Gia_Man_t* pNew; + Gia_Obj_t* pObj; + word v; + word* pTruth; + int i, k; + Gia_ManLevelNum(p); + pNew = Gia_ManStart(Gia_ManObjNum(p)); + pNew->pName = Abc_UtilStrsav(p->pName); + pNew->pSpec = Abc_UtilStrsav(p->pSpec); + Gia_ManForEachCi(p, pObj, k) + Gia_ManAppendCi(pNew); + Gia_ObjComputeTruthTableStart(p, nIns); + Gia_ManHashStart(pNew); + DecGraph::DecisionDiagram dd; + for (k = 0; k < nOuts; k++) { + DecGraph::TruthTable tt; + tt.create(1lu << nIns); + int num_words = tt.nWords(); + pObj = Gia_ManCo(p, k); + pTruth = Gia_ObjComputeTruthTable(p, Gia_ObjFanin0(pObj)); + if (nIns >= 6) { + for (i = num_words - 1; i >= 0; --i) { + tt.data()[i] = Gia_ObjFaninC0(pObj) ? ~DecGraph::reverseBits(pTruth[i]) : DecGraph::reverseBits(pTruth[i]); + } + } else { + v = DecGraph::reverseBits((Gia_ObjFaninC0(pObj) ? ~pTruth[0] : pTruth[0]) & DecGraph::ones_mask[nIns]); + tt.data()[0] = v; + } + dd.addOutput(tt); + } + dd.build(); + dd.buildAig(pNew); + Gia_ObjComputeTruthTableStop(p); + Gia_ManHashStop(pNew); + Gia_ManSetRegNum(pNew, Gia_ManRegNum(p)); + return pNew; +} + +extern "C" { +extern char * Extra_FileReadContents( char * pFileName ); +} + +Gia_Man_t* Gia_ManDecGraphFromFile(char* pFileName) { + char* pBuffer = Extra_FileReadContents(pFileName); + + char *table = strtok(pBuffer, " \r\n\t|"); + DecGraph::DecisionDiagram dd; + while (table) { + if (strlen(table) == 0) { + break; + } + DecGraph::TruthTable tt; + tt.readBinaryReverse(table); + dd.addOutput(tt); + table = strtok(NULL, " \r\n\t|"); + } + + free(pBuffer); + + dd.build(); + + Gia_Man_t* pNew = Gia_ManStart(dd.nNodeAllocated()); + pNew->pName = Abc_UtilStrsav("top"); + for (int i = 0; i < dd.nVars(); ++i) + Gia_ManAppendCi(pNew); + Gia_ManHashStart(pNew); + + dd.buildAig(pNew); + return pNew; +} + +ABC_NAMESPACE_IMPL_END diff --git a/src/aig/gia/module.make b/src/aig/gia/module.make index b4e2efb8b..ebc39b1f6 100644 --- a/src/aig/gia/module.make +++ b/src/aig/gia/module.make @@ -113,4 +113,5 @@ SRC += src/aig/gia/giaAig.c \ src/aig/gia/giaTtopt.cpp \ src/aig/gia/giaUnate.c \ src/aig/gia/giaUtil.c \ - src/aig/gia/giaBound.c + src/aig/gia/giaBound.c \ + src/aig/gia/giaDecGraph.cpp diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c index 159b0a0f7..81a5f4478 100644 --- a/src/base/abci/abc.c +++ b/src/base/abci/abc.c @@ -532,6 +532,7 @@ static int Abc_CommandAbc9Transduction ( Abc_Frame_t * pAbc, int argc, cha static int Abc_CommandAbc9TranStoch ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandAbc9Rrr ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandAbc9Rewire ( Abc_Frame_t * pAbc, int argc, char ** argv ); +static int Abc_CommandAbc9DecGraph ( Abc_Frame_t * pAbc, int argc, char ** argv ); //#endif static int Abc_CommandAbc9LNetMap ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandAbc9Unmap ( Abc_Frame_t * pAbc, int argc, char ** argv ); @@ -1352,6 +1353,7 @@ void Abc_Init( Abc_Frame_t * pAbc ) Cmd_CommandAdd( pAbc, "ABC9", "&transtoch" , Abc_CommandAbc9TranStoch, 0 ); Cmd_CommandAdd( pAbc, "ABC9", "&rrr", Abc_CommandAbc9Rrr, 0 ); Cmd_CommandAdd( pAbc, "ABC9", "&rewire" , Abc_CommandAbc9Rewire, 0 ); + Cmd_CommandAdd( pAbc, "ABC9", "&dg" , Abc_CommandAbc9DecGraph, 0 ); //#endif Cmd_CommandAdd( pAbc, "ABC9", "&lnetmap", Abc_CommandAbc9LNetMap, 0 ); Cmd_CommandAdd( pAbc, "ABC9", "&unmap", Abc_CommandAbc9Unmap, 0 ); @@ -46972,6 +46974,80 @@ usage: return 1; } +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Abc_CommandAbc9DecGraph( Abc_Frame_t * pAbc, int argc, char ** argv ) +{ + Gia_Man_t * pTemp; + char * pFileName = NULL; + int c, fFile = 0; + + Extra_UtilGetoptReset(); + while ( ( c = Extra_UtilGetopt( argc, argv, "fh" ) ) != EOF ) + { + switch ( c ) + { + case 'f': + fFile ^= 1; + break; + case 'h': + default: + goto usage; + } + } + if ( argc > globalUtilOptind + 1 ) + { + return 0; + } + if ( !fFile && argc == globalUtilOptind + 1 ) + { + return 0; + } + if ( !fFile && pAbc->pGia == NULL ) + { + Abc_Print( -1, "Empty GIA network.\n" ); + return 1; + } + if ( fFile && argc == globalUtilOptind + 1 ) + { + FILE * pFile = fopen( argv[globalUtilOptind], "rb" ); + if ( pFile == NULL ) + { + Abc_Print( -1, "Abc_CommandAbc9BCore(): Cannot open file \"%s\" for reading the simulation information.\n", argv[globalUtilOptind] ); + return 0; + } + fclose( pFile ); + pFileName = argv[globalUtilOptind]; + } + if ( pFileName ) { + pTemp = Gia_ManDecGraphFromFile( pFileName ); + } else { + pTemp = Gia_ManDecGraph( pAbc->pGia ); + } + Abc_FrameUpdateGia( pAbc, pTemp ); + return 0; + +usage: + Abc_Print( -2, "usage: &dg [-vhf] \n" ); + Abc_Print( -2, "\t convert AIG into decision graph structure\n" ); + Abc_Print( -2, "\t-f : read from file (in IWLS format) [default = %s]\n" , fFile ? "yes" : "no"); + Abc_Print( -2, "\t-h : prints the command usage\n\n"); + Abc_Print( -2, "\t This command was contributed by Jiun-Hao Chen from National Taiwan University.\n" ); + Abc_Print( -2, "\t For more info, please refer to the paper: Jiun-Hao Chen and Jie-Hong R. Jiang,\n"); + Abc_Print( -2, "\t \"Circuit learning for multi-output Boolean functions\", Proc. IWLS 2025.\n"); + Abc_Print( -2, "\t https://people.eecs.berkeley.edu/~alanmi/publications/other/iwls25_dg.pdf\n"); + return 1; +} + /**Function************************************************************* Synopsis [] From f39b84a4a1d2ff4ac26d954148e8a2dd09a8da03 Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Wed, 22 Oct 2025 11:24:18 -0700 Subject: [PATCH 02/17] Fixing compilation problem. --- src/aig/gia/giaDecGraph.cpp | 5 +---- 1 file changed, 1 insertion(+), 4 deletions(-) diff --git a/src/aig/gia/giaDecGraph.cpp b/src/aig/gia/giaDecGraph.cpp index 01a7101c6..0efbe7bf8 100644 --- a/src/aig/gia/giaDecGraph.cpp +++ b/src/aig/gia/giaDecGraph.cpp @@ -41,6 +41,7 @@ #include "gia.h" #include "misc/vec/vecHash.h" +#include "misc/extra/extra.h" ABC_NAMESPACE_IMPL_START @@ -2180,10 +2181,6 @@ Gia_Man_t* Gia_ManDecGraph(Gia_Man_t* p) { return pNew; } -extern "C" { -extern char * Extra_FileReadContents( char * pFileName ); -} - Gia_Man_t* Gia_ManDecGraphFromFile(char* pFileName) { char* pBuffer = Extra_FileReadContents(pFileName); From 6fb4f739b0bfd2bf21bb738c99d092688d9932cf Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Fri, 24 Oct 2025 10:58:38 -0700 Subject: [PATCH 03/17] Suppress a warning about uninitialized variable. --- src/map/if/acd/ac_decomposition.hpp | 15 +++++++++------ 1 file changed, 9 insertions(+), 6 deletions(-) diff --git a/src/map/if/acd/ac_decomposition.hpp b/src/map/if/acd/ac_decomposition.hpp index 55097a453..8d5ddb5c4 100644 --- a/src/map/if/acd/ac_decomposition.hpp +++ b/src/map/if/acd/ac_decomposition.hpp @@ -512,17 +512,16 @@ private: } while ( combinations_offset_next( free_set_size, offset, pComb, pInvPerm, tt ) ); std::array res_perm; + for ( uint32_t i = 0; i < num_vars; ++i ) + { + res_perm[i] = permutations[bestPerm[i]]; + } if ( best_cost > ( 1 << ( ps.lut_size - free_set_size ) ) ) { return std::make_tuple( local_best_tt, res_perm, UINT32_MAX ); } - for ( uint32_t i = 0; i < num_vars; ++i ) - { - res_perm[i] = permutations[bestPerm[i]]; - } - return std::make_tuple( local_best_tt, res_perm, best_cost ); } @@ -544,7 +543,11 @@ private: } /* enumerate combinations */ - std::array res_perm; + std::array res_perm; + for ( uint32_t i = 0; i < num_vars; ++i ) + { + res_perm[i] = permutations[pComb[i]]; + } do { From 4c6b0824631e26749ee62c5b1beb2b34f01d454e Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Fri, 24 Oct 2025 10:59:56 -0700 Subject: [PATCH 04/17] Reusing switch "-j" in "if" and "&if". --- src/base/abci/abc.c | 14 +++++----- src/map/if/if.h | 1 + src/map/if/ifDecJ.c | 60 ++++++++++++++++++++++++++++++++++++++++++ src/map/if/module.make | 1 + 4 files changed, 69 insertions(+), 7 deletions(-) create mode 100644 src/map/if/ifDecJ.c diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c index 81a5f4478..688ea3e96 100644 --- a/src/base/abci/abc.c +++ b/src/base/abci/abc.c @@ -21845,7 +21845,7 @@ int Abc_CommandIf( Abc_Frame_t * pAbc, int argc, char ** argv ) Abc_Print( -1, "This feature only works for {6,7}-LUTs.\n" ); return 1; } - pPars->pFuncCell = If_CutPerformCheck07; + pPars->pFuncCell = If_CutPerformCheckJ; pPars->fCutMin = 1; } if ( pPars->fUseCofVars ) @@ -43180,12 +43180,12 @@ int Abc_CommandAbc9If( Abc_Frame_t * pAbc, int argc, char ** argv ) //pPars->fUseCofVars ^= 1; pPars->fUseCheck2 ^= 1; break; -// case 'j': -// pPars->fEnableCheck07 ^= 1; -// break; case 'j': - pPars->fUseAndVars ^= 1; + pPars->fEnableCheck07 ^= 1; break; + //case 'j': + // pPars->fUseAndVars ^= 1; + // break; case 'k': pPars->fUseDsdTune ^= 1; break; @@ -43288,7 +43288,7 @@ int Abc_CommandAbc9If( Abc_Frame_t * pAbc, int argc, char ** argv ) Abc_Print( -1, "This feature only works for {6,7}-LUTs.\n" ); return 1; } - pPars->pFuncCell = If_CutPerformCheck07; + pPars->pFuncCell = If_CutPerformCheckJ; pPars->fCutMin = 1; } if ( pPars->fUseCheck1 || pPars->fUseCheck2 ) @@ -43569,7 +43569,7 @@ usage: Abc_Print( -2, "\t-f : toggles enabling additional check [default = %s]\n", pPars->fEnableCheck75? "yes": "no" ); Abc_Print( -2, "\t-u : toggles enabling additional check [default = %s]\n", pPars->fEnableCheck75u? "yes": "no" ); Abc_Print( -2, "\t-i : toggles using cofactoring variables [default = %s]\n", pPars->fUseCofVars? "yes": "no" ); -// Abc_Print( -2, "\t-j : toggles enabling additional check [default = %s]\n", pPars->fEnableCheck07? "yes": "no" ); + Abc_Print( -2, "\t-j : toggles enabling additional check [default = %s]\n", pPars->fEnableCheck07? "yes": "no" ); Abc_Print( -2, "\t-j : toggles using AND bi-decomposition [default = %s]\n", pPars->fUseAndVars? "yes": "no" ); Abc_Print( -2, "\t-k : toggles matching based on precomputed DSD manager [default = %s]\n", pPars->fUseDsdTune? "yes": "no" ); Abc_Print( -2, "\t-z : toggles deriving LUTs when mapping into LUT structures [default = %s]\n", pPars->fDeriveLuts? "yes": "no" ); diff --git a/src/map/if/if.h b/src/map/if/if.h index e638b80da..9056d1f1f 100644 --- a/src/map/if/if.h +++ b/src/map/if/if.h @@ -560,6 +560,7 @@ extern int If_CutPerformCheckXX( If_Man_t * p, unsigned * pTruth, in extern int If_CutPerformCheck45( If_Man_t * p, unsigned * pTruth, int nVars, int nLeaves, char * pStr ); extern int If_CutPerformCheck54( If_Man_t * p, unsigned * pTruth, int nVars, int nLeaves, char * pStr ); extern int If_CutPerformCheck75( If_Man_t * p, unsigned * pTruth, int nVars, int nLeaves, char * pStr ); +extern int If_CutPerformCheckJ( If_Man_t * p, unsigned * pTruth, int nVars, int nLeaves, char * pStr ); extern float If_CutDelayLutStruct( If_Man_t * p, If_Cut_t * pCut, char * pStr, float WireDelay ); // extern int If_CutPerformAcd( If_Man_t * p, unsigned nVars, int lutSize, unsigned * pdelay, int use_late_arrival, unsigned * cost ); extern int If_CluCheckExt( void * p, word * pTruth, int nVars, int nLutLeaf, int nLutRoot, diff --git a/src/map/if/ifDecJ.c b/src/map/if/ifDecJ.c new file mode 100644 index 000000000..d77640ee0 --- /dev/null +++ b/src/map/if/ifDecJ.c @@ -0,0 +1,60 @@ +/**CFile**************************************************************** + + FileName [ifDec07.c] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [FPGA mapping based on priority cuts.] + + Synopsis [Performs additional check.] + + Author [Alan Mishchenko] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - November 21, 2006.] + + Revision [$Id: ifDec07.c,v 1.00 2006/11/21 00:00:00 alanmi Exp $] + +***********************************************************************/ + +#include "if.h" + +ABC_NAMESPACE_IMPL_START + +//////////////////////////////////////////////////////////////////////// +/// DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + +/**Function************************************************************* + + Synopsis [Performs additional check.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int If_CutPerformCheckJ( If_Man_t * p, unsigned * pTruth, int nVars, int nLeaves, char * pStr ) +{ + int v; + // skip non-support minimal + for ( v = 0; v < nLeaves; v++ ) + if ( !Abc_TtHasVar( (word *)pTruth, nVars, v ) ) + return 0; + return 1; +} + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + + +ABC_NAMESPACE_IMPL_END + diff --git a/src/map/if/module.make b/src/map/if/module.make index bd652f35b..96c90cab8 100644 --- a/src/map/if/module.make +++ b/src/map/if/module.make @@ -9,6 +9,7 @@ SRC += src/map/if/ifCom.c \ src/map/if/ifDec16.c \ src/map/if/ifDec66.c \ src/map/if/ifDec75.c \ + src/map/if/ifDecJ.c \ src/map/if/ifDelay.c \ src/map/if/ifDsd.c \ src/map/if/ifLibBox.c \ From 3a1efd48f72ac916d954035fc166d6d76efe198f Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Fri, 24 Oct 2025 11:46:55 -0700 Subject: [PATCH 05/17] Enabling multiple LUT libraries. --- src/base/abci/abc.c | 12 +++---- src/base/main/main.h | 5 +++ src/base/main/mainFrame.c | 6 ++-- src/base/main/mainInt.h | 2 +- src/map/if/ifCom.c | 75 +++++++++++++++++++++++++-------------- src/map/mpm/mpmMan.c | 5 +-- 6 files changed, 67 insertions(+), 38 deletions(-) diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c index 688ea3e96..490167206 100644 --- a/src/base/abci/abc.c +++ b/src/base/abci/abc.c @@ -42941,12 +42941,12 @@ int Abc_CommandAbc9If( Abc_Frame_t * pAbc, int argc, char ** argv ) int c; // set defaults Gia_ManSetIfParsDefault( pPars ); - if ( pAbc->pLibLut == NULL ) + if ( Abc_FrameReadLibLut() == NULL ) { Abc_Print( -1, "LUT library is not given. Using default LUT library.\n" ); - pAbc->pLibLut = If_LibLutSetSimple( 6 ); + Abc_FrameSetLibLut( If_LibLutSetSimple( 6 ) ); } - pPars->pLutLib = (If_LibLut_t *)pAbc->pLibLut; + pPars->pLutLib = (If_LibLut_t *)Abc_FrameReadLibLut(); Extra_UtilGetoptReset(); while ( ( c = Extra_UtilGetopt( argc, argv, "KCFAGRDEWSJTXYZqalepmrsdbgxyofuijkztncvwh" ) ) != EOF ) { @@ -43621,12 +43621,12 @@ int Abc_CommandAbc9Iff( Abc_Frame_t * pAbc, int argc, char ** argv ) Abc_Print( -1, "Abc_CommandAbc9Iff(): Mapping of the AIG is not defined.\n" ); return 1; } - if ( pAbc->pLibLut == NULL ) + if ( Abc_FrameReadLibLut() == NULL ) { Abc_Print( -1, "Abc_CommandAbc9Iff(): LUT library is not defined.\n" ); return 1; } - Gia_ManIffTest( pAbc->pGia, (If_LibLut_t *)pAbc->pLibLut, fVerbose ); + Gia_ManIffTest( pAbc->pGia, (If_LibLut_t *)Abc_FrameReadLibLut(), fVerbose ); return 0; usage: @@ -47296,7 +47296,7 @@ int Abc_CommandAbc9Trace( Abc_Frame_t * pAbc, int argc, char ** argv ) Abc_Print( -1, "Abc_CommandAbc9Speedup(): Mapping of the AIG is not defined.\n" ); return 1; } - pAbc->pGia->pLutLib = fUseLutLib ? pAbc->pLibLut : NULL; + pAbc->pGia->pLutLib = fUseLutLib ? Abc_FrameReadLibLut() : NULL; Gia_ManDelayTraceLutPrint( pAbc->pGia, fVerbose ); return 0; diff --git a/src/base/main/main.h b/src/base/main/main.h index f3457e27f..768cebd07 100644 --- a/src/base/main/main.h +++ b/src/base/main/main.h @@ -62,6 +62,9 @@ ABC_NAMESPACE_HEADER_START /// MACRO DEFINITIONS /// //////////////////////////////////////////////////////////////////////// +// the maximum number of LUT libraries +#define ABC_LUT_LIBS 4 + //////////////////////////////////////////////////////////////////////// /// FUNCTION DEFINITIONS /// //////////////////////////////////////////////////////////////////////// @@ -96,6 +99,7 @@ extern ABC_DLL Abc_Frame_t * Abc_FrameReadGlobalFrame(); extern ABC_DLL Vec_Ptr_t * Abc_FrameReadStore(); extern ABC_DLL int Abc_FrameReadStoreSize(); extern ABC_DLL void * Abc_FrameReadLibLut(); +extern ABC_DLL void * Abc_FrameReadLibLutI( int i ); extern ABC_DLL void * Abc_FrameReadLibBox(); extern ABC_DLL void * Abc_FrameReadLibGen(); extern ABC_DLL void * Abc_FrameReadLibGen2(); @@ -134,6 +138,7 @@ extern ABC_DLL int Abc_FrameReadCexFrame( Abc_Frame_t * p ); extern ABC_DLL void Abc_FrameSetNtkStore( Abc_Ntk_t * pNtk ); extern ABC_DLL void Abc_FrameSetNtkStoreSize( int nStored ); extern ABC_DLL void Abc_FrameSetLibLut( void * pLib ); +extern ABC_DLL void Abc_FrameSetLibLutI( void * pLib, int i ); extern ABC_DLL void Abc_FrameSetLibBox( void * pLib ); extern ABC_DLL void Abc_FrameSetLibGen( void * pLib ); extern ABC_DLL void Abc_FrameSetLibGen2( void * pLib ); diff --git a/src/base/main/mainFrame.c b/src/base/main/mainFrame.c index 77faabb0d..4027f8ad7 100644 --- a/src/base/main/mainFrame.c +++ b/src/base/main/mainFrame.c @@ -54,7 +54,8 @@ static Abc_Frame_t * s_GlobalFrame = NULL; ***********************************************************************/ Vec_Ptr_t * Abc_FrameReadStore() { return s_GlobalFrame->vStore; } int Abc_FrameReadStoreSize() { return Vec_PtrSize(s_GlobalFrame->vStore); } -void * Abc_FrameReadLibLut() { return s_GlobalFrame->pLibLut; } +void * Abc_FrameReadLibLut() { return s_GlobalFrame->pLibLut[0]; } +void * Abc_FrameReadLibLutI( int i ) { return s_GlobalFrame->pLibLut[i]; } void * Abc_FrameReadLibBox() { return s_GlobalFrame->pLibBox; } void * Abc_FrameReadLibGen() { return s_GlobalFrame->pLibGen; } void * Abc_FrameReadLibGen2() { return s_GlobalFrame->pLibGen2; } @@ -90,7 +91,8 @@ void Abc_FrameInputNdr( Abc_Frame_t * pAbc, void * pData ) { Ndr_Delete(s void * Abc_FrameOutputNdr( Abc_Frame_t * pAbc ) { void * pData = s_GlobalFrame->pNdr; s_GlobalFrame->pNdr = NULL; return pData; } int * Abc_FrameOutputNdrArray( Abc_Frame_t * pAbc ) { int * pArray = s_GlobalFrame->pNdrArray; s_GlobalFrame->pNdrArray = NULL; return pArray; } -void Abc_FrameSetLibLut( void * pLib ) { s_GlobalFrame->pLibLut = pLib; } +void Abc_FrameSetLibLut( void * pLib ) { s_GlobalFrame->pLibLut[0]= pLib; } +void Abc_FrameSetLibLutI( void * pLib, int i ) { s_GlobalFrame->pLibLut[i]= pLib; } void Abc_FrameSetLibBox( void * pLib ) { s_GlobalFrame->pLibBox = pLib; } void Abc_FrameSetLibGen( void * pLib ) { s_GlobalFrame->pLibGen = pLib; } void Abc_FrameSetLibGen2( void * pLib ) { s_GlobalFrame->pLibGen2 = pLib; } diff --git a/src/base/main/mainInt.h b/src/base/main/mainInt.h index dd86642cb..118b6916e 100644 --- a/src/base/main/mainInt.h +++ b/src/base/main/mainInt.h @@ -98,7 +98,7 @@ struct Abc_Frame_t_ void * pManDsd; // decomposition manager void * pManDsd2; // decomposition manager // libraries for mapping - void * pLibLut; // the current LUT library + void * pLibLut[ABC_LUT_LIBS]; // the current LUT library void * pLibBox; // the current box library void * pLibGen; // the current genlib void * pLibGen2; // the current genlib diff --git a/src/map/if/ifCom.c b/src/map/if/ifCom.c index a2f54ae35..97fefea1d 100644 --- a/src/map/if/ifCom.c +++ b/src/map/if/ifCom.c @@ -78,7 +78,10 @@ void If_Init( Abc_Frame_t * pAbc ) ***********************************************************************/ void If_End( Abc_Frame_t * pAbc ) { - If_LibLutFree( (If_LibLut_t *) Abc_FrameReadLibLut() ); + int i; + for ( i = 0; i < ABC_LUT_LIBS; i++ ) + if ( Abc_FrameReadLibLutI(i) ) + If_LibLutFree( (If_LibLut_t *)Abc_FrameReadLibLutI(i) ); If_LibBoxFree( (If_LibBox_t *)Abc_FrameReadLibBox() ); } @@ -125,36 +128,51 @@ int If_CommandReadLut( Abc_Frame_t * pAbc, int argc, char **argv ) } } - if ( argc != globalUtilOptind + 1 ) - goto usage; - - // get the input file name - FileName = argv[globalUtilOptind]; - if ( (pFile = fopen( FileName, "r" )) == NULL ) - { - fprintf( pErr, "Cannot open input file \"%s\". ", FileName ); - if ( (FileName = Extra_FileGetSimilarName( FileName, ".genlib", ".lib", ".gen", ".g", NULL )) ) - fprintf( pErr, "Did you mean \"%s\"?", FileName ); - fprintf( pErr, "\n" ); - return 1; - } - fclose( pFile ); - - // set the new network - pLib = If_LibLutRead( FileName ); - if ( pLib == NULL ) - { - fprintf( pErr, "Reading LUT library has failed.\n" ); + if ( argc == globalUtilOptind ) { + fprintf( pErr, "The library file should be specified in the command line.\n" ); goto usage; } - // replace the current library - If_LibLutFree( (If_LibLut_t *)Abc_FrameReadLibLut() ); - Abc_FrameSetLibLut( pLib ); + if ( argc > globalUtilOptind + ABC_LUT_LIBS ) { + fprintf( pErr, "Can read at most %d libraries. Quitting...\n", ABC_LUT_LIBS ); + goto usage; + } + + // remove current libraries + int i; + for ( i = 0; i < ABC_LUT_LIBS; i++ ) + if ( Abc_FrameReadLibLutI(i) ) { + If_LibLutFree( (If_LibLut_t *)Abc_FrameReadLibLutI(i) ); + Abc_FrameSetLibLutI( NULL, i ); + } + + // input new libraries + for ( i = globalUtilOptind; i < argc; i++ ) { + // get the input file name + FileName = argv[i]; + if ( (pFile = fopen( FileName, "r" )) == NULL ) + { + fprintf( pErr, "Cannot open input file \"%s\". ", FileName ); + if ( (FileName = Extra_FileGetSimilarName( FileName, ".genlib", ".lib", ".gen", ".g", NULL )) ) + fprintf( pErr, "Did you mean \"%s\"?", FileName ); + fprintf( pErr, "\n" ); + return 1; + } + fclose( pFile ); + // set the new network + pLib = If_LibLutRead( FileName ); + if ( pLib == NULL ) + { + fprintf( pErr, "Reading LUT library has failed.\n" ); + goto usage; + } + // replace the current library + Abc_FrameSetLibLutI( pLib, i-globalUtilOptind ); + } return 0; usage: - fprintf( pErr, "\nusage: read_lut [-vh]\n"); - fprintf( pErr, "\t read the LUT library from the file\n" ); + fprintf( pErr, "\nusage: read_lut [-vh] ... \n"); + fprintf( pErr, "\t read the LUT library from the file(s)\n" ); fprintf( pErr, "\t-v : toggles enabling of verbose output [default = %s]\n", (fVerbose? "yes" : "no") ); fprintf( pErr, "\t-h : print the command usage\n"); fprintf( pErr, "\t \n"); @@ -216,7 +234,10 @@ int If_CommandPrintLut( Abc_Frame_t * pAbc, int argc, char **argv ) goto usage; // set the new network - If_LibLutPrint( (If_LibLut_t *)Abc_FrameReadLibLut() ); + int i; + for ( i = 0; i < ABC_LUT_LIBS; i++ ) + if ( Abc_FrameReadLibLutI(i) ) + If_LibLutPrint( (If_LibLut_t *)Abc_FrameReadLibLutI(i) ); return 0; usage: diff --git a/src/map/mpm/mpmMan.c b/src/map/mpm/mpmMan.c index 4648148de..cdcee1388 100644 --- a/src/map/mpm/mpmMan.c +++ b/src/map/mpm/mpmMan.c @@ -19,6 +19,7 @@ ***********************************************************************/ #include "mpmInt.h" +#include "base/main/main.h" ABC_NAMESPACE_IMPL_START @@ -55,8 +56,8 @@ Mpm_Man_t * Mpm_ManStart( Mig_Man_t * pMig, Mpm_Par_t * pPars ) p = ABC_CALLOC( Mpm_Man_t, 1 ); p->pMig = pMig; p->pPars = pPars; - p->pLibLut = pPars->pLib; - p->nLutSize = pPars->pLib->LutMax; + p->pLibLut = (Mpm_LibLut_t *)Abc_FrameReadLibLut(); + p->nLutSize = p->pLibLut->LutMax; p->nTruWords = pPars->fUseTruth ? Abc_Truth6WordNum(p->nLutSize) : 0; p->nNumCuts = pPars->nNumCuts; // cuts From 18f6464ec765c2ca14ede4f7a17f09011b0a0600 Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Fri, 24 Oct 2025 16:57:55 -0700 Subject: [PATCH 06/17] Experiments with LUT mapping. --- src/aig/gia/giaIf.c | 109 +++++++++++++++++++++++++++++++++++++++++++- src/base/abci/abc.c | 8 ++-- src/map/if/if.h | 1 + src/map/if/ifDecJ.c | 23 +++------- 4 files changed, 119 insertions(+), 22 deletions(-) diff --git a/src/aig/gia/giaIf.c b/src/aig/gia/giaIf.c index d44a47102..0ce43a351 100644 --- a/src/aig/gia/giaIf.c +++ b/src/aig/gia/giaIf.c @@ -1175,6 +1175,111 @@ int Gia_ManFromIfLogicCreateLutSpecial( Gia_Man_t * pNew, word * pRes, Vec_Int_t return iObjLit2; } +/**Function************************************************************* + + Synopsis [Write mapping for LUT with given fanins.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Gia_ManFromIfLogicCreateLutSpecialJ( Gia_Man_t * pNew, word * pRes, Vec_Int_t * vLeaves, Vec_Int_t * vLeavesTemp, Vec_Int_t * vCover, Vec_Int_t * vMapping, Vec_Int_t * vMapping2, Vec_Int_t * vPacking ) +{ + word z = If_CutPerformDeriveJ( NULL, (unsigned *)pRes, Vec_IntSize(vLeaves), Vec_IntSize(vLeaves), NULL, 1 ); + word Truth; + int i, iObjLit1, iObjLit2, iObjLit3; + + if ( ((z >> 63) & 1) == 0 ) // S44 decomposition + { + // create first LUT + Vec_IntClear( vLeavesTemp ); + for ( i = 0; i < 4; i++ ) + { + int v = (int)((z >> (16+(i<<2))) & 7); + if ( v == 6 && Vec_IntSize(vLeaves) == 5 ) + continue; + Vec_IntPush( vLeavesTemp, Vec_IntEntry(vLeaves, v) ); + } + Truth = (z & 0xffff); + Truth |= (Truth << 16); + Truth |= (Truth << 32); + iObjLit1 = Gia_ManFromIfLogicCreateLut( pNew, &Truth, vLeavesTemp, vCover, vMapping, vMapping2 ); + // create second LUT + Vec_IntClear( vLeavesTemp ); + for ( i = 0; i < 4; i++ ) + { + int v = (int)((z >> (48+(i<<2))) & 7); + if ( v == 6 && Vec_IntSize(vLeaves) == 5 ) + continue; + if ( v == 7 ) + Vec_IntPush( vLeavesTemp, iObjLit1 ); + else + Vec_IntPush( vLeavesTemp, Vec_IntEntry(vLeaves, v) ); + } + Truth = ((z >> 32) & 0xffff); + Truth |= (Truth << 16); + Truth |= (Truth << 32); + iObjLit2 = Gia_ManFromIfLogicCreateLut( pNew, &Truth, vLeavesTemp, vCover, vMapping, vMapping2 ); + // write packing + Vec_IntPush( vPacking, 2 ); + Vec_IntPush( vPacking, Abc_Lit2Var(iObjLit1) ); + Vec_IntPush( vPacking, Abc_Lit2Var(iObjLit2) ); + Vec_IntAddToEntry( vPacking, 0, 1 ); + return iObjLit2; + } + else + { + int Pla2Var[9]; + extern void If_PermUnpack( unsigned Value, int Pla2Var[9] ); + If_PermUnpack( (unsigned)(z >> 32), Pla2Var ); + + // create first data LUT + Vec_IntClear( vLeavesTemp ); + for ( i = 0; i < 4; i++ ) + { + if ( Pla2Var[i] != 9 ) + Vec_IntPush( vLeavesTemp, Vec_IntEntry(vLeaves, Pla2Var[i]) ); + } + Truth = (z & 0xffff); + Truth |= (Truth << 16); + Truth |= (Truth << 32); + iObjLit1 = Gia_ManFromIfLogicCreateLut( pNew, &Truth, vLeavesTemp, vCover, vMapping, vMapping2 ); + + // create second data LUT + Vec_IntClear( vLeavesTemp ); + for ( i = 4; i < 8; i++ ) + { + if ( Pla2Var[i] != 9 ) + Vec_IntPush( vLeavesTemp, Vec_IntEntry(vLeaves, Pla2Var[i]) ); + } + Truth = ((z >> 16) & 0xffff); + Truth |= (Truth << 16); + Truth |= (Truth << 32); + iObjLit2 = Gia_ManFromIfLogicCreateLut( pNew, &Truth, vLeavesTemp, vCover, vMapping, vMapping2 ); + + // create MUX LUT (2-input MUX: select ? iObjLit2 : iObjLit1) + Vec_IntClear( vLeavesTemp ); + Vec_IntPush( vLeavesTemp, iObjLit1 ); // data 0 + Vec_IntPush( vLeavesTemp, iObjLit2 ); // data 1 + if ( Pla2Var[8] != 9 ) + Vec_IntPush( vLeavesTemp, Vec_IntEntry(vLeaves, Pla2Var[8]) ); // select + // MUX truth table: f = s ? d1 : d0 = ~s&d0 | s&d1 = 0xCACACACA for (d0,d1,s) + Truth = ABC_CONST(0xCACACACACACACACA); + iObjLit3 = Gia_ManFromIfLogicCreateLut( pNew, &Truth, vLeavesTemp, vCover, vMapping, vMapping2 ); + + // write packing - 3 LUTs packed together + Vec_IntPush( vPacking, 3 ); + Vec_IntPush( vPacking, Abc_Lit2Var(iObjLit1) ); + Vec_IntPush( vPacking, Abc_Lit2Var(iObjLit2) ); + Vec_IntPush( vPacking, Abc_Lit2Var(iObjLit3) ); + Vec_IntAddToEntry( vPacking, 0, 1 ); + return iObjLit3; + } +} + /**Function************************************************************* Synopsis [Write the node into a file.] @@ -1197,7 +1302,7 @@ int Gia_ManFromIfLogicNode( void * pIfMan, Gia_Man_t * pNew, int iObj, Vec_Int_t // perform special case matching for 44 if ( fCheck44e ) { - if ( Vec_IntSize(vLeaves) <= 4 ) + if ( Vec_IntSize(vLeaves) <= 5 ) { // create mapping iObjLit1 = Gia_ManFromIfLogicCreateLut( pNew, pRes, vLeaves, vCover, vMapping, vMapping2 ); @@ -1210,7 +1315,7 @@ int Gia_ManFromIfLogicNode( void * pIfMan, Gia_Man_t * pNew, int iObj, Vec_Int_t } return iObjLit1; } - return Gia_ManFromIfLogicCreateLutSpecial( pNew, pRes, vLeaves, vLeavesTemp, vCover, vMapping, vMapping2, vPacking ); + return Gia_ManFromIfLogicCreateLutSpecialJ( pNew, pRes, vLeaves, vLeavesTemp, vCover, vMapping, vMapping2, vPacking ); } if ( ((If_Man_t *)pIfMan)->pPars->fLut6Filter && Vec_IntSize(vLeaves) == 6 ) { diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c index 490167206..3face1f5b 100644 --- a/src/base/abci/abc.c +++ b/src/base/abci/abc.c @@ -21840,9 +21840,9 @@ int Abc_CommandIf( Abc_Frame_t * pAbc, int argc, char ** argv ) } if ( pPars->fEnableCheck07 ) { - if ( pPars->nLutSize < 6 || pPars->nLutSize > 7 ) + if ( pPars->nLutSize > 9 ) { - Abc_Print( -1, "This feature only works for {6,7}-LUTs.\n" ); + Abc_Print( -1, "This feature only works for up to 9-input LUTs.\n" ); return 1; } pPars->pFuncCell = If_CutPerformCheckJ; @@ -43283,9 +43283,9 @@ int Abc_CommandAbc9If( Abc_Frame_t * pAbc, int argc, char ** argv ) } if ( pPars->fEnableCheck07 ) { - if ( pPars->nLutSize < 6 || pPars->nLutSize > 7 ) + if ( pPars->nLutSize > 9 ) { - Abc_Print( -1, "This feature only works for {6,7}-LUTs.\n" ); + Abc_Print( -1, "This feature only works for up to 9-input LUTs.\n" ); return 1; } pPars->pFuncCell = If_CutPerformCheckJ; diff --git a/src/map/if/if.h b/src/map/if/if.h index 9056d1f1f..f5ea0b966 100644 --- a/src/map/if/if.h +++ b/src/map/if/if.h @@ -552,6 +552,7 @@ extern float If_CutPowerDerefed( If_Man_t * p, If_Cut_t * pCut, If_Obj extern float If_CutPowerRefed( If_Man_t * p, If_Cut_t * pCut, If_Obj_t * pRoot ); /*=== ifDec.c =============================================================*/ extern word If_CutPerformDerive07( If_Man_t * p, unsigned * pTruth, int nVars, int nLeaves, char * pStr ); +extern word If_CutPerformDeriveJ( If_Man_t * p, unsigned * pTruth, int nVars, int nLeaves, char * pStr, int fDerive ); extern int If_CutPerformCheck07( If_Man_t * p, unsigned * pTruth, int nVars, int nLeaves, char * pStr ); extern int If_CutPerformCheck08( If_Man_t * p, unsigned * pTruth, int nVars, int nLeaves, char * pStr ); extern int If_CutPerformCheck10( If_Man_t * p, unsigned * pTruth, int nVars, int nLeaves, char * pStr ); diff --git a/src/map/if/ifDecJ.c b/src/map/if/ifDecJ.c index d77640ee0..4b33703ff 100644 --- a/src/map/if/ifDecJ.c +++ b/src/map/if/ifDecJ.c @@ -30,26 +30,17 @@ ABC_NAMESPACE_IMPL_START /// FUNCTION DEFINITIONS /// //////////////////////////////////////////////////////////////////////// -/**Function************************************************************* - - Synopsis [Performs additional check.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ int If_CutPerformCheckJ( If_Man_t * p, unsigned * pTruth, int nVars, int nLeaves, char * pStr ) { - int v; - // skip non-support minimal - for ( v = 0; v < nLeaves; v++ ) - if ( !Abc_TtHasVar( (word *)pTruth, nVars, v ) ) - return 0; return 1; } +word If_CutPerformDeriveJ( If_Man_t * p, unsigned * pTruth, int nVars, int nLeaves, char * pStr, int fDerive ) +{ + return 0; +} +void If_PermUnpack( unsigned Value, int Pla2Var[9] ) +{ +} //////////////////////////////////////////////////////////////////////// /// END OF FILE /// From 56a7c049aef3dd923e246a9cb631b5fe6c5195f5 Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Thu, 30 Oct 2025 16:35:15 -0700 Subject: [PATCH 07/17] Extending max support size in "lutexact". --- src/base/abci/abc.c | 2 +- src/sat/bmc/bmcMaj.c | 45 +++++++++++++++++++++++++++---------------- src/sat/bmc/bmcMaj2.c | 18 +++++++++++------ src/sat/bmc/bmcMaj3.c | 4 ++-- 4 files changed, 43 insertions(+), 26 deletions(-) diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c index 3face1f5b..56993e208 100644 --- a/src/base/abci/abc.c +++ b/src/base/abci/abc.c @@ -10837,7 +10837,7 @@ int Abc_CommandLutExact( Abc_Frame_t * pAbc, int argc, char ** argv ) Abc_Print( -1, "Function with %d variales cannot be implemented with %d %d-input LUTs.\n", pPars->nVars, pPars->nNodes, pPars->nLutSize ); return 1; } - if ( pPars->nVars > 10 ) + if ( pPars->nVars > 12 ) { Abc_Print( -1, "Function should not have more than 10 inputs.\n" ); return 1; diff --git a/src/sat/bmc/bmcMaj.c b/src/sat/bmc/bmcMaj.c index b54418a41..780271c47 100644 --- a/src/sat/bmc/bmcMaj.c +++ b/src/sat/bmc/bmcMaj.c @@ -605,19 +605,23 @@ static inline int Exa_ManEval( Exa_Man_t * p ) ***********************************************************************/ void Exa_ManDumpBlif( Exa_Man_t * p, int fCompl ) { - char Buffer[1000]; + char * pStr = ABC_ALLOC( char, (1 << (p->nVars-2)) + 10 ); char FileName[1100]; FILE * pFile; int i, k, iVar; if ( fCompl ) Abc_TtNot( p->pTruth, p->nWords ); - Extra_PrintHexadecimalString( Buffer, (unsigned *)p->pTruth, p->nVars ); + Extra_PrintHexadecimalString( pStr, (unsigned *)p->pTruth, p->nVars ); + if ( strlen(pStr) > 16 ) { + pStr[16] = '_'; + pStr[17] = '\0'; + } if ( fCompl ) Abc_TtNot( p->pTruth, p->nWords ); - sprintf( FileName, "%s_%d_%d.blif", Buffer, 2, p->nNodes ); + sprintf( FileName, "%s_%d_%d.blif", pStr, 2, p->nNodes ); pFile = fopen( FileName, "wb" ); - fprintf( pFile, "# Realization of the %d-input function %s using %d two-input gates:\n", p->nVars, Buffer, p->nNodes ); - fprintf( pFile, ".model %s_%d_%d\n", Buffer, 2, p->nNodes ); + fprintf( pFile, "# Realization of the %d-input function %s using %d two-input gates:\n", p->nVars, pStr, p->nNodes ); + fprintf( pFile, ".model %s_%d_%d\n", pStr, 2, p->nNodes ); fprintf( pFile, ".inputs" ); for ( i = 0; i < p->nVars; i++ ) fprintf( pFile, " %c", 'a'+i ); @@ -655,6 +659,7 @@ void Exa_ManDumpBlif( Exa_Man_t * p, int fCompl ) fprintf( pFile, ".end\n\n" ); fclose( pFile ); printf( "Solution was dumped into file \"%s\".\n", FileName ); + ABC_FREE( pStr ); } void Exa_ManPrintSolution( Exa_Man_t * p, int fCompl ) { @@ -942,8 +947,8 @@ void Exa_ManExactSynthesis( Bmc_EsPar_t * pPars ) int i, status, iMint = 1; abctime clkTotal = Abc_Clock(); Exa_Man_t * p; int fCompl = 0; - word pTruth[16]; Abc_TtReadHex( pTruth, pPars->pTtStr ); - assert( pPars->nVars <= 10 ); + word pTruth[64]; Abc_TtReadHex( pTruth, pPars->pTtStr ); + assert( pPars->nVars <= 12 ); p = Exa_ManAlloc( pPars, pTruth ); if ( pTruth[0] & 1 ) { fCompl = 1; Abc_TtNot( pTruth, p->nWords ); } status = Exa_ManAddCnfStart( p, pPars->fOnlyAnd ); @@ -1327,11 +1332,16 @@ static void Exa3_ManDumpBlif( Exa3_Man_t * p, int fCompl ) { int i, k, b, iVar; char pFileName[1000]; - sprintf( pFileName, "%s.blif", p->pPars->pTtStr ); + char * pStr = Abc_UtilStrsav(p->pPars->pTtStr); + if ( strlen(pStr) > 16 ) { + pStr[16] = '_'; + pStr[17] = '\0'; + } + sprintf( pFileName, "%s.blif", pStr ); FILE * pFile = fopen( pFileName, "wb" ); if ( pFile == NULL ) return; fprintf( pFile, "# Realization of given %d-input function using %d %d-input LUTs synthesized by ABC on %s\n", p->nVars, p->nNodes, p->nLutSize, Extra_TimeStamp() ); - fprintf( pFile, ".model %s\n", p->pPars->pTtStr ); + fprintf( pFile, ".model %s\n", pStr ); fprintf( pFile, ".inputs" ); for ( k = 0; k < p->nVars; k++ ) fprintf( pFile, " %c", 'a'+k ); @@ -1365,6 +1375,7 @@ static void Exa3_ManDumpBlif( Exa3_Man_t * p, int fCompl ) fprintf( pFile, ".end\n\n" ); fclose( pFile ); printf( "Finished dumping the resulting LUT network into file \"%s\".\n", pFileName ); + ABC_FREE( pStr ); } @@ -1600,7 +1611,7 @@ int Exa3_ManExactSynthesis( Bmc_EsPar_t * pPars ) int i, status, Res = 0, iMint = 1; abctime clkTotal = Abc_Clock(); Exa3_Man_t * p; int fCompl = 0; - word pTruth[16]; + word pTruth[64]; if ( pPars->pSymStr ) { word * pFun = Abc_TtSymFunGenerate( pPars->pSymStr, pPars->nVars ); pPars->pTtStr = ABC_CALLOC( char, pPars->nVars > 2 ? (1 << (pPars->nVars-2)) + 1 : 2 ); @@ -1611,7 +1622,7 @@ int Exa3_ManExactSynthesis( Bmc_EsPar_t * pPars ) if ( pPars->pTtStr ) Abc_TtReadHex( pTruth, pPars->pTtStr ); else assert( 0 ); - assert( pPars->nVars <= 10 ); + assert( pPars->nVars <= 12 ); assert( pPars->nLutSize <= 6 ); p = Exa3_ManAlloc( pPars, pTruth ); if ( pTruth[0] & 1 ) { fCompl = 1; Abc_TtNot( pTruth, p->nWords ); } @@ -2491,9 +2502,9 @@ void Exa_ManExactSynthesis4( Bmc_EsPar_t * pPars ) int i, m, nMints = 1 << pPars->nVars, fCompl = 0; Vec_Wrd_t * vSimsIn = Vec_WrdStart( nMints ); Vec_Wrd_t * vSimsOut = Vec_WrdStart( nMints ); - word pTruth[16]; Abc_TtReadHex( pTruth, pPars->pTtStr ); + word pTruth[64]; Abc_TtReadHex( pTruth, pPars->pTtStr ); if ( pTruth[0] & 1 ) { fCompl = 1; Abc_TtNot( pTruth, Abc_TtWordNum(pPars->nVars) ); } - assert( pPars->nVars <= 10 ); + assert( pPars->nVars <= 12 ); for ( m = 0; m < nMints; m++ ) { Abc_TtSetBit( Vec_WrdEntryP(vSimsOut, m), Abc_TtGetBit(pTruth, m) ); @@ -2995,9 +3006,9 @@ void Exa_ManExactSynthesis5( Bmc_EsPar_t * pPars ) int i, m, nMints = 1 << pPars->nVars, fCompl = 0; Vec_Wrd_t * vSimsIn = Vec_WrdStart( nMints ); Vec_Wrd_t * vSimsOut = Vec_WrdStart( nMints ); - word pTruth[16]; Abc_TtReadHex( pTruth, pPars->pTtStr ); + word pTruth[64]; Abc_TtReadHex( pTruth, pPars->pTtStr ); if ( pTruth[0] & 1 ) { fCompl = 1; Abc_TtNot( pTruth, Abc_TtWordNum(pPars->nVars) ); } - assert( pPars->nVars <= 10 ); + assert( pPars->nVars <= 12 ); for ( m = 0; m < nMints; m++ ) { Abc_TtSetBit( Vec_WrdEntryP(vSimsOut, m), Abc_TtGetBit(pTruth, m) ); @@ -3102,7 +3113,7 @@ word Exa_ManExactSynthesis4VarsOne( int Index, int Truth, int nNodes ) int i, m, nMints = 16, fCompl = 0; Vec_Wrd_t * vSimsIn = Vec_WrdStart( nMints ); Vec_Wrd_t * vSimsOut = Vec_WrdStart( nMints ); - word pTruth[16] = { Abc_Tt6Stretch((word)Truth, 4) }; + word pTruth[64] = { Abc_Tt6Stretch((word)Truth, 4) }; if ( pTruth[0] & 1 ) { fCompl = 1; Abc_TtNot( pTruth, 1 ); } for ( m = 0; m < nMints; m++ ) { @@ -4189,7 +4200,7 @@ void Exa_ManExactSynthesis7( Bmc_EsPar_t * pPars, int GateSize ) abctime clkTotal = Abc_Clock(); int v, n, nMints = 1 << pPars->nVars; int nV = pPars->nVars + pPars->nNodes; - word pTruth[16]; Abc_TtReadHex( pTruth, pPars->pTtStr ); + word pTruth[64]; Abc_TtReadHex( pTruth, pPars->pTtStr ); Vec_Int_t * vValues = NULL; int Rand = ((((unsigned)rand()) << 12) ^ ((unsigned)rand())) & 0xFFFFF; char pFileNameIn[32]; sprintf( pFileNameIn, "_%05x_.cnf", Rand ); diff --git a/src/sat/bmc/bmcMaj2.c b/src/sat/bmc/bmcMaj2.c index 665b61611..c9403e037 100644 --- a/src/sat/bmc/bmcMaj2.c +++ b/src/sat/bmc/bmcMaj2.c @@ -854,8 +854,8 @@ void Exa_ManExactSynthesis2( Bmc_EsPar_t * pPars ) int i, status, iMint = 1; abctime clkTotal = Abc_Clock(); Exa_Man_t * p; int fCompl = 0; - word pTruth[16]; Abc_TtReadHex( pTruth, pPars->pTtStr ); - assert( pPars->nVars <= 10 ); + word pTruth[64]; Abc_TtReadHex( pTruth, pPars->pTtStr ); + assert( pPars->nVars <= 12 ); p = Exa_ManAlloc( pPars, pTruth ); if ( pTruth[0] & 1 ) { fCompl = 1; Abc_TtNot( pTruth, p->nWords ); } status = Exa_ManAddCnfStart( p, pPars->fOnlyAnd ); @@ -1191,11 +1191,16 @@ static void Exa3_ManDumpBlif( Exa3_Man_t * p, int fCompl ) { int i, k, b, iVar; char pFileName[1000]; - sprintf( pFileName, "%s.blif", p->pPars->pTtStr ); + char * pStr = Abc_UtilStrsav(p->pPars->pTtStr); + if ( strlen(pStr) > 16 ) { + pStr[16] = '_'; + pStr[17] = '\0'; + } + sprintf( pFileName, "%s.blif", pStr ); FILE * pFile = fopen( pFileName, "wb" ); if ( pFile == NULL ) return; fprintf( pFile, "# Realization of given %d-input function using %d %d-input LUTs synthesized by ABC on %s\n", p->nVars, p->nNodes, p->nLutSize, Extra_TimeStamp() ); - fprintf( pFile, ".model %s\n", p->pPars->pTtStr ); + fprintf( pFile, ".model %s\n", pStr ); fprintf( pFile, ".inputs" ); for ( k = 0; k < p->nVars; k++ ) fprintf( pFile, " %c", 'a'+k ); @@ -1229,6 +1234,7 @@ static void Exa3_ManDumpBlif( Exa3_Man_t * p, int fCompl ) fprintf( pFile, ".end\n\n" ); fclose( pFile ); printf( "Finished dumping the resulting LUT network into file \"%s\".\n", pFileName ); + ABC_FREE( pStr ); } @@ -1387,7 +1393,7 @@ void Exa3_ManExactSynthesis2( Bmc_EsPar_t * pPars ) int i, status, iMint = 1; abctime clkTotal = Abc_Clock(); Exa3_Man_t * p; int fCompl = 0; - word pTruth[16]; + word pTruth[64]; if ( pPars->pSymStr ) { word * pFun = Abc_TtSymFunGenerate( pPars->pSymStr, pPars->nVars ); pPars->pTtStr = ABC_CALLOC( char, pPars->nVars > 2 ? (1 << (pPars->nVars-2)) + 1 : 2 ); @@ -1398,7 +1404,7 @@ void Exa3_ManExactSynthesis2( Bmc_EsPar_t * pPars ) if ( pPars->pTtStr ) Abc_TtReadHex( pTruth, pPars->pTtStr ); else assert( 0 ); - assert( pPars->nVars <= 10 ); + assert( pPars->nVars <= 12 ); assert( pPars->nLutSize <= 6 ); p = Exa3_ManAlloc( pPars, pTruth ); if ( pTruth[0] & 1 ) { fCompl = 1; Abc_TtNot( pTruth, p->nWords ); } diff --git a/src/sat/bmc/bmcMaj3.c b/src/sat/bmc/bmcMaj3.c index 2a3bca07b..59f42bfa9 100644 --- a/src/sat/bmc/bmcMaj3.c +++ b/src/sat/bmc/bmcMaj3.c @@ -1263,13 +1263,13 @@ void Zyx_ManExactSynthesis( Bmc_EsPar_t * pPars ) { int status, Iter, iMint = 0, fCompl = 0, nLazyAll = 0, nSols = 0; abctime clkTotal = Abc_Clock(), clk = Abc_Clock(); Zyx_Man_t * p; - word pTruth[16]; + word pTruth[64]; if ( !pPars->fMajority ) { Abc_TtReadHex( pTruth, pPars->pTtStr ); if ( pTruth[0] & 1 ) { fCompl = 1; Abc_TtNot( pTruth, Abc_TtWordNum(pPars->nVars) ); } } - assert( pPars->nVars <= 10 ); + assert( pPars->nVars <= 12 ); assert( pPars->nLutSize <= 6 ); p = Zyx_ManAlloc( pPars, pPars->fMajority ? NULL : pTruth ); printf( "Running exact synthesis for %d-input function with %d %d-input %s...\n", From 6034f6621bd924b39e23a3f0a7765c1c259c03e0 Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Thu, 30 Oct 2025 22:14:18 -0700 Subject: [PATCH 08/17] Changes to cut dumping. --- src/map/if/ifMan.c | 47 +++++++++++++++++++++++++++++++++------------- 1 file changed, 34 insertions(+), 13 deletions(-) diff --git a/src/map/if/ifMan.c b/src/map/if/ifMan.c index b5b81294a..1a79014da 100644 --- a/src/map/if/ifMan.c +++ b/src/map/if/ifMan.c @@ -229,19 +229,24 @@ void If_ManDumpCut( If_Cut_t * pCut, int nLutSize, Vec_Int_t * vCuts ) for ( i = 0; i < pCut->nLeaves; i++ ) Vec_IntPush( vCuts, pCut->pLeaves[i] ); for ( ; i < nLutSize; i++ ) - Vec_IntPush( vCuts, 0 ); + Vec_IntPush( vCuts, -1 ); } void If_ManDumpCutsAndCost( If_Man_t * p, If_Obj_t * pObj, Vec_Int_t * vCuts, Vec_Int_t * vCutCosts ) { If_Cut_t * pCut; int k, nCuts = 0; - while ( nCuts < p->pPars->nCutsMax ) { - If_ObjForEachCut( pObj, pCut, k ) { - If_ManDumpCut( pCut, p->pPars->nLutSize, vCuts ); - Vec_IntPush( vCutCosts, (int)pCut->Area ); - if ( ++nCuts == p->pPars->nCutsMax ) - break; - } + If_ObjForEachCut( pObj, pCut, k ) { + If_ManDumpCut( pCut, p->pPars->nLutSize, vCuts ); + Vec_IntPush( vCutCosts, 1 ); + if ( ++nCuts == p->pPars->nCutsMax ) + break; } + while ( nCuts < p->pPars->nCutsMax ) { + for ( k = 0; k < p->pPars->nLutSize; k++ ) + Vec_IntPush( vCuts, -1 ); + Vec_IntPush( vCutCosts, 1 ); + nCuts++; + } + assert( nCuts == p->pPars->nCutsMax ); } void If_ManDumpCutsAndCostAdd( int Obj, int nCutsMax, int nLutSize, Vec_Int_t * vCopy, Vec_Int_t * vCuts, Vec_Int_t * vCutCosts, Vec_Int_t * vCutsOut, Vec_Int_t * vCutCostsOut ) { @@ -255,7 +260,7 @@ void If_ManDumpCutsAndCostAdd( int Obj, int nCutsMax, int nLutSize, Vec_Int_t * for ( i = 0; i < nCutsMax; i++ ) Vec_IntPush( vCutCostsOut, Vec_IntEntry( vCutCosts, Obj * nCutsMax + i ) ); } -int If_ManDumpData( If_Man_t * p, FILE * pFile ) +int If_ManDumpData2( If_Man_t * p, FILE * pFile ) { Vec_Int_t * vCopy = Vec_IntStartFull( If_ManObjNum(p) ); Vec_Int_t * vCopy2 = Vec_IntAlloc( If_ManObjNum(p) ); @@ -313,6 +318,22 @@ int If_ManDumpData( If_Man_t * p, FILE * pFile ) Vec_IntFree( vCutCosts ); return nBytes; } +int If_ManDumpData( If_Man_t * p, FILE * pFile ) +{ + int nSpace = p->pPars->nCutsMax * p->pPars->nLutSize; + If_Obj_t * pObj; int i, nBytes; + Vec_Int_t * vCuts = Vec_IntAlloc( 1 << 20 ); + Vec_IntFill( vCuts, (1 + If_ManCiNum(p))*nSpace, -1 ); + Vec_IntAppend( vCuts, p->vCuts ); + If_ManForEachCo( p, pObj, i ) { + Vec_IntPush( vCuts, If_ObjFanin0(pObj)->Id ); + Vec_IntFillExtra( vCuts, Vec_IntSize(vCuts)+nSpace-1, -1 ); + } + nBytes = fwrite( Vec_IntArray(vCuts), 1, sizeof(int)*Vec_IntSize(vCuts), pFile ); + assert( nBytes == If_ManObjNum(p)*nSpace*sizeof(int) ); + Vec_IntFree( vCuts ); + return nBytes; +} /**Function************************************************************* @@ -332,16 +353,16 @@ void If_ManStop( If_Man_t * p ) char pFileName[1000] = {0}; // "I15_O20_L32_N256_C16_K6__name.bin" char * pName = Extra_FileNameGeneric(Extra_FileNameWithoutPath(p->pName)); - sprintf( pFileName, "%s__I%d_O%d_L%d_N%d_C%d_K%d.bin", pName, If_ManCiNum(p), If_ManCoNum(p), p->nLevelMax, If_ManAndNum(p), p->pPars->nCutsMax, p->pPars->nLutSize ); + sprintf( pFileName, "%s__n%d_c%d_k%d.bin", pName, If_ManObjNum(p), p->pPars->nCutsMax, p->pPars->nLutSize ); ABC_FREE( pName ); FILE * pFile = fopen( pFileName, "wb" ); if ( pFile == NULL ) printf( "Cannot open file \"%s\" for writing.\n", pFileName ); else { int nBytes = If_ManDumpData( p, pFile ); - int nBytes2 = sizeof(int) * (If_ManAndNum(p) * p->pPars->nCutsMax * p->pPars->nLutSize + If_ManCoNum(p) + p->nLevelMax + 1); - nBytes2 += sizeof(int) * (If_ManAndNum(p) * p->pPars->nCutsMax); - assert( nBytes == nBytes2 ); + //int nBytes2 = sizeof(int) * (If_ManAndNum(p) * p->pPars->nCutsMax * p->pPars->nLutSize + If_ManCoNum(p) + p->nLevelMax + 1); + //nBytes2 += sizeof(int) * (If_ManAndNum(p) * p->pPars->nCutsMax); + //assert( nBytes == nBytes2 ); fclose( pFile ); printf( "Finished writing cut information into file \"%s\" (%.3f MB).\n", pFileName, 1.0 * nBytes / (1<<20) ); } From a9d62d845d4cabb434e27f345a7e0959303e209a Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Sat, 1 Nov 2025 01:21:37 -0700 Subject: [PATCH 09/17] Experiments with LUT mapping. --- src/aig/gia/gia.h | 1 + src/aig/gia/giaAiger.c | 113 ++++++++++++++ src/aig/gia/giaDup.c | 2 + src/aig/gia/giaIf.c | 271 +++++++++++++++++++++++++++++++-- src/aig/gia/giaMan.c | 1 + src/base/abci/abc.c | 3 + src/map/if/ifTune.c | 336 +++++++++++++++++++++++++++++++++++++++++ 7 files changed, 716 insertions(+), 11 deletions(-) diff --git a/src/aig/gia/gia.h b/src/aig/gia/gia.h index 45f2329cb..098892f85 100644 --- a/src/aig/gia/gia.h +++ b/src/aig/gia/gia.h @@ -140,6 +140,7 @@ struct Gia_Man_t_ void * pSatlutWinman; // windowing for SAT-based mapping Vec_Int_t * vPacking; // packing information Vec_Int_t * vConfigs; // cell configurations + Vec_Str_t * vConfigs2; // cell configurations char * pCellStr; // cell description Vec_Int_t * vLutConfigs; // LUT configurations Vec_Int_t * vEdgeDelay; // special edge information diff --git a/src/aig/gia/giaAiger.c b/src/aig/gia/giaAiger.c index 107faaceb..a51ddfa43 100644 --- a/src/aig/gia/giaAiger.c +++ b/src/aig/gia/giaAiger.c @@ -22,6 +22,7 @@ #include "gia.h" #include "misc/tim/tim.h" #include "base/main/main.h" +#include "map/if/if.h" ABC_NAMESPACE_IMPL_START @@ -800,6 +801,36 @@ Gia_Man_t * Gia_AigerReadFromMemory( char * pContents, int nFileSize, int fGiaSi assert( pCur == pCurTemp ); if ( fVerbose ) printf( "Finished reading extension \"b\".\n" ); } + // read configuration data for extension "j" + else if ( *pCur == 'j' ) + { + int nSize, Reserved, NumCellTypes, CellId, BytesPerInstance, TotalInstances; + pCur++; + nSize = Gia_AigerReadInt(pCur); + pCurTemp = pCur + nSize + 4; pCur += 4; + // Read reserved value (should be 0) + Reserved = Gia_AigerReadInt(pCur); pCur += 4; + assert( Reserved == 0 ); + // Read number of cell types + NumCellTypes = Gia_AigerReadInt(pCur); pCur += 4; + // Skip cell type definitions (we know them already) + for ( i = 0; i < NumCellTypes; i++ ) + { + CellId = Gia_AigerReadInt(pCur); pCur += 4; + // Skip function description string (null-terminated) + while ( *pCur++ != '\0' ); + BytesPerInstance = Gia_AigerReadInt(pCur); pCur += 4; + } + // Read total number of instances + TotalInstances = Gia_AigerReadInt(pCur); pCur += 4; + // Create byte vector for instance data + pNew->vConfigs2 = Vec_StrAlloc( (int)(pCurTemp - pCur) ); + // Read instance data as bytes + while ( pCur < pCurTemp ) + Vec_StrPush( pNew->vConfigs2, *pCur++ ); + assert( pCur == pCurTemp ); + if ( fVerbose ) printf( "Finished reading extension \"j\".\n" ); + } // read choices else if ( *pCur == 'q' ) { @@ -1514,6 +1545,88 @@ void Gia_AigerWriteS( Gia_Man_t * pInit, char * pFileName, int fWriteSymbols, in for ( i = 0; i < Vec_IntSize(p->vConfigs); i++ ) Gia_FileWriteBufferSize( pFile, Vec_IntEntry(p->vConfigs, i) ); } + // write configuration data for extension "j" + if ( p->vConfigs2 ) + { + int nTotalSize, nInstances = 0; + If_LibCell_t * pLibCell = NULL; // (If_LibCell_t *)Abc_FrameReadLibCell(); + char *pCell0, *pCell1, *pCell2; + + // Get formulas from cell library or use defaults + if ( pLibCell && pLibCell->nCellNum == 3 && + pLibCell->pCellNames[0] && pLibCell->pCellNames[1] && pLibCell->pCellNames[2] ) + { + pCell0 = pLibCell->pCellNames[0]; + pCell1 = pLibCell->pCellNames[1]; + pCell2 = pLibCell->pCellNames[2]; + } + else + { + if ( !pLibCell ) + Abc_Print( 0, "Warning: Cell library is not loaded. Using generic formulas.\n" ); + else if ( pLibCell->nCellNum != 3 ) + Abc_Print( 0, "Warning: Cell library has %d cells (expected exactly 3). Using generic formulas.\n", pLibCell->nCellNum ); + else + Abc_Print( 0, "Warning: Cell library does not contain all required cells. Using generic formulas.\n" ); + pCell0 = "Formula1"; + pCell1 = "Formula2"; + pCell2 = "Formula3"; + } + // Count instances by scanning the byte data + for ( i = 0; i < Vec_StrSize(p->vConfigs2); ) + { + unsigned char CellId = (unsigned char)Vec_StrEntry(p->vConfigs2, i); + if ( CellId == 0 ) + i += 4; // 1 byte CellId + 2 bytes truth table + 1 padding + else if ( CellId == 1 ) + i += 12; // 1 byte CellId + 4 bytes mapping + 4 bytes truth tables + 3 padding + else if ( CellId == 2 ) + i += 12; // 1 byte CellId + 5 bytes mapping + 4 bytes truth tables + 2 padding + else + assert( 0 ); // Unknown cell type + nInstances++; + } + fprintf( pFile, "j" ); + // Calculate total size + nTotalSize = 4; // Reserved value + nTotalSize += 4; // Number of cell types + // Cell type 0 + nTotalSize += 4; // CellId + nTotalSize += strlen(pCell0) + 1; // Function description + nTotalSize += 4; // Bytes per instance + // Cell type 1 + nTotalSize += 4; // CellId + nTotalSize += strlen(pCell1) + 1; // Function description + nTotalSize += 4; // Bytes per instance + // Cell type 2 + nTotalSize += 4; // CellId + nTotalSize += strlen(pCell2) + 1; // Function description + nTotalSize += 4; // Bytes per instance + // Instance data + nTotalSize += 4; // Total instances count + nTotalSize += Vec_StrSize(p->vConfigs2); // Actual instance data + Gia_FileWriteBufferSize( pFile, nTotalSize ); + // Write reserved value + Gia_FileWriteBufferSize( pFile, 0 ); + // Write number of cell types + Gia_FileWriteBufferSize( pFile, 3 ); + // Write cell type 0 (LUT4) + Gia_FileWriteBufferSize( pFile, 0 ); // CellId + fwrite( pCell0, 1, strlen(pCell0) + 1, pFile ); + Gia_FileWriteBufferSize( pFile, 4 ); // 1 byte CellId + 2 bytes truth table, rounded to 4 + // Write cell type 1 (S44) + Gia_FileWriteBufferSize( pFile, 1 ); // CellId + fwrite( pCell1, 1, strlen(pCell1) + 1, pFile ); + Gia_FileWriteBufferSize( pFile, 12 ); // 1 byte CellId + 4 bytes mapping + 4 bytes truth tables, rounded to 12 + // Write cell type 2 (9-input) + Gia_FileWriteBufferSize( pFile, 2 ); // CellId + fwrite( pCell2, 1, strlen(pCell2) + 1, pFile ); + Gia_FileWriteBufferSize( pFile, 12 ); // 1 byte CellId + 5 bytes mapping + 4 bytes truth tables (LUT4s only), rounded to 12 + // Write total instances + Gia_FileWriteBufferSize( pFile, nInstances ); + // Write instance data as raw bytes + fwrite( Vec_StrArray(p->vConfigs2), 1, Vec_StrSize(p->vConfigs2), pFile ); + } // write choices if ( Gia_ManHasChoices(p) ) { diff --git a/src/aig/gia/giaDup.c b/src/aig/gia/giaDup.c index c72582b05..ea58ba8b2 100644 --- a/src/aig/gia/giaDup.c +++ b/src/aig/gia/giaDup.c @@ -790,6 +790,8 @@ Gia_Man_t * Gia_ManDupWithAttributes( Gia_Man_t * p ) pNew->vRegInits = Vec_IntDup( p->vRegInits ); if ( p->vConfigs ) pNew->vConfigs = Vec_IntDup( p->vConfigs ); + if ( p->vConfigs2 ) + pNew->vConfigs2 = Vec_StrDup( p->vConfigs2 ); if ( p->pCellStr ) pNew->pCellStr = Abc_UtilStrsav( p->pCellStr ); // copy names if present diff --git a/src/aig/gia/giaIf.c b/src/aig/gia/giaIf.c index 0ce43a351..c386dbcb9 100644 --- a/src/aig/gia/giaIf.c +++ b/src/aig/gia/giaIf.c @@ -1188,11 +1188,13 @@ int Gia_ManFromIfLogicCreateLutSpecial( Gia_Man_t * pNew, word * pRes, Vec_Int_t ***********************************************************************/ int Gia_ManFromIfLogicCreateLutSpecialJ( Gia_Man_t * pNew, word * pRes, Vec_Int_t * vLeaves, Vec_Int_t * vLeavesTemp, Vec_Int_t * vCover, Vec_Int_t * vMapping, Vec_Int_t * vMapping2, Vec_Int_t * vPacking ) { - word z = If_CutPerformDeriveJ( NULL, (unsigned *)pRes, Vec_IntSize(vLeaves), Vec_IntSize(vLeaves), NULL, 1 ); + return Gia_ManFromIfLogicCreateLut( pNew, pRes, vLeaves, vCover, vMapping, vMapping2 ); + word Truth; int i, iObjLit1, iObjLit2, iObjLit3; - - if ( ((z >> 63) & 1) == 0 ) // S44 decomposition + word z = If_CutPerformDeriveJ( NULL, (unsigned *)pRes, Vec_IntSize(vLeaves), Vec_IntSize(vLeaves), NULL, 1 ); + assert( z != 0 ); + if ( ((z >> 63) & 1) == 0 ) { // create first LUT Vec_IntClear( vLeavesTemp ); @@ -1292,7 +1294,7 @@ int Gia_ManFromIfLogicCreateLutSpecialJ( Gia_Man_t * pNew, word * pRes, Vec_Int_ ***********************************************************************/ int Gia_ManFromIfLogicNode( void * pIfMan, Gia_Man_t * pNew, int iObj, Vec_Int_t * vLeaves, Vec_Int_t * vLeavesTemp, - word * pRes, char * pStr, Vec_Int_t * vCover, Vec_Int_t * vMapping, Vec_Int_t * vMapping2, Vec_Int_t * vPacking, int fCheck75, int fCheck44e ) + word * pRes, char * pStr, Vec_Int_t * vCover, Vec_Int_t * vMapping, Vec_Int_t * vMapping2, Vec_Int_t * vPacking, int fCheck75, int fEnableCheck07 ) { int nLeaves = Vec_IntSize(vLeaves); int i, Length, nLutLeaf, nLutLeaf2, nLutRoot, iObjLit1, iObjLit2, iObjLit3; @@ -1300,9 +1302,9 @@ int Gia_ManFromIfLogicNode( void * pIfMan, Gia_Man_t * pNew, int iObj, Vec_Int_t if ( fCheck75 ) pStr = "54"; // perform special case matching for 44 - if ( fCheck44e ) - { - if ( Vec_IntSize(vLeaves) <= 5 ) + if ( fEnableCheck07 ) + { + if ( 0 && Vec_IntSize(vLeaves) <= 4 ) { // create mapping iObjLit1 = Gia_ManFromIfLogicCreateLut( pNew, pRes, vLeaves, vCover, vMapping, vMapping2 ); @@ -1314,7 +1316,7 @@ int Gia_ManFromIfLogicNode( void * pIfMan, Gia_Man_t * pNew, int iObj, Vec_Int_t Vec_IntAddToEntry( vPacking, 0, 1 ); } return iObjLit1; - } + } return Gia_ManFromIfLogicCreateLutSpecialJ( pNew, pRes, vLeaves, vLeavesTemp, vCover, vMapping, vMapping2, vPacking ); } if ( ((If_Man_t *)pIfMan)->pPars->fLut6Filter && Vec_IntSize(vLeaves) == 6 ) @@ -1916,6 +1918,234 @@ void Gia_ManFromIfGetConfig( Vec_Int_t * vConfigs, If_Man_t * pIfMan, If_Cut_t * Vec_StrPush( vConfigsStr, '\n' ); } } +/**Function************************************************************* + + Synopsis [Print configuration during encoding.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Gia_ManConfigPrint( word Truth4, word z, int nLeaves ) +{ + static int Count = 0; + int i; + printf( "[%4d] Encoding (nLeaves=%d): ", Count++, nLeaves ); + // Simple LUT4 case (Truth4 != 0, z == 0) + if ( z == 0 ) + { + printf( "%04lX{", (unsigned long)(Truth4 & 0xFFFF) ); + for ( i = 0; i < nLeaves && i < 4; i++ ) + printf( "%c", 'a' + i ); + printf( "} [Cell 0, LUT4]\n" ); + return; + } + if ( ((z >> 63) & 1) == 0 ) + { + // Extract truth tables + word Truth1 = z & 0xFFFF; + word Truth2 = (z >> 32) & 0xFFFF; + printf( "h=%04lX{", (unsigned long)Truth1 ); + // First LUT4 inputs from bits 16-31 + for ( i = 0; i < 4; i++ ) + { + int v = (int)((z >> (16 + (i << 2))) & 7); + if ( v == 6 && nLeaves == 5 ) + printf( "0" ); // Constant 0 for 5-input cuts + else if ( v == 7 ) + printf( "?" ); // Internal connection (shouldn't appear in first LUT) + else if ( v <= 6 ) + printf( "%c", 'a' + v ); + else + printf( "?" ); + } + printf( "} "); + printf( "i=%04lX{", (unsigned long)Truth2 ); + // Second LUT4 inputs from bits 48-63 + for ( i = 0; i < 4; i++ ) + { + int v = (int)((z >> (48 + (i << 2))) & 7); + if ( v == 6 && nLeaves == 5 ) + printf( "0" ); // Constant 0 for 5-input cuts + else if ( v == 7 ) + printf( "h" ); // Output of first LUT + else if ( v <= 6 ) + printf( "%c", 'a' + v ); + else + printf( "?" ); + } + printf( "} [Cell 1, S44]\n" ); + } + else + { + int Pla2Var[9]; + extern void If_PermUnpack( unsigned Value, int Pla2Var[9] ); + If_PermUnpack( (unsigned)(z >> 32), Pla2Var ); + // Extract truth tables + word Truth1 = z & 0xFFFF; + word Truth2 = (z >> 16) & 0xFFFF; + printf( "j=%04lX{", (unsigned long)Truth1 ); + // First LUT4 inputs + for ( i = 0; i < 4; i++ ) + { + if ( Pla2Var[i] == 9 ) + printf( "0" ); // Will be encoded as constant 0 + else if ( Pla2Var[i] < 9 ) + printf( "%c", 'a' + Pla2Var[i] ); + else + printf( "?" ); + } + printf( "} "); + printf( "k=%04lX{", (unsigned long)Truth2 ); + // Second LUT4 inputs + for ( i = 4; i < 8; i++ ) + { + if ( Pla2Var[i] == 9 ) + printf( "0" ); // Will be encoded as constant 0 + else if ( Pla2Var[i] < 9 ) + printf( "%c", 'a' + Pla2Var[i] ); + else + printf( "?" ); + } + printf( "} "); + // final + printf( "l=<" ); + if ( Pla2Var[8] == 9 ) + printf( "0" ); // Will be encoded as constant 0 + else if ( Pla2Var[8] < 9 ) + printf( "%c", 'a' + Pla2Var[8] ); + else + printf( "?" ); + printf( "jk> [Cell 2, 9-input MUX]\n" ); + } +} + +/**Function************************************************************* + + Synopsis [Derive configurations.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Gia_ManFromIfGetConfig2( Vec_Str_t * vConfigs2, If_Man_t * pIfMan, If_Cut_t * pCutBest ) +{ + int i, CellId, nBytes; + int startPos = Vec_StrSize(vConfigs2); + + // Determine cell type based on the number of leaves and configuration + if ( pCutBest->nLeaves <= 4 ) + { + // Cell type 0: Simple LUT4 + CellId = 0; + nBytes = 3; // 1 byte CellId + 2 bytes truth table (16 bits) + // Write CellId + Vec_StrPush( vConfigs2, (char)CellId ); + // Write truth table (16 bits for LUT4) + word Truth = *If_CutTruthW(pIfMan, pCutBest); + Vec_StrPush( vConfigs2, (char)(Truth & 0xFF) ); + Vec_StrPush( vConfigs2, (char)((Truth >> 8) & 0xFF) ); + // Pad to 4-byte boundary + while ( (Vec_StrSize(vConfigs2) - startPos) % 4 != 0 ) + Vec_StrPush( vConfigs2, 0 ); + //Gia_ManConfigPrint( Truth, 0, pCutBest->nLeaves ); + } + else + { + word z = If_CutPerformDeriveJ( pIfMan, (unsigned *)If_CutTruthW(pIfMan, pCutBest), pCutBest->nLeaves, pCutBest->nLeaves, NULL, 1 ); + //Gia_ManConfigPrint( 0, z, pCutBest->nLeaves ); + if ( ((z >> 63) & 1) == 0 ) + { + CellId = 1; + unsigned char mappingBytes[4] = {0}; + // Write CellId + Vec_StrPush( vConfigs2, (char)CellId ); + // Write input mappings for first LUT4 (4 inputs) + for ( i = 0; i < 4; i++ ) + { + int v = (int)((z >> (16 + (i << 2))) & 7); + if ( v == 6 && pCutBest->nLeaves == 5 ) + mappingBytes[i / 2] |= (0 << ((i % 2) * 4)); // constant 0 + else + mappingBytes[i / 2] |= ((v+2) << ((i % 2) * 4)); // leaf v (direct mapping) + } + Vec_StrPush( vConfigs2, (char)mappingBytes[0] ); + Vec_StrPush( vConfigs2, (char)mappingBytes[1] ); + // Write input mappings for second LUT4 (4 inputs) + mappingBytes[0] = mappingBytes[1] = 0; + for ( i = 0; i < 4; i++ ) + { + int v = (int)((z >> (48 + (i << 2))) & 7); + if ( v == 6 && pCutBest->nLeaves == 5 ) + mappingBytes[i / 2] |= (0 << ((i % 2) * 4)); // constant 0 + else if ( v == 7 ) + mappingBytes[i / 2] |= ((7+2) << ((i % 2) * 4)); // output of first LUT at index N+2 where N=7 + else + mappingBytes[i / 2] |= ((v+2) << ((i % 2) * 4)); // leaf v (direct mapping) + } + Vec_StrPush( vConfigs2, (char)mappingBytes[0] ); + Vec_StrPush( vConfigs2, (char)mappingBytes[1] ); + // Write truth tables + word Truth1 = z & 0xFFFF; + word Truth2 = (z >> 32) & 0xFFFF; + Vec_StrPush( vConfigs2, (char)(Truth1 & 0xFF) ); + Vec_StrPush( vConfigs2, (char)((Truth1 >> 8) & 0xFF) ); + Vec_StrPush( vConfigs2, (char)(Truth2 & 0xFF) ); + Vec_StrPush( vConfigs2, (char)((Truth2 >> 8) & 0xFF) ); + // Pad to 4-byte boundary + while ( (Vec_StrSize(vConfigs2) - startPos) % 4 != 0 ) + Vec_StrPush( vConfigs2, 0 ); + } + else + { + CellId = 2; + int Pla2Var[9]; + extern void If_PermUnpack( unsigned Value, int Pla2Var[9] ); + If_PermUnpack( (unsigned)(z >> 32), Pla2Var ); + // Write CellId + Vec_StrPush( vConfigs2, (char)CellId ); + // Write input mappings (9 inputs, 4 bits each, packed) + unsigned char mappingByte = 0; + int bitPos = 0; + for ( i = 0; i < 9; i++ ) + { + int v; + if ( Pla2Var[i] == 9 ) // constant 0 + v = 0; + else // leaf index + v = Pla2Var[i] + 2; + if ( bitPos == 0 ) { + mappingByte = v & 0xF; + bitPos = 4; + } + else { + mappingByte |= (v & 0xF) << 4; + Vec_StrPush( vConfigs2, (char)mappingByte ); + bitPos = 0; + } + } + // Push last byte if needed + if ( bitPos != 0 ) + Vec_StrPush( vConfigs2, (char)mappingByte ); + // Write truth tables for the two LUT4s only (MUX is structural, not a LUT) + word Truth1 = z & 0xFFFF; + word Truth2 = (z >> 16) & 0xFFFF; + Vec_StrPush( vConfigs2, (char)(Truth1 & 0xFF) ); + Vec_StrPush( vConfigs2, (char)((Truth1 >> 8) & 0xFF) ); + Vec_StrPush( vConfigs2, (char)(Truth2 & 0xFF) ); + Vec_StrPush( vConfigs2, (char)((Truth2 >> 8) & 0xFF) ); + // Pad to 4-byte boundary + while ( (Vec_StrSize(vConfigs2) - startPos) % 4 != 0 ) + Vec_StrPush( vConfigs2, 0 ); + } + } +} int Gia_ManFromIfLogicFindCell( If_Man_t * pIfMan, Gia_Man_t * pNew, Gia_Man_t * pTemp, If_Cut_t * pCutBest, Ifn_Ntk_t * pNtkCell, int nLutMax, Vec_Int_t * vLeaves, Vec_Int_t * vLits, Vec_Int_t * vCover, Vec_Int_t * vMapping, Vec_Int_t * vMapping2, Vec_Int_t * vConfigs ) { int iLit; @@ -2109,14 +2339,15 @@ Gia_Man_t * Gia_ManFromIfLogic( If_Man_t * pIfMan ) If_Cut_t * pCutBest; If_Obj_t * pIfObj, * pIfLeaf; Vec_Int_t * vMapping, * vMapping2, * vPacking = NULL, * vConfigs = NULL; + Vec_Str_t * vConfigs2 = NULL; Vec_Int_t * vLeaves, * vLeaves2, * vCover, * vLits; Vec_Str_t * vConfigsStr = NULL; Ifn_Ntk_t * pNtkCell = NULL; sat_solver * pSat = NULL; int i, k, Entry; assert( !pIfMan->pPars->fDeriveLuts || pIfMan->pPars->fTruth ); -// if ( pIfMan->pPars->fEnableCheck07 ) -// pIfMan->pPars->fDeriveLuts = 0; + //if ( pIfMan->pPars->fEnableCheck07 ) + // pIfMan->pPars->fDeriveLuts = 0; // start mapping and packing vMapping = Vec_IntStart( If_ManObjNum(pIfMan) ); vMapping2 = Vec_IntStart( 1 ); @@ -2136,6 +2367,8 @@ Gia_Man_t * Gia_ManFromIfLogic( If_Man_t * pIfMan ) if ( fWriteConfigs ) vConfigsStr = Vec_StrAlloc( 1000 ); } + if ( pIfMan->pPars->fEnableCheck07 ) + vConfigs2 = Vec_StrAlloc( 1000 ); // create new manager pNew = Gia_ManStart( If_ManObjNum(pIfMan) ); // iterate through nodes used in the mapping @@ -2223,6 +2456,12 @@ Gia_Man_t * Gia_ManFromIfLogic( If_Man_t * pIfMan ) pIfObj->iCopy = Abc_LitNotCond( pIfObj->iCopy, pCutBest->fCompl ); if ( vConfigs && Vec_IntSize(vLeaves) > 1 && !Gia_ObjIsCi(Gia_ManObj(pNew, Abc_Lit2Var(pIfObj->iCopy))) && pIfObj->iCopy > 1 ) Gia_ManFromIfGetConfig( vConfigs, pIfMan, pCutBest, pIfObj->iCopy, vConfigsStr ); + else if ( vConfigs2 && Vec_IntSize(vLeaves) > 1 && !Gia_ObjIsCi(Gia_ManObj(pNew, Abc_Lit2Var(pIfObj->iCopy))) && pIfObj->iCopy > 1 ) { + assert( pCutBest->fCompl == 0 ); + //pCutBest->iCutFunc = Abc_LitNotCond( pCutBest->iCutFunc, Abc_LitIsCompl(pIfObj->iCopy) ); + Gia_ManFromIfGetConfig2( vConfigs2, pIfMan, pCutBest ); + //pCutBest->iCutFunc = Abc_LitNotCond( pCutBest->iCutFunc, Abc_LitIsCompl(pIfObj->iCopy) ); + } } else { @@ -2235,6 +2474,8 @@ Gia_Man_t * Gia_ManFromIfLogic( If_Man_t * pIfMan ) Vec_IntForEachEntry( vLeaves, Entry, k ) Vec_IntPush( vMapping2, Abc_Lit2Var(Entry) ); Vec_IntPush( vMapping2, Abc_Lit2Var(pIfObj->iCopy) ); + //if ( pIfMan->pPars->fEnableCheck07 && vConfigs2 && Vec_IntSize(vLeaves) > 1 ) + // Gia_ManFromIfGetConfig2( vConfigs2, pIfMan, pCutBest ); } } else if ( If_ObjIsCi(pIfObj) ) @@ -2279,11 +2520,14 @@ Gia_Man_t * Gia_ManFromIfLogic( If_Man_t * pIfMan ) assert( pNew->vPacking == NULL ); assert( pNew->vConfigs == NULL ); assert( pNew->pCellStr == NULL ); + assert( pNew->vConfigs2== NULL ); pNew->vMapping = vMapping; pNew->vPacking = vPacking; pNew->vConfigs = vConfigs; pNew->pCellStr = vConfigs ? Abc_UtilStrsav( If_DsdManGetCellStr(pIfMan->pIfDsdMan) ) : NULL; - assert( !vConfigs || Vec_IntSize(vConfigs) == 2 + Vec_IntEntry(vConfigs, 0) * Vec_IntEntry(vConfigs, 1) ); + pNew->vConfigs2= vConfigs2; + assert( !vConfigs || Vec_IntSize(vConfigs) == 2 + Vec_IntEntry(vConfigs, 0) * Vec_IntEntry(vConfigs, 1) ); + // vConfigs2 is now a byte vector, no fixed size relationship // verify that COs have mapping { Gia_Obj_t * pObj; @@ -2503,6 +2747,10 @@ void Gia_ManTransferTiming( Gia_Man_t * p, Gia_Man_t * pGia ) p->vConfigs = pGia->vConfigs; pGia->vConfigs = NULL; p->pCellStr = pGia->pCellStr; pGia->pCellStr = NULL; } + if ( pGia->vConfigs2 ) + { + p->vConfigs2 = pGia->vConfigs2; pGia->vConfigs2 = NULL; + } if ( pGia->pManTime == NULL ) return; p->pManTime = pGia->pManTime; pGia->pManTime = NULL; @@ -2628,6 +2876,7 @@ Gia_Man_t * Gia_ManPerformMappingInt( Gia_Man_t * p, If_Par_t * pPars ) */ ABC_FREE( p->pCellStr ); Vec_IntFreeP( &p->vConfigs ); + Vec_StrFreeP( &p->vConfigs2 ); // disable cut minimization when GIA strucure is needed if ( !pPars->fDelayOpt && !pPars->fDelayOptLut && !pPars->fDsdBalance && !pPars->fUserRecLib && !pPars->fUserSesLib && !pPars->fDeriveLuts && !pPars->fUseDsd && !pPars->fUseTtPerm && !pPars->pFuncCell2 ) pPars->fCutMin = 0; diff --git a/src/aig/gia/giaMan.c b/src/aig/gia/giaMan.c index efedcfb0a..72ec211ef 100644 --- a/src/aig/gia/giaMan.c +++ b/src/aig/gia/giaMan.c @@ -142,6 +142,7 @@ void Gia_ManStop( Gia_Man_t * p ) Vec_IntFreeP( &p->vCellMapping ); Vec_IntFreeP( &p->vPacking ); Vec_IntFreeP( &p->vConfigs ); + Vec_StrFreeP( &p->vConfigs2 ); ABC_FREE( p->pCellStr ); Vec_FltFreeP( &p->vInArrs ); Vec_FltFreeP( &p->vOutReqs ); diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c index 56993e208..2787c0a82 100644 --- a/src/base/abci/abc.c +++ b/src/base/abci/abc.c @@ -35644,6 +35644,8 @@ int Abc_CommandAbc9Strash( Abc_Frame_t * pAbc, int argc, char ** argv ) Gia_ManTransferPacking( pTemp, pAbc->pGia ); Gia_ManTransferTiming( pTemp, pAbc->pGia ); } + else if ( Gia_ManHasMapping(pAbc->pGia) && pAbc->pGia->vConfigs2 ) + pTemp = (Gia_Man_t *)If_ManDeriveGiaFromCells2( pAbc->pGia ); else if ( Gia_ManHasMapping(pAbc->pGia) && pAbc->pGia->vConfigs ) pTemp = (Gia_Man_t *)If_ManDeriveGiaFromCells( pAbc->pGia ); else if ( Gia_ManHasMapping(pAbc->pGia) ) @@ -35692,6 +35694,7 @@ int Abc_CommandAbc9Strash( Abc_Frame_t * pAbc, int argc, char ** argv ) Gia_ManTransferTiming( pTemp, pAbc->pGia ); pAbc->pGia->vConfigs = pTemp->vConfigs; pTemp->vConfigs = NULL; pAbc->pGia->pCellStr = pTemp->pCellStr; pTemp->pCellStr = NULL; + pAbc->pGia->vConfigs2= pTemp->vConfigs2; pTemp->vConfigs2= NULL; } Abc_FrameUpdateGia( pAbc, pTemp ); return 0; diff --git a/src/map/if/ifTune.c b/src/map/if/ifTune.c index 9195fc8e0..47d90b4fd 100644 --- a/src/map/if/ifTune.c +++ b/src/map/if/ifTune.c @@ -892,6 +892,342 @@ void * If_ManDeriveGiaFromCells( void * pGia ) } +/**Function************************************************************* + + Synopsis [Print cell configuration data.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void If_ManConfigPrint( unsigned char * pConfigData, int nLeaves ) +{ + unsigned char CellId = pConfigData[0]; + int i; + static int Count = 0; + printf( "[%4d] ", Count++ ); // Print instance number + if ( CellId == 0 ) + { + // Extract 16-bit truth table + word Truth = ((word)pConfigData[2] << 8) | pConfigData[1]; + printf( "%04lX{", (unsigned long)Truth ); + // Print as simple {abcd} since it's just a direct LUT4 + for ( i = 0; i < nLeaves && i < 4; i++ ) + printf( "%c", 'a' + i ); + printf( "}" ); + // Pad with spaces if less than 4 inputs + for ( i = nLeaves; i < 4; i++ ) + printf( " " ); + printf( " [Cell %d, %d leaves]\n", CellId, nLeaves ); + } + else if ( CellId == 1 ) + { + // First LUT4 + word Truth1 = ((word)pConfigData[6] << 8) | pConfigData[5]; + printf( "h=%04lX{", (unsigned long)Truth1 ); + for ( i = 0; i < 4; i++ ) + { + int v = (pConfigData[1 + i/2] >> ((i%2) * 4)) & 0xF; + if ( v == 0 ) + printf( "0"); + else if ( v == 1 ) + printf( "1"); + else if ( v >= 2 && v < 2 + nLeaves ) + printf( "%c", 'a' + (v-2)); + else + printf( "?"); + } + printf( "} "); + // Second LUT4 + word Truth2 = ((word)pConfigData[8] << 8) | pConfigData[7]; + printf( "i=%04lX{", (unsigned long)Truth2 ); + for ( i = 0; i < 4; i++ ) + { + int v = (pConfigData[3 + i/2] >> ((i%2) * 4)) & 0xF; + if ( v == 0 ) + printf( "0"); + else if ( v == 1 ) + printf( "1"); + else if ( v >= 2 && v < 2 + nLeaves ) + printf( "%c", 'a' + (v-2)); + else if ( v == 9 ) + printf( "h"); // Output of first LUT + else + printf( "?"); + } + printf( "} [Cell %d, %d leaves]\n", CellId, nLeaves ); + } + else if ( CellId == 2 ) + { + // Extract 9 input mappings + int inputs[9]; + int bitPos = 0; + for ( i = 0; i < 9; i++ ) + { + if ( bitPos == 0 ) + { + inputs[i] = pConfigData[1 + i/2] & 0xF; + bitPos = 4; + } + else + { + inputs[i] = (pConfigData[1 + i/2] >> 4) & 0xF; + bitPos = 0; + } + } + // First LUT4 + word Truth1 = ((word)pConfigData[7] << 8) | pConfigData[6]; + printf( "j=%04lX{", (unsigned long)Truth1 ); + for ( i = 0; i < 4; i++ ) + { + int v = inputs[i]; + if ( v == 0 ) + printf( "0"); + else if ( v == 1 ) + printf( "1"); + else if ( v >= 2 && v < 2 + nLeaves ) + printf( "%c", 'a' + (v-2)); + else + printf( "?"); + } + printf( "} "); + // Second LUT4 + word Truth2 = ((word)pConfigData[9] << 8) | pConfigData[8]; + printf( "k=%04lX{", (unsigned long)Truth2 ); + for ( i = 4; i < 8; i++ ) + { + int v = inputs[i]; + if ( v == 0 ) + printf( "0"); + else if ( v == 1 ) + printf( "1"); + else if ( v >= 2 && v < 2 + nLeaves ) + printf( "%c", 'a' + (v-2)); + else + printf( "?"); + } + printf( "} "); + // final node + printf( "l=<"); + int v = inputs[8]; + if ( v == 0 ) + printf( "0"); + else if ( v == 1 ) + printf( "1"); + else if ( v >= 2 && v < 2 + nLeaves ) + printf( "%c", 'a' + (v-2)); + else + printf( "?"); + printf( "jk> [Cell %d, %d leaves]\n", CellId, nLeaves ); + } + else + { + printf( "Unknown cell type %d!\n", CellId ); + } +} + +/**Function************************************************************* + + Synopsis [Derive GIA using programmable bits.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void * If_ManDeriveGiaFromCells2( void * pGia ) +{ + Gia_Man_t * p = (Gia_Man_t *)pGia; + Gia_Man_t * pNew, * pTemp; + Vec_Int_t * vCover, * vLeaves; + Gia_Obj_t * pObj; + unsigned char * pConfigData; + int k, i, iLut, iVar; + int Count = 0; + assert( p->vConfigs2 != NULL ); + assert( Gia_ManHasMapping(p) ); + // create new manager + pNew = Gia_ManStart( 6*Gia_ManObjNum(p)/5 + 100 ); + pNew->pName = Abc_UtilStrsav( p->pName ); + pNew->pSpec = Abc_UtilStrsav( p->pSpec ); + // map primary inputs + Gia_ManFillValue(p); + Gia_ManConst0(p)->Value = 0; + Gia_ManForEachCi( p, pObj, i ) + pObj->Value = Gia_ManAppendCi(pNew); + // iterate through nodes used in the mapping + vLeaves = Vec_IntAlloc( 16 ); + vCover = Vec_IntAlloc( 1 << 16 ); + Gia_ManHashStart( pNew ); + // Process each mapped node + int bytePos = 0; + Gia_ManForEachAnd( p, pObj, iLut ) + { + if ( Gia_ObjIsBuf(pObj) ) + { + pObj->Value = Gia_ManAppendBuf( pNew, Gia_ObjFanin0Copy(pObj) ); + continue; + } + if ( !Gia_ObjIsLut(p, iLut) ) + continue; + + // collect incoming literals + Vec_IntClear( vLeaves ); + Gia_LutForEachFanin( p, iLut, iVar, k ) + Vec_IntPush( vLeaves, Gia_ManObj(p, iVar)->Value ); + // Get configuration data for this instance + pConfigData = (unsigned char *)Vec_StrEntryP( p->vConfigs2, bytePos ); + //If_ManConfigPrint( pConfigData, Vec_IntSize(vLeaves) ); + unsigned char CellId = pConfigData[0]; + if ( CellId == 0 ) + { + // Extract 16-bit truth table + word Truth = ((word)pConfigData[2] << 8) | pConfigData[1]; + Truth = Abc_Tt6Stretch( Truth, 4 ); + extern int Kit_TruthToGia( Gia_Man_t * pMan, unsigned * pTruth, int nVars, Vec_Int_t * vMemory, Vec_Int_t * vLeaves, int fHash ); + Gia_ManObj(p, iLut)->Value = Kit_TruthToGia( pNew, (unsigned *)&Truth, Vec_IntSize(vLeaves), vCover, vLeaves, 1 ); + bytePos += 4; // 1 byte CellId + 2 bytes truth table + 1 padding + } + else if ( CellId == 1 ) + { + Vec_Int_t * vLeavesTemp = Vec_IntAlloc( 4 ); + int iObjLit1, iObjLit2; + // First LUT4 - extract inputs and truth table + Vec_IntClear( vLeavesTemp ); + for ( i = 0; i < 4; i++ ) + { + int v = (pConfigData[1 + i/2] >> ((i%2) * 4)) & 0xF; + if ( v == 0 ) + Vec_IntPush( vLeavesTemp, 0 ); // constant 0 + else if ( v == 1 ) + Vec_IntPush( vLeavesTemp, 1 ); // constant 1 + else if ( v >= 2 && v < 2 + Vec_IntSize(vLeaves) ) + Vec_IntPush( vLeavesTemp, Vec_IntEntry(vLeaves, v - 2) ); // leaf (v-2) + else + assert( 0 ); // Invalid value + } + word Truth1 = ((word)pConfigData[6] << 8) | pConfigData[5]; + Truth1 = Abc_Tt6Stretch( Truth1, 4 ); + extern int Kit_TruthToGia( Gia_Man_t * pMan, unsigned * pTruth, int nVars, Vec_Int_t * vMemory, Vec_Int_t * vLeaves, int fHash ); + iObjLit1 = Kit_TruthToGia( pNew, (unsigned *)&Truth1, Vec_IntSize(vLeavesTemp), vCover, vLeavesTemp, 1 ); + // Second LUT4 - extract inputs and truth table + Vec_IntClear( vLeavesTemp ); + for ( i = 0; i < 4; i++ ) + { + int v = (pConfigData[3 + i/2] >> ((i%2) * 4)) & 0xF; + if ( v == 0 ) + Vec_IntPush( vLeavesTemp, 0 ); // constant 0 + else if ( v == 1 ) + Vec_IntPush( vLeavesTemp, 1 ); // constant 1 + else if ( v >= 2 && v < 2 + Vec_IntSize(vLeaves) ) + Vec_IntPush( vLeavesTemp, Vec_IntEntry(vLeaves, v - 2) ); // leaf (v-2) + else if ( v == 9 ) // N+2 where N=7 (number of S44 inputs) + Vec_IntPush( vLeavesTemp, iObjLit1 ); // output of first LUT (internal connection) + else + assert( 0 ); // Invalid value + } + word Truth2 = ((word)pConfigData[8] << 8) | pConfigData[7]; + Truth2 = Abc_Tt6Stretch( Truth2, 4 ); + iObjLit2 = Kit_TruthToGia( pNew, (unsigned *)&Truth2, Vec_IntSize(vLeavesTemp), vCover, vLeavesTemp, 1 ); + Gia_ManObj(p, iLut)->Value = iObjLit2; + Vec_IntFree( vLeavesTemp ); + bytePos += 12; // 1 byte CellId + 4 bytes mapping + 4 bytes truth tables + 3 padding + } + else if ( CellId == 2 ) + { + Vec_Int_t * vLeavesTemp = Vec_IntAlloc( 4 ); + int iObjLit1, iObjLit2, iObjLit3; + // Extract 9 input mappings (4 bits each, packed) + int inputs[9]; + int bitPos = 0; + for ( i = 0; i < 9; i++ ) + { + if ( bitPos == 0 ) + { + inputs[i] = pConfigData[1 + i/2] & 0xF; + bitPos = 4; + } + else + { + inputs[i] = (pConfigData[1 + i/2] >> 4) & 0xF; + bitPos = 0; + } + } + // First LUT4 (inputs 0-3) + Vec_IntClear( vLeavesTemp ); + for ( i = 0; i < 4; i++ ) + { + int v = inputs[i]; + if ( v == 0 ) + Vec_IntPush( vLeavesTemp, 0 ); // constant 0 + else if ( v == 1 ) + Vec_IntPush( vLeavesTemp, 1 ); // constant 1 + else if ( v >= 2 && v < 2 + Vec_IntSize(vLeaves) ) + Vec_IntPush( vLeavesTemp, Vec_IntEntry(vLeaves, v - 2) ); // leaf (v-2) + else + assert( 0 ); // Invalid value + } + word Truth1 = ((word)pConfigData[7] << 8) | pConfigData[6]; + Truth1 = Abc_Tt6Stretch( Truth1, 4 ); + extern int Kit_TruthToGia( Gia_Man_t * pMan, unsigned * pTruth, int nVars, Vec_Int_t * vMemory, Vec_Int_t * vLeaves, int fHash ); + iObjLit1 = Kit_TruthToGia( pNew, (unsigned *)&Truth1, Vec_IntSize(vLeavesTemp), vCover, vLeavesTemp, 1 ); + // Second LUT4 (inputs 4-7) + Vec_IntClear( vLeavesTemp ); + for ( i = 4; i < 8; i++ ) + { + int v = inputs[i]; + if ( v == 0 ) + Vec_IntPush( vLeavesTemp, 0 ); // constant 0 + else if ( v == 1 ) + Vec_IntPush( vLeavesTemp, 1 ); // constant 1 + else if ( v >= 2 && v < 2 + Vec_IntSize(vLeaves) ) + Vec_IntPush( vLeavesTemp, Vec_IntEntry(vLeaves, v - 2) ); // leaf (v-2) + else + assert( 0 ); // Invalid value + } + word Truth2 = ((word)pConfigData[9] << 8) | pConfigData[8]; + Truth2 = Abc_Tt6Stretch( Truth2, 4 ); + iObjLit2 = Kit_TruthToGia( pNew, (unsigned *)&Truth2, Vec_IntSize(vLeavesTemp), vCover, vLeavesTemp, 1 ); + // MUX (select is input 8) - structural implementation + int iSelectLit; + int v = inputs[8]; + if ( v == 0 ) + iSelectLit = 0; // constant 0 select + else if ( v == 1 ) + iSelectLit = 1; // constant 1 select (unlikely for select) + else if ( v >= 2 && v < 2 + Vec_IntSize(vLeaves) ) + iSelectLit = Vec_IntEntry(vLeaves, v - 2); // select from leaf (v-2) + else + assert( 0 ); // Invalid value + iObjLit3 = Gia_ManHashMux( pNew, iSelectLit, iObjLit2, iObjLit1 ); + Gia_ManObj(p, iLut)->Value = iObjLit3; + Vec_IntFree( vLeavesTemp ); + bytePos += 12; // 1 byte CellId + 5 bytes mapping + 4 bytes truth tables + 2 padding + } + else + { + assert( 0 ); // Unknown cell type + } + Count++; + } + + Gia_ManForEachCo( p, pObj, i ) + pObj->Value = Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) ); + Gia_ManHashStop( pNew ); + Gia_ManSetRegNum( pNew, Gia_ManRegNum(p) ); + Vec_IntFree( vLeaves ); + Vec_IntFree( vCover ); + // perform cleanup + pNew = Gia_ManCleanup( pTemp = pNew ); + Gia_ManStop( pTemp ); + return pNew; +} + /**Function************************************************************* Synopsis [Derive truth table given the configulation values.] From 7c6b779327025589146a101a4da70f1552353b79 Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Sat, 1 Nov 2025 01:23:30 -0700 Subject: [PATCH 10/17] Supporting programmable cell libraries. --- src/base/main/main.h | 2 + src/base/main/mainFrame.c | 2 + src/base/main/mainInt.h | 1 + src/map/if/if.h | 17 +++ src/map/if/ifCom.c | 142 +++++++++++++++++++++++ src/map/if/ifLibLut.c | 234 ++++++++++++++++++++++++++++++++++++++ 6 files changed, 398 insertions(+) diff --git a/src/base/main/main.h b/src/base/main/main.h index 768cebd07..197d9036e 100644 --- a/src/base/main/main.h +++ b/src/base/main/main.h @@ -100,6 +100,7 @@ extern ABC_DLL Vec_Ptr_t * Abc_FrameReadStore(); extern ABC_DLL int Abc_FrameReadStoreSize(); extern ABC_DLL void * Abc_FrameReadLibLut(); extern ABC_DLL void * Abc_FrameReadLibLutI( int i ); +extern ABC_DLL void * Abc_FrameReadLibCell(); extern ABC_DLL void * Abc_FrameReadLibBox(); extern ABC_DLL void * Abc_FrameReadLibGen(); extern ABC_DLL void * Abc_FrameReadLibGen2(); @@ -139,6 +140,7 @@ extern ABC_DLL void Abc_FrameSetNtkStore( Abc_Ntk_t * pNtk ); extern ABC_DLL void Abc_FrameSetNtkStoreSize( int nStored ); extern ABC_DLL void Abc_FrameSetLibLut( void * pLib ); extern ABC_DLL void Abc_FrameSetLibLutI( void * pLib, int i ); +extern ABC_DLL void Abc_FrameSetLibCell( void * pLib ); extern ABC_DLL void Abc_FrameSetLibBox( void * pLib ); extern ABC_DLL void Abc_FrameSetLibGen( void * pLib ); extern ABC_DLL void Abc_FrameSetLibGen2( void * pLib ); diff --git a/src/base/main/mainFrame.c b/src/base/main/mainFrame.c index 4027f8ad7..f9093d02c 100644 --- a/src/base/main/mainFrame.c +++ b/src/base/main/mainFrame.c @@ -56,6 +56,7 @@ Vec_Ptr_t * Abc_FrameReadStore() { return s_GlobalFr int Abc_FrameReadStoreSize() { return Vec_PtrSize(s_GlobalFrame->vStore); } void * Abc_FrameReadLibLut() { return s_GlobalFrame->pLibLut[0]; } void * Abc_FrameReadLibLutI( int i ) { return s_GlobalFrame->pLibLut[i]; } +void * Abc_FrameReadLibCell() { return s_GlobalFrame->pLibCell; } void * Abc_FrameReadLibBox() { return s_GlobalFrame->pLibBox; } void * Abc_FrameReadLibGen() { return s_GlobalFrame->pLibGen; } void * Abc_FrameReadLibGen2() { return s_GlobalFrame->pLibGen2; } @@ -93,6 +94,7 @@ int * Abc_FrameOutputNdrArray( Abc_Frame_t * pAbc ) { int * pArray = s_ void Abc_FrameSetLibLut( void * pLib ) { s_GlobalFrame->pLibLut[0]= pLib; } void Abc_FrameSetLibLutI( void * pLib, int i ) { s_GlobalFrame->pLibLut[i]= pLib; } +void Abc_FrameSetLibCell( void * pLib ) { s_GlobalFrame->pLibCell = pLib; } void Abc_FrameSetLibBox( void * pLib ) { s_GlobalFrame->pLibBox = pLib; } void Abc_FrameSetLibGen( void * pLib ) { s_GlobalFrame->pLibGen = pLib; } void Abc_FrameSetLibGen2( void * pLib ) { s_GlobalFrame->pLibGen2 = pLib; } diff --git a/src/base/main/mainInt.h b/src/base/main/mainInt.h index 118b6916e..db98fbb3e 100644 --- a/src/base/main/mainInt.h +++ b/src/base/main/mainInt.h @@ -99,6 +99,7 @@ struct Abc_Frame_t_ void * pManDsd2; // decomposition manager // libraries for mapping void * pLibLut[ABC_LUT_LIBS]; // the current LUT library + void * pLibCell; // the current cell library void * pLibBox; // the current box library void * pLibGen; // the current genlib void * pLibGen2; // the current genlib diff --git a/src/map/if/if.h b/src/map/if/if.h index f5ea0b966..0252a467e 100644 --- a/src/map/if/if.h +++ b/src/map/if/if.h @@ -80,6 +80,7 @@ typedef struct If_Obj_t_ If_Obj_t; typedef struct If_Cut_t_ If_Cut_t; typedef struct If_Set_t_ If_Set_t; typedef struct If_LibLut_t_ If_LibLut_t; +typedef struct If_LibCell_t_ If_LibCell_t; typedef struct If_LibBox_t_ If_LibBox_t; typedef struct If_DsdMan_t_ If_DsdMan_t; typedef struct Ifn_Ntk_t_ Ifn_Ntk_t; @@ -194,6 +195,17 @@ struct If_LibLut_t_ float pLutDelays[IF_MAX_LUTSIZE+1][IF_MAX_LUTSIZE+1];// the delays of LUTs }; +// the cell library +struct If_LibCell_t_ +{ + char * pName; // the name of the LUT library + int nCellNum; // the number of cells in the library + int nCellInputs[IF_MAX_LUTSIZE]; + char * pCellNames[IF_MAX_LUTSIZE]; + float pCellAreas[IF_MAX_LUTSIZE]; + int pCellPinDelays[IF_MAX_LUTSIZE][IF_MAX_LUTSIZE]; +}; + // manager struct If_Man_t_ { @@ -626,6 +638,10 @@ extern int If_LibLutDelaysAreDifferent( If_LibLut_t * pLutLib ); extern If_LibLut_t * If_LibLutSetSimple( int nLutSize ); extern float If_LibLutFastestPinDelay( If_LibLut_t * p ); extern float If_LibLutSlowestPinDelay( If_LibLut_t * p ); +extern If_LibCell_t * If_LibCellRead( char * FileName ); +extern If_LibCell_t * If_LibCellDup( If_LibCell_t * p ); +extern void If_LibCellFree( If_LibCell_t * pCellLib ); +extern void If_LibCellPrint( If_LibCell_t * pCellLib ); /*=== ifLibBox.c =============================================================*/ extern If_LibBox_t * If_LibBoxStart(); extern void If_LibBoxFree( If_LibBox_t * p ); @@ -692,6 +708,7 @@ extern void * If_ManSatBuildFromCell( char * pStr, Vec_Int_t ** pvPiVar extern int If_ManSatFindCofigBits( void * pSat, Vec_Int_t * vPiVars, Vec_Int_t * vPoVars, word * pTruth, int nVars, word Perm, int nInps, Vec_Int_t * vValues ); extern int If_ManSatDeriveGiaFromBits( void * pNew, Ifn_Ntk_t * p, word * pTtData, Vec_Int_t * vLeaves, Vec_Int_t * vValues ); extern void * If_ManDeriveGiaFromCells( void * p ); +extern void * If_ManDeriveGiaFromCells2( void * p ); /*=== ifUtil.c ============================================================*/ extern void If_ManCleanNodeCopy( If_Man_t * p ); extern void If_ManCleanCutData( If_Man_t * p ); diff --git a/src/map/if/ifCom.c b/src/map/if/ifCom.c index 97fefea1d..8c401e843 100644 --- a/src/map/if/ifCom.c +++ b/src/map/if/ifCom.c @@ -30,6 +30,8 @@ ABC_NAMESPACE_IMPL_START static int If_CommandReadLut ( Abc_Frame_t * pAbc, int argc, char **argv ); static int If_CommandPrintLut( Abc_Frame_t * pAbc, int argc, char **argv ); +static int If_CommandReadCell( Abc_Frame_t * pAbc, int argc, char **argv ); +static int If_CommandPrintCell( Abc_Frame_t * pAbc, int argc, char **argv ); static int If_CommandReadBox ( Abc_Frame_t * pAbc, int argc, char **argv ); static int If_CommandPrintBox( Abc_Frame_t * pAbc, int argc, char **argv ); static int If_CommandWriteBox( Abc_Frame_t * pAbc, int argc, char **argv ); @@ -59,6 +61,9 @@ void If_Init( Abc_Frame_t * pAbc ) Cmd_CommandAdd( pAbc, "FPGA mapping", "read_lut", If_CommandReadLut, 0 ); Cmd_CommandAdd( pAbc, "FPGA mapping", "print_lut", If_CommandPrintLut, 0 ); + Cmd_CommandAdd( pAbc, "FPGA mapping", "read_cell", If_CommandReadCell, 0 ); + Cmd_CommandAdd( pAbc, "FPGA mapping", "print_cell", If_CommandPrintCell, 0 ); + Cmd_CommandAdd( pAbc, "FPGA mapping", "read_box", If_CommandReadBox, 0 ); Cmd_CommandAdd( pAbc, "FPGA mapping", "print_box", If_CommandPrintBox, 0 ); Cmd_CommandAdd( pAbc, "FPGA mapping", "write_box", If_CommandWriteBox, 0 ); @@ -248,6 +253,143 @@ usage: return 1; /* error exit */ } +/**Function************************************************************* + + Synopsis [Command procedure to read LUT libraries.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int If_CommandReadCell( Abc_Frame_t * pAbc, int argc, char **argv ) +{ + FILE * pFile; + FILE * pOut, * pErr; + If_LibCell_t * pLib; + Abc_Ntk_t * pNet; + char * FileName; + int fVerbose; + int c; + + pNet = Abc_FrameReadNtk(pAbc); + pOut = Abc_FrameReadOut(pAbc); + pErr = Abc_FrameReadErr(pAbc); + + // set the defaults + fVerbose = 1; + Extra_UtilGetoptReset(); + while ( (c = Extra_UtilGetopt(argc, argv, "vh")) != EOF ) + { + switch (c) + { + case 'v': + fVerbose ^= 1; + break; + case 'h': + goto usage; + break; + default: + goto usage; + } + } + + if ( argc == globalUtilOptind ) { + fprintf( pErr, "The library file should be specified in the command line.\n" ); + goto usage; + } + + // remove current libraries + If_LibCellFree( (If_LibCell_t *)Abc_FrameReadLibCell() ); + Abc_FrameSetLibCell( NULL ); + + // get the input file name + FileName = argv[globalUtilOptind]; + if ( (pFile = fopen( FileName, "r" )) == NULL ) + { + fprintf( pErr, "Cannot open input file \"%s\". ", FileName ); + if ( (FileName = Extra_FileGetSimilarName( FileName, ".genlib", ".lib", ".gen", ".g", NULL )) ) + fprintf( pErr, "Did you mean \"%s\"?", FileName ); + fprintf( pErr, "\n" ); + return 1; + } + fclose( pFile ); + // set the new network + pLib = If_LibCellRead( FileName ); + if ( pLib == NULL ) + { + fprintf( pErr, "Reading LUT library has failed.\n" ); + goto usage; + } + // replace the current library + Abc_FrameSetLibCell( pLib ); + return 0; + +usage: + fprintf( pErr, "\nusage: read_cell [-vh] \n"); + fprintf( pErr, "\t read the cell library from the file\n" ); + fprintf( pErr, "\t-v : toggles enabling of verbose output [default = %s]\n", (fVerbose? "yes" : "no") ); + fprintf( pErr, "\t-h : print the command usage\n"); + return 1; /* error exit */ +} + +/**Function************************************************************* + + Synopsis [Command procedure to read cell libraries.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int If_CommandPrintCell( Abc_Frame_t * pAbc, int argc, char **argv ) +{ + FILE * pOut, * pErr; + Abc_Ntk_t * pNet; + int fVerbose; + int c; + + pNet = Abc_FrameReadNtk(pAbc); + pOut = Abc_FrameReadOut(pAbc); + pErr = Abc_FrameReadErr(pAbc); + + // set the defaults + fVerbose = 1; + Extra_UtilGetoptReset(); + while ( (c = Extra_UtilGetopt(argc, argv, "vh")) != EOF ) + { + switch (c) + { + case 'v': + fVerbose ^= 1; + break; + case 'h': + goto usage; + break; + default: + goto usage; + } + } + + if ( argc != globalUtilOptind ) + goto usage; + + // set the new network + If_LibCellPrint( (If_LibCell_t *)Abc_FrameReadLibCell() ); + return 0; + +usage: + fprintf( pErr, "\nusage: print_cell [-vh]\n"); + fprintf( pErr, "\t print the current cell library\n" ); + fprintf( pErr, "\t-v : toggles enabling of verbose output [default = %s]\n", (fVerbose? "yes" : "no") ); + fprintf( pErr, "\t-h : print the command usage\n"); + return 1; /* error exit */ +} + /**Function************************************************************* Synopsis [] diff --git a/src/map/if/ifLibLut.c b/src/map/if/ifLibLut.c index 94946390a..4da141a97 100644 --- a/src/map/if/ifLibLut.c +++ b/src/map/if/ifLibLut.c @@ -369,6 +369,240 @@ void If_LibLutPrint( If_LibLut_t * pLutLib ) Abc_Print( 1, "%d %7.2f %7.2f\n", i, pLutLib->pLutAreas[i], pLutLib->pLutDelays[i][0] ); } +/**Function************************************************************* + + Synopsis [Allocates the cell library structure.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +If_LibCell_t * If_LibCellAlloc( void ) +{ + If_LibCell_t * p; + p = ABC_ALLOC( If_LibCell_t, 1 ); + memset( p, 0, sizeof(If_LibCell_t) ); + return p; +} + +/**Function************************************************************* + + Synopsis [Reads the description of cells from the cell library file.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +If_LibCell_t * If_LibCellRead( char * FileName ) +{ + char pBuffer[1000], * pToken; + If_LibCell_t * p; + FILE * pFile; + int i, k; + int CellId; + char * FuncDesc; + + pFile = fopen( FileName, "r" ); + if ( pFile == NULL ) + { + Abc_Print( -1, "Cannot open cell library file \"%s\".\n", FileName ); + return NULL; + } + + p = If_LibCellAlloc(); + p->pName = Abc_UtilStrsav( FileName ); + p->nCellNum = 0; + + // Read each line of the file + while ( fgets( pBuffer, 1000, pFile ) != NULL ) + { + pToken = strtok( pBuffer, " \t\n" ); + if ( pToken == NULL ) + continue; + if ( pToken[0] == '#' ) + continue; + + // Read CellId + CellId = atoi(pToken); + if ( CellId < 0 || CellId >= IF_MAX_LUTSIZE ) + { + Abc_Print( -1, "Cell ID %d is out of bounds (0-%d).\n", CellId, IF_MAX_LUTSIZE-1 ); + If_LibCellFree( p ); + fclose( pFile ); + return NULL; + } + + // Read FuncDesc + pToken = strtok( NULL, " \t\n" ); + if ( pToken == NULL ) + { + Abc_Print( -1, "Missing function description for cell %d.\n", CellId ); + If_LibCellFree( p ); + fclose( pFile ); + return NULL; + } + FuncDesc = Abc_UtilStrsav( pToken ); + p->pCellNames[CellId] = FuncDesc; + + // Determine number of inputs from function description + int nInputs = 0; + if ( FuncDesc[0] >= 'a' && FuncDesc[0] <= 'z' ) + { + // If it begins with a letter, that letter indicates the output + // and the number of inputs is that letter - 'a' + nInputs = FuncDesc[0] - 'a'; + } + else + { + // Otherwise, find the largest letter in the formula + char maxChar = 'a' - 1; + for ( i = 0; FuncDesc[i]; i++ ) + { + if ( FuncDesc[i] >= 'a' && FuncDesc[i] <= 'z' && FuncDesc[i] > maxChar ) + maxChar = FuncDesc[i]; + } + if ( maxChar >= 'a' ) + nInputs = maxChar - 'a' + 1; + } + p->nCellInputs[CellId] = nInputs; + + // Read Area + pToken = strtok( NULL, " \t\n" ); + if ( pToken == NULL ) + { + Abc_Print( -1, "Missing area for cell %d.\n", CellId ); + If_LibCellFree( p ); + fclose( pFile ); + return NULL; + } + p->pCellAreas[CellId] = (float)atof(pToken); + + // Read all available delays + k = 0; + while ( (pToken = strtok( NULL, " \t\n" )) != NULL && k < IF_MAX_LUTSIZE ) + { + p->pCellPinDelays[CellId][k] = atoi(pToken); + k++; + } + + // Check if number of delays matches number of inputs + if ( k != nInputs ) + { + Abc_Print( 0, "Warning: Cell %d has %d inputs but %d delays specified.\n", CellId, nInputs, k ); + } + + p->nCellNum++; + } + + fclose( pFile ); + + // Validate the library + for ( i = 0; i < IF_MAX_LUTSIZE; i++ ) + { + if ( p->pCellNames[i] == NULL ) + continue; + for ( k = 0; k < IF_MAX_LUTSIZE && p->pCellPinDelays[i][k] > 0; k++ ) + { + if ( p->pCellPinDelays[i][k] < 0 ) + { + Abc_Print( 0, "Pin %d of cell %d has delay %d. Pin delays should be non-negative. Technology mapping may not work correctly.\n", + k, i, p->pCellPinDelays[i][k] ); + } + } + } + + return p; +} + +/**Function************************************************************* + + Synopsis [Duplicates the cell library.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +If_LibCell_t * If_LibCellDup( If_LibCell_t * p ) +{ + If_LibCell_t * pNew; + int i; + pNew = ABC_ALLOC( If_LibCell_t, 1 ); + *pNew = *p; + pNew->pName = Abc_UtilStrsav( p->pName ); + for ( i = 0; i < IF_MAX_LUTSIZE; i++ ) + if ( p->pCellNames[i] ) + pNew->pCellNames[i] = Abc_UtilStrsav( p->pCellNames[i] ); + return pNew; +} + +/**Function************************************************************* + + Synopsis [Frees the cell library.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void If_LibCellFree( If_LibCell_t * pCellLib ) +{ + int i; + if ( pCellLib == NULL ) + return; + ABC_FREE( pCellLib->pName ); + for ( i = 0; i < IF_MAX_LUTSIZE; i++ ) + ABC_FREE( pCellLib->pCellNames[i] ); + ABC_FREE( pCellLib ); +} + +/**Function************************************************************* + + Synopsis [Prints the cell library.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void If_LibCellPrint( If_LibCell_t * pCellLib ) +{ + int i, k; + if ( pCellLib == NULL ) + { + Abc_Print( 1, "Cell library is not available.\n" ); + return; + } + Abc_Print( 1, "# Cell library: %s\n", pCellLib->pName ? pCellLib->pName : "Unknown" ); + Abc_Print( 1, "# Number of cells: %d\n", pCellLib->nCellNum ); + Abc_Print( 1, "# CellId Inputs Cell Description Area Delays\n" ); + + for ( i = 0; i < IF_MAX_LUTSIZE; i++ ) + { + if ( pCellLib->pCellNames[i] == NULL ) + continue; + + Abc_Print( 1, "%3d %6d %-32s %6.2f ", i, pCellLib->nCellInputs[i], pCellLib->pCellNames[i], pCellLib->pCellAreas[i] ); + + // Print all non-zero delays + for ( k = 0; k < IF_MAX_LUTSIZE && pCellLib->pCellPinDelays[i][k] > 0; k++ ) + Abc_Print( 1, " %4d", pCellLib->pCellPinDelays[i][k] ); + Abc_Print( 1, "\n" ); + } +} + /**Function************************************************************* Synopsis [Returns 1 if the delays are discrete.] From f808e2c68bd971737c21a8c254dd93410d1db21d Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Sat, 1 Nov 2025 10:47:00 -0700 Subject: [PATCH 11/17] Experiments with LUT mapping. --- src/aig/gia/giaAiger.c | 2 +- src/aig/gia/giaIf.c | 53 ++++++++++++++---------------------------- 2 files changed, 19 insertions(+), 36 deletions(-) diff --git a/src/aig/gia/giaAiger.c b/src/aig/gia/giaAiger.c index a51ddfa43..0b5e5a110 100644 --- a/src/aig/gia/giaAiger.c +++ b/src/aig/gia/giaAiger.c @@ -1549,7 +1549,7 @@ void Gia_AigerWriteS( Gia_Man_t * pInit, char * pFileName, int fWriteSymbols, in if ( p->vConfigs2 ) { int nTotalSize, nInstances = 0; - If_LibCell_t * pLibCell = NULL; // (If_LibCell_t *)Abc_FrameReadLibCell(); + If_LibCell_t * pLibCell = (If_LibCell_t *)Abc_FrameReadLibCell(); char *pCell0, *pCell1, *pCell2; // Get formulas from cell library or use defaults diff --git a/src/aig/gia/giaIf.c b/src/aig/gia/giaIf.c index c386dbcb9..0ffc015b2 100644 --- a/src/aig/gia/giaIf.c +++ b/src/aig/gia/giaIf.c @@ -1188,8 +1188,6 @@ int Gia_ManFromIfLogicCreateLutSpecial( Gia_Man_t * pNew, word * pRes, Vec_Int_t ***********************************************************************/ int Gia_ManFromIfLogicCreateLutSpecialJ( Gia_Man_t * pNew, word * pRes, Vec_Int_t * vLeaves, Vec_Int_t * vLeavesTemp, Vec_Int_t * vCover, Vec_Int_t * vMapping, Vec_Int_t * vMapping2, Vec_Int_t * vPacking ) { - return Gia_ManFromIfLogicCreateLut( pNew, pRes, vLeaves, vCover, vMapping, vMapping2 ); - word Truth; int i, iObjLit1, iObjLit2, iObjLit3; word z = If_CutPerformDeriveJ( NULL, (unsigned *)pRes, Vec_IntSize(vLeaves), Vec_IntSize(vLeaves), NULL, 1 ); @@ -1294,31 +1292,13 @@ int Gia_ManFromIfLogicCreateLutSpecialJ( Gia_Man_t * pNew, word * pRes, Vec_Int_ ***********************************************************************/ int Gia_ManFromIfLogicNode( void * pIfMan, Gia_Man_t * pNew, int iObj, Vec_Int_t * vLeaves, Vec_Int_t * vLeavesTemp, - word * pRes, char * pStr, Vec_Int_t * vCover, Vec_Int_t * vMapping, Vec_Int_t * vMapping2, Vec_Int_t * vPacking, int fCheck75, int fEnableCheck07 ) + word * pRes, char * pStr, Vec_Int_t * vCover, Vec_Int_t * vMapping, Vec_Int_t * vMapping2, Vec_Int_t * vPacking, int fCheck75 ) { int nLeaves = Vec_IntSize(vLeaves); int i, Length, nLutLeaf, nLutLeaf2, nLutRoot, iObjLit1, iObjLit2, iObjLit3; // workaround for the special case if ( fCheck75 ) pStr = "54"; - // perform special case matching for 44 - if ( fEnableCheck07 ) - { - if ( 0 && Vec_IntSize(vLeaves) <= 4 ) - { - // create mapping - iObjLit1 = Gia_ManFromIfLogicCreateLut( pNew, pRes, vLeaves, vCover, vMapping, vMapping2 ); - // write packing - if ( !Gia_ObjIsCi(Gia_ManObj(pNew, Abc_Lit2Var(iObjLit1))) && iObjLit1 > 1 ) - { - Vec_IntPush( vPacking, 1 ); - Vec_IntPush( vPacking, Abc_Lit2Var(iObjLit1) ); - Vec_IntAddToEntry( vPacking, 0, 1 ); - } - return iObjLit1; - } - return Gia_ManFromIfLogicCreateLutSpecialJ( pNew, pRes, vLeaves, vLeavesTemp, vCover, vMapping, vMapping2, vPacking ); - } if ( ((If_Man_t *)pIfMan)->pPars->fLut6Filter && Vec_IntSize(vLeaves) == 6 ) { extern word If_Dec6Perform( word t, int fDerive ); @@ -2034,13 +2014,13 @@ void Gia_ManConfigPrint( word Truth4, word z, int nLeaves ) SeeAlso [] ***********************************************************************/ -void Gia_ManFromIfGetConfig2( Vec_Str_t * vConfigs2, If_Man_t * pIfMan, If_Cut_t * pCutBest ) +void Gia_ManFromIfGetConfig2( Vec_Str_t * vConfigs2, If_Man_t * pIfMan, word * pTruth, int nLeaves ) { int i, CellId, nBytes; int startPos = Vec_StrSize(vConfigs2); // Determine cell type based on the number of leaves and configuration - if ( pCutBest->nLeaves <= 4 ) + if ( nLeaves <= 4 ) { // Cell type 0: Simple LUT4 CellId = 0; @@ -2048,7 +2028,7 @@ void Gia_ManFromIfGetConfig2( Vec_Str_t * vConfigs2, If_Man_t * pIfMan, If_Cut_t // Write CellId Vec_StrPush( vConfigs2, (char)CellId ); // Write truth table (16 bits for LUT4) - word Truth = *If_CutTruthW(pIfMan, pCutBest); + word Truth = pTruth[0]; Vec_StrPush( vConfigs2, (char)(Truth & 0xFF) ); Vec_StrPush( vConfigs2, (char)((Truth >> 8) & 0xFF) ); // Pad to 4-byte boundary @@ -2058,7 +2038,7 @@ void Gia_ManFromIfGetConfig2( Vec_Str_t * vConfigs2, If_Man_t * pIfMan, If_Cut_t } else { - word z = If_CutPerformDeriveJ( pIfMan, (unsigned *)If_CutTruthW(pIfMan, pCutBest), pCutBest->nLeaves, pCutBest->nLeaves, NULL, 1 ); + word z = If_CutPerformDeriveJ( pIfMan, (unsigned *)pTruth, nLeaves, nLeaves, NULL, 1 ); //Gia_ManConfigPrint( 0, z, pCutBest->nLeaves ); if ( ((z >> 63) & 1) == 0 ) { @@ -2070,7 +2050,7 @@ void Gia_ManFromIfGetConfig2( Vec_Str_t * vConfigs2, If_Man_t * pIfMan, If_Cut_t for ( i = 0; i < 4; i++ ) { int v = (int)((z >> (16 + (i << 2))) & 7); - if ( v == 6 && pCutBest->nLeaves == 5 ) + if ( v == 6 && nLeaves == 5 ) mappingBytes[i / 2] |= (0 << ((i % 2) * 4)); // constant 0 else mappingBytes[i / 2] |= ((v+2) << ((i % 2) * 4)); // leaf v (direct mapping) @@ -2082,7 +2062,7 @@ void Gia_ManFromIfGetConfig2( Vec_Str_t * vConfigs2, If_Man_t * pIfMan, If_Cut_t for ( i = 0; i < 4; i++ ) { int v = (int)((z >> (48 + (i << 2))) & 7); - if ( v == 6 && pCutBest->nLeaves == 5 ) + if ( v == 6 && nLeaves == 5 ) mappingBytes[i / 2] |= (0 << ((i % 2) * 4)); // constant 0 else if ( v == 7 ) mappingBytes[i / 2] |= ((7+2) << ((i % 2) * 4)); // output of first LUT at index N+2 where N=7 @@ -2351,7 +2331,7 @@ Gia_Man_t * Gia_ManFromIfLogic( If_Man_t * pIfMan ) // start mapping and packing vMapping = Vec_IntStart( If_ManObjNum(pIfMan) ); vMapping2 = Vec_IntStart( 1 ); - if ( pIfMan->pPars->fDeriveLuts && (pIfMan->pPars->pLutStruct || pIfMan->pPars->fEnableCheck75 || pIfMan->pPars->fEnableCheck75u || pIfMan->pPars->fEnableCheck07) ) + if ( pIfMan->pPars->fDeriveLuts && (pIfMan->pPars->pLutStruct || pIfMan->pPars->fEnableCheck75 || pIfMan->pPars->fEnableCheck75u) ) { vPacking = Vec_IntAlloc( 1000 ); Vec_IntPush( vPacking, 0 ); @@ -2452,15 +2432,20 @@ Gia_Man_t * Gia_ManFromIfLogic( If_Man_t * pIfMan ) if ( If_CutLeafBit(pCutBest, k) ) Abc_TtFlip( pTruth, Abc_TtWordNum(pCutBest->nLeaves), k ); // perform decomposition of the cut - pIfObj->iCopy = Gia_ManFromIfLogicNode( pIfMan, pNew, i, vLeaves, vLeaves2, pTruth, pIfMan->pPars->pLutStruct, vCover, vMapping, vMapping2, vPacking, (pIfMan->pPars->fEnableCheck75 || pIfMan->pPars->fEnableCheck75u), pIfMan->pPars->fEnableCheck07 ); + if ( pIfMan->pPars->fEnableCheck07 ) + pIfObj->iCopy = Gia_ManFromIfLogicCreateLut( pNew, pTruth, vLeaves, vCover, vMapping, vMapping2 ); + else + pIfObj->iCopy = Gia_ManFromIfLogicNode( pIfMan, pNew, i, vLeaves, vLeaves2, pTruth, pIfMan->pPars->pLutStruct, vCover, vMapping, vMapping2, vPacking, (pIfMan->pPars->fEnableCheck75 || pIfMan->pPars->fEnableCheck75u) ); pIfObj->iCopy = Abc_LitNotCond( pIfObj->iCopy, pCutBest->fCompl ); if ( vConfigs && Vec_IntSize(vLeaves) > 1 && !Gia_ObjIsCi(Gia_ManObj(pNew, Abc_Lit2Var(pIfObj->iCopy))) && pIfObj->iCopy > 1 ) Gia_ManFromIfGetConfig( vConfigs, pIfMan, pCutBest, pIfObj->iCopy, vConfigsStr ); else if ( vConfigs2 && Vec_IntSize(vLeaves) > 1 && !Gia_ObjIsCi(Gia_ManObj(pNew, Abc_Lit2Var(pIfObj->iCopy))) && pIfObj->iCopy > 1 ) { - assert( pCutBest->fCompl == 0 ); - //pCutBest->iCutFunc = Abc_LitNotCond( pCutBest->iCutFunc, Abc_LitIsCompl(pIfObj->iCopy) ); - Gia_ManFromIfGetConfig2( vConfigs2, pIfMan, pCutBest ); - //pCutBest->iCutFunc = Abc_LitNotCond( pCutBest->iCutFunc, Abc_LitIsCompl(pIfObj->iCopy) ); + If_CutForEachLeaf( pIfMan, pCutBest, pIfLeaf, k ) + if ( Abc_LitIsCompl(pIfLeaf->iCopy) ) + Abc_TtFlip( pTruth, Abc_TtWordNum(pCutBest->nLeaves), k ); + if ( Abc_LitIsCompl(pIfObj->iCopy) ^ pCutBest->fCompl ) + Abc_TtNot( pTruth, Abc_TtWordNum(pCutBest->nLeaves) ); + Gia_ManFromIfGetConfig2( vConfigs2, pIfMan, pTruth, pCutBest->nLeaves ); } } else @@ -2474,8 +2459,6 @@ Gia_Man_t * Gia_ManFromIfLogic( If_Man_t * pIfMan ) Vec_IntForEachEntry( vLeaves, Entry, k ) Vec_IntPush( vMapping2, Abc_Lit2Var(Entry) ); Vec_IntPush( vMapping2, Abc_Lit2Var(pIfObj->iCopy) ); - //if ( pIfMan->pPars->fEnableCheck07 && vConfigs2 && Vec_IntSize(vLeaves) > 1 ) - // Gia_ManFromIfGetConfig2( vConfigs2, pIfMan, pCutBest ); } } else if ( If_ObjIsCi(pIfObj) ) From aac61902081c12d91969197defce2c1bdc21f212 Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Sat, 1 Nov 2025 11:07:30 -0700 Subject: [PATCH 12/17] Extending support of CI/CO timing info. --- src/aig/gia/giaAiger.c | 6 ++++++ src/misc/tim/timMan.c | 28 ++++++++++++++++++++-------- 2 files changed, 26 insertions(+), 8 deletions(-) diff --git a/src/aig/gia/giaAiger.c b/src/aig/gia/giaAiger.c index 0b5e5a110..3c44a566d 100644 --- a/src/aig/gia/giaAiger.c +++ b/src/aig/gia/giaAiger.c @@ -652,6 +652,9 @@ Gia_Man_t * Gia_AigerReadFromMemory( char * pContents, int nFileSize, int fGiaSi pNew->vInArrs = Vec_FltStart( nInputs ); memcpy( Vec_FltArray(pNew->vInArrs), pCur, (size_t)4*nInputs ); pCur += 4*nInputs; if ( fVerbose ) printf( "Finished reading extension \"i\".\n" ); + if ( Vec_FltSize(pNew->vInArrs) == Gia_ManPiNum(pNew) ) + Vec_FltFillExtra(pNew->vInArrs, Gia_ManCiNum(pNew), 0); + assert( Vec_FltSize(pNew->vInArrs) == Gia_ManCiNum(pNew) ); } else if ( *pCur == 'o' ) { @@ -660,6 +663,9 @@ Gia_Man_t * Gia_AigerReadFromMemory( char * pContents, int nFileSize, int fGiaSi pNew->vOutReqs = Vec_FltStart( nOutputs ); memcpy( Vec_FltArray(pNew->vOutReqs), pCur, (size_t)4*nOutputs ); pCur += 4*nOutputs; if ( fVerbose ) printf( "Finished reading extension \"o\".\n" ); + if ( Vec_FltSize(pNew->vOutReqs) == Gia_ManPoNum(pNew) ) + Vec_FltFillExtra(pNew->vOutReqs, Gia_ManCoNum(pNew), 0); + assert( Vec_FltSize(pNew->vOutReqs) == Gia_ManCoNum(pNew) ); } // read equivalence classes else if ( *pCur == 'e' ) diff --git a/src/misc/tim/timMan.c b/src/misc/tim/timMan.c index 7e112669e..9bcdaaae6 100644 --- a/src/misc/tim/timMan.c +++ b/src/misc/tim/timMan.c @@ -451,19 +451,31 @@ void Tim_ManCreate( Tim_Man_t * p, void * pLib, Vec_Flt_t * vInArrs, Vec_Flt_t * // create arrival times if ( vInArrs ) { - assert( Vec_FltSize(vInArrs) == Tim_ManPiNum(p) ); - Tim_ManForEachPi( p, pObj, i ) - pObj->timeArr = Vec_FltEntry(vInArrs, i); - + if ( Vec_FltSize(vInArrs) == Tim_ManPiNum(p) ) { + Tim_ManForEachPi( p, pObj, i ) + pObj->timeArr = Vec_FltEntry(vInArrs, i); + } + else if ( Vec_FltSize(vInArrs) == Tim_ManCiNum(p) ) { + Tim_ManForEachCi( p, pObj, i ) + pObj->timeArr = Vec_FltEntry(vInArrs, i); + } + else assert( 0 ); } // create required times if ( vOutReqs ) { k = 0; - assert( Vec_FltSize(vOutReqs) == Tim_ManPoNum(p) ); - Tim_ManForEachPo( p, pObj, i ) - pObj->timeReq = Vec_FltEntry(vOutReqs, k++); - assert( k == Tim_ManPoNum(p) ); + if ( Vec_FltSize(vOutReqs) == Tim_ManPoNum(p) ) { + Tim_ManForEachPo( p, pObj, i ) + pObj->timeReq = Vec_FltEntry(vOutReqs, k++); + assert( k == Tim_ManPoNum(p) ); + } + else if ( Vec_FltSize(vOutReqs) == Tim_ManCoNum(p) ) { + Tim_ManForEachCo( p, pObj, i ) + pObj->timeReq = Vec_FltEntry(vOutReqs, k++); + assert( k == Tim_ManCoNum(p) ); + } + else assert( 0 ); } } From 5273eab9f72fa0beff90e2c5f1819e0587a50f1a Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Sat, 1 Nov 2025 11:14:37 -0700 Subject: [PATCH 13/17] Fixing compilation problem. --- src/map/mpm/mpmAbc.c | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/map/mpm/mpmAbc.c b/src/map/mpm/mpmAbc.c index ba16b20f0..8fac69f0c 100644 --- a/src/map/mpm/mpmAbc.c +++ b/src/map/mpm/mpmAbc.c @@ -249,14 +249,14 @@ void * Mpm_ManFromIfLogic( Mpm_Man_t * pMan ) if ( pMan->pPars->fDeriveLuts && (pMan->pPars->fUseTruth || pMan->pPars->fUseDsd) ) { extern int Gia_ManFromIfLogicNode( void * p, Gia_Man_t * pNew, int iObj, Vec_Int_t * vLeaves, Vec_Int_t * vLeavesTemp, - word * pRes, char * pStr, Vec_Int_t * vCover, Vec_Int_t * vMapping, Vec_Int_t * vMapping2, Vec_Int_t * vPacking, int fCheck75, int fCheck44e ); + word * pRes, char * pStr, Vec_Int_t * vCover, Vec_Int_t * vMapping, Vec_Int_t * vMapping2, Vec_Int_t * vPacking, int fCheck75 ); if ( pMan->pPars->fUseTruth ) pTruth = Mpm_CutTruth(pMan, Abc_Lit2Var(pCutBest->iFunc)); else uTruth = Mpm_CutTruthFromDsd( pMan, pCutBest, Abc_Lit2Var(pCutBest->iFunc) ); // Kit_DsdPrintFromTruth( pTruth, Vec_IntSize(vLeaves) ); printf( "\n" ); // perform decomposition of the cut - iLitNew = Gia_ManFromIfLogicNode( NULL, pNew, Mig_ObjId(pObj), vLeaves, vLeaves2, pTruth, NULL, vCover, vMapping, vMapping2, vPacking, 0, 0 ); + iLitNew = Gia_ManFromIfLogicNode( NULL, pNew, Mig_ObjId(pObj), vLeaves, vLeaves2, pTruth, NULL, vCover, vMapping, vMapping2, vPacking, 0 ); iLitNew = Abc_LitNotCond( iLitNew, pCutBest->fCompl ^ Abc_LitIsCompl(pCutBest->iFunc) ); } else From 800c274cc26664ba5419da8b35932c6e9df76ad0 Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Sat, 1 Nov 2025 22:55:14 -0700 Subject: [PATCH 14/17] Linear equetion solver. --- src/misc/util/module.make | 1 + src/misc/util/utilLinear.c | 814 +++++++++++++++++++++++++++++++++++++ 2 files changed, 815 insertions(+) create mode 100644 src/misc/util/utilLinear.c diff --git a/src/misc/util/module.make b/src/misc/util/module.make index 937c4a982..ef4baebf1 100644 --- a/src/misc/util/module.make +++ b/src/misc/util/module.make @@ -4,6 +4,7 @@ SRC += src/misc/util/utilBridge.c \ src/misc/util/utilColor.c \ src/misc/util/utilFile.c \ src/misc/util/utilIsop.c \ + src/misc/util/utilLinear.c \ src/misc/util/utilNam.c \ src/misc/util/utilPrefix.cpp \ src/misc/util/utilPth.c \ diff --git a/src/misc/util/utilLinear.c b/src/misc/util/utilLinear.c new file mode 100644 index 000000000..4a543c190 --- /dev/null +++ b/src/misc/util/utilLinear.c @@ -0,0 +1,814 @@ +/**CFile**************************************************************** + + FileName [utilLinear.c] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [Handling counter-examples.] + + Synopsis [Handling counter-examples.] + + Author [Alan Mishchenko] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - June 20, 2005.] + + Revision [$Id: utilColor.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $] + +***********************************************************************/ + +//#define _POSIX_C_SOURCE 200809L + +#include +#include +#include +#include +#include +#include + +#include "misc/util/abc_global.h" + +ABC_NAMESPACE_IMPL_START + +//////////////////////////////////////////////////////////////////////// +/// DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +#define EPSILON 1e-12 +#define VERIFY_TOLERANCE 1e-9 +#define INTEGER_TOLERANCE 1e-9 + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + +// Reads a full line from the file, allocating memory dynamically. +static char *read_line(FILE *fp) { + size_t capacity = 128; + size_t length = 0; + char *buffer = malloc(capacity); + if (!buffer) { + errno = ENOMEM; + return NULL; + } + + int ch; + while ((ch = fgetc(fp)) != EOF) { + if (ch == '\r') { + continue; + } + if (ch == '\n') { + break; + } + if (length + 1 >= capacity) { + size_t new_capacity = capacity * 2; + char *tmp = realloc(buffer, new_capacity); + if (!tmp) { + free(buffer); + errno = ENOMEM; + return NULL; + } + buffer = tmp; + capacity = new_capacity; + } + buffer[length++] = (char)ch; + } + + if (length == 0 && ch == EOF) { + free(buffer); + return NULL; + } + + buffer[length] = '\0'; + return buffer; +} + +// Loads the augmented matrix from a text file. +static int load_augmented_matrix(const char *path, double **outMatrix, int *outEqus, int *outVars) { + FILE *fp = fopen(path, "r"); + if (!fp) { + perror("fopen"); + return 0; + } + + double *data = NULL; + size_t capacity = 0; + size_t count = 0; + int row_width = -1; + int rows = 0; + + while (1) { + char *line = read_line(fp); + if (!line) { + if (feof(fp)) { + break; + } + fprintf(stderr, "Failed to read line from input file.\n"); + free(data); + fclose(fp); + return 0; + } + + char *ptr = line; + int columns = 0; + while (*ptr != '\0') { + char *end_ptr; + double value = strtod(ptr, &end_ptr); + if (end_ptr == ptr) { + if (*ptr == '\0') { + break; + } + ++ptr; + continue; + } + + if (count == capacity) { + size_t new_capacity = capacity == 0 ? 64 : capacity * 2; + double *tmp = realloc(data, new_capacity * sizeof(double)); + if (!tmp) { + fprintf(stderr, "Out of memory while loading matrix.\n"); + free(data); + free(line); + fclose(fp); + return 0; + } + data = tmp; + capacity = new_capacity; + } + + data[count++] = value; + ++columns; + ptr = end_ptr; + } + + free(line); + + if (columns == 0) { + continue; + } + + if (row_width == -1) { + row_width = columns; + } else if (columns != row_width) { + fprintf(stderr, "Row %d has %d entries, expected %d.\n", rows + 1, columns, row_width); + free(data); + fclose(fp); + return 0; + } + + ++rows; + } + + fclose(fp); + + if (rows == 0) { + fprintf(stderr, "Input file is empty or contains no data rows.\n"); + free(data); + return 0; + } + + if (row_width <= 1) { + fprintf(stderr, "Each row must contain at least two numbers.\n"); + free(data); + return 0; + } + + if ((size_t)rows * (size_t)row_width != count) { + fprintf(stderr, "Internal error: unexpected data size.\n"); + free(data); + return 0; + } + + *outMatrix = data; + *outEqus = rows; + *outVars = row_width - 1; + + return 1; +} + +// Swaps two rows in-place. +static void swap_rows(double *matrix, int cols, int row_a, int row_b) { + if (row_a == row_b) { + return; + } + for (int c = 0; c < cols; ++c) { + double tmp = matrix[row_a * cols + c]; + matrix[row_a * cols + c] = matrix[row_b * cols + c]; + matrix[row_b * cols + c] = tmp; + } +} + +// Clears values that are numerically close to zero. +static void prune_small_values(double *row, int count) { + for (int i = 0; i < count; ++i) { + if (fabs(row[i]) < EPSILON) { + row[i] = 0.0; + } + } +} + +// Computes a solution vector given assignments for the free variables. +static void compute_solution_from_free( + const double *rref, + int nVars, + const int *pivot_cols, + int rank, + const int *free_cols, + int free_count, + const double *free_values, + double *solution_out) { + int row_len = nVars + 1; + + for (int i = 0; i < nVars; ++i) { + solution_out[i] = 0.0; + } + + for (int i = 0; i < free_count; ++i) { + int col = free_cols[i]; + double value = free_values ? free_values[i] : 0.0; + solution_out[col] = value; + } + + for (int r = 0; r < rank; ++r) { + int pivot_col = pivot_cols[r]; + double value = rref[r * row_len + nVars]; + for (int j = 0; j < free_count; ++j) { + int free_col = free_cols[j]; + value -= rref[r * row_len + free_col] * solution_out[free_col]; + } + solution_out[pivot_col] = value; + } +} + +// Verifies that the solution satisfies the original system. +static int verify_solution( + const double *matrix, + int nEqus, + int nVars, + const double *solution, + double tolerance, + double *out_max_residual) { + int row_len = nVars + 1; + double max_residual = 0.0; + int ok = 1; + + for (int r = 0; r < nEqus; ++r) { + double lhs = 0.0; + for (int c = 0; c < nVars; ++c) { + lhs += (double)matrix[r * row_len + c] * (double)solution[c]; + } + double rhs = matrix[r * row_len + nVars]; + double residual = fabs(lhs - rhs); + if ((double)residual > max_residual) { + max_residual = (double)residual; + } + if ((double)residual > tolerance) { + ok = 0; + } + } + + if (out_max_residual) { + *out_max_residual = max_residual; + } + + return ok; +} + +// Checks whether a particular free-variable assignment yields an integer solution. +// Optionally enforces that the first two variables differ once rounded to integers. +static int assign_and_check_integer( + const double *rref, + int nVars, + const int *pivot_cols, + int rank, + const int *free_cols, + int free_count, + const double *free_values, + const double *original_matrix, + int nEqus, + double verify_tolerance, + double *workspace, + double *rounded, + double *out_solution, + int require_nonzero, + int require_distinct_first_two) { + compute_solution_from_free( + rref, + nVars, + pivot_cols, + rank, + free_cols, + free_count, + free_values, + workspace); + + for (int i = 0; i < nVars; ++i) { + double candidate = workspace[i]; + double nearest = round(candidate); + if (fabs(candidate - nearest) > INTEGER_TOLERANCE) { + return 0; + } + rounded[i] = nearest; + } + + int all_zero = 1; + int has_zero_component = 0; + int has_positive_component = 0; + int has_negative_component = 0; + for (int i = 0; i < nVars; ++i) { + if (rounded[i] != 0.0) { + all_zero = 0; + } else { + has_zero_component = 1; + } + if (rounded[i] > 0.0) { + has_positive_component = 1; + } else if (rounded[i] < 0.0) { + has_negative_component = 1; + } + } + if (require_nonzero) { + if (all_zero || has_negative_component || !has_positive_component || !has_zero_component) { + return 0; + } + } + + if (require_distinct_first_two && nVars >= 2) { + if (fabs(rounded[0] - rounded[1]) < INTEGER_TOLERANCE) { + return 0; + } + } + + if (verify_solution(original_matrix, nEqus, nVars, rounded, verify_tolerance, NULL)) { + memcpy(out_solution, rounded, (size_t)nVars * sizeof(double)); + return 1; + } + + return 0; +} + +// Recursively explores integer assignments for free variables while propagating optional constraints. +static int search_integer_solutions( + int depth, + int free_count, + double *free_values, + const int *candidates, + int candidate_count, + const double *rref, + int nEqus, + int nVars, + const int *pivot_cols, + int rank, + const int *free_cols, + const double *original_matrix, + double verify_tolerance, + double *workspace, + double *rounded, + double *out_solution, + int require_nonzero, + int require_distinct_first_two, + int *explored, + int exploration_limit) { + if (*explored >= exploration_limit) { + return 0; + } + + if (depth == free_count) { + (*explored)++; + return assign_and_check_integer( + rref, + nVars, + pivot_cols, + rank, + free_cols, + free_count, + free_values, + original_matrix, + nEqus, + verify_tolerance, + workspace, + rounded, + out_solution, + require_nonzero, + require_distinct_first_two); + } + + for (int i = 0; i < candidate_count; ++i) { + free_values[depth] = (double)candidates[i]; + if (search_integer_solutions( + depth + 1, + free_count, + free_values, + candidates, + candidate_count, + rref, + nEqus, + nVars, + pivot_cols, + rank, + free_cols, + original_matrix, + verify_tolerance, + workspace, + rounded, + out_solution, + require_nonzero, + require_distinct_first_two, + explored, + exploration_limit)) { + return 1; + } + } + + return 0; +} + +// Attempts to locate an integer solution when free variables are present. +// Searches a small integer lattice and enforces optional constraints such as distinct first variables. +static int try_integer_solution( + const double *rref, + int nEqus, + int nVars, + const int *pivot_cols, + int rank, + const int *free_cols, + int free_count, + const double *original_matrix, + double verify_tolerance, + double *workspace, + double *rounded, + double *out_solution, + int require_nonzero, + int require_distinct_first_two) { + if (free_count == 0) { + return 0; + } + + // Expand search radius to allow moderately sized integer assignments (up to |20|). + const int candidates[] = { + 0, + 1, -1, + 2, -2, + 3, -3, + 4, -4, + 5, -5, + 6, -6, + 7, -7, + 8, -8, + 9, -9, + 10, -10, + 11, -11, + 12, -12, + 13, -13, + 14, -14, + 15, -15, + 16, -16, + 17, -17, + 18, -18, + 19, -19, + 20, -20 + }; + const int candidate_count = (int)(sizeof(candidates) / sizeof(candidates[0])); + int exploration_limit = 200000; + int explored = 0; + + double *free_values = malloc((size_t)free_count * sizeof(double)); + if (!free_values) { + return 0; + } + for (int i = 0; i < free_count; ++i) { + free_values[i] = 0.0; + } + + if (assign_and_check_integer( + rref, + nVars, + pivot_cols, + rank, + free_cols, + free_count, + free_values, + original_matrix, + nEqus, + verify_tolerance, + workspace, + rounded, + out_solution, + require_nonzero, + require_distinct_first_two)) { + free(free_values); + return 1; + } + + int found = search_integer_solutions( + 0, + free_count, + free_values, + candidates, + candidate_count, + rref, + nEqus, + nVars, + pivot_cols, + rank, + free_cols, + original_matrix, + verify_tolerance, + workspace, + rounded, + out_solution, + require_nonzero, + require_distinct_first_two, + &explored, + exploration_limit); + + free(free_values); + return found; +} + +// Gaussian-elimination-based solver that optionally searches for integer solutions. +double *linear_equation_solver(double *pMatrix, int nEqus, int nVars) { + if (!pMatrix || nEqus <= 0 || nVars <= 0) { + fprintf(stderr, "Invalid matrix dimensions provided to solver.\n"); + return NULL; + } + + int row_len = nVars + 1; + size_t matrix_bytes = (size_t)nEqus * (size_t)row_len * sizeof(double); + + double *matrix_copy = NULL; + double *solution = NULL; + double *workspace = NULL; + double *rounded = NULL; + double *result = NULL; + int *pivot_cols = NULL; + int *pivot_column_used = NULL; + int *free_cols = NULL; + + matrix_copy = malloc(matrix_bytes); + if (!matrix_copy) { + fprintf(stderr, "Unable to allocate memory for solver workspace.\n"); + goto cleanup; + } + memcpy(matrix_copy, pMatrix, matrix_bytes); + + pivot_cols = malloc((size_t)nEqus * sizeof(int)); + if (!pivot_cols) { + fprintf(stderr, "Unable to allocate memory for pivot tracking.\n"); + goto cleanup; + } + for (int i = 0; i < nEqus; ++i) { + pivot_cols[i] = -1; + } + + int pivot_row_index = 0; + for (int col = 0; col < nVars && pivot_row_index < nEqus; ++col) { + int best_row = pivot_row_index; + double max_value = fabs(matrix_copy[best_row * row_len + col]); + for (int r = pivot_row_index + 1; r < nEqus; ++r) { + double value = fabs(matrix_copy[r * row_len + col]); + if (value > max_value) { + max_value = value; + best_row = r; + } + } + + if (max_value < EPSILON) { + continue; + } + + swap_rows(matrix_copy, row_len, pivot_row_index, best_row); + + double pivot_value = matrix_copy[pivot_row_index * row_len + col]; + for (int c = 0; c < row_len; ++c) { + matrix_copy[pivot_row_index * row_len + c] /= pivot_value; + } + matrix_copy[pivot_row_index * row_len + col] = 1.0; + prune_small_values(&matrix_copy[pivot_row_index * row_len], row_len); + + for (int r = 0; r < nEqus; ++r) { + if (r == pivot_row_index) { + continue; + } + double factor = matrix_copy[r * row_len + col]; + if (fabs(factor) < EPSILON) { + continue; + } + for (int c = 0; c < row_len; ++c) { + matrix_copy[r * row_len + c] -= factor * matrix_copy[pivot_row_index * row_len + c]; + } + matrix_copy[r * row_len + col] = 0.0; + prune_small_values(&matrix_copy[r * row_len], row_len); + } + + pivot_cols[pivot_row_index] = col; + ++pivot_row_index; + } + + int rank = pivot_row_index; + //printf("Rank: %d\n", rank); + + for (int r = 0; r < nEqus; ++r) { + int zero_row = 1; + for (int c = 0; c < nVars; ++c) { + if (fabs(matrix_copy[r * row_len + c]) > EPSILON) { + zero_row = 0; + break; + } + } + if (zero_row && fabs(matrix_copy[r * row_len + nVars]) > EPSILON) { + printf("Verification: inconsistent system detected.\n"); + goto cleanup; + } + } + + pivot_column_used = calloc((size_t)nVars, sizeof(int)); + if (!pivot_column_used) { + fprintf(stderr, "Unable to allocate memory for pivot metadata.\n"); + goto cleanup; + } + for (int r = 0; r < rank; ++r) { + int col = pivot_cols[r]; + if (col >= 0 && col < nVars) { + pivot_column_used[col] = 1; + } + } + + int free_count = 0; + for (int c = 0; c < nVars; ++c) { + if (!pivot_column_used[c]) { + ++free_count; + } + } + + if (free_count > 0) { + free_cols = malloc((size_t)free_count * sizeof(int)); + if (!free_cols) { + fprintf(stderr, "Unable to allocate memory for free column list.\n"); + goto cleanup; + } + int idx = 0; + for (int c = 0; c < nVars; ++c) { + if (!pivot_column_used[c]) { + free_cols[idx++] = c; + } + } + } + + int homogeneous_rhs = 1; + for (int r = 0; r < nEqus; ++r) { + if (fabs(pMatrix[r * row_len + nVars]) > EPSILON) { + homogeneous_rhs = 0; + break; + } + } + // Only demand integer solutions when the system is homogeneous with free variables. + int require_nonzero_integer = homogeneous_rhs && free_count > 0; + // Enforce distinct first two variables whenever multiple variables remain free. + int require_distinct_first_two = (free_count > 0 && nVars >= 2); + + solution = malloc((size_t)nVars * sizeof(double)); + workspace = malloc((size_t)nVars * sizeof(double)); + rounded = malloc((size_t)nVars * sizeof(double)); + if (!solution || !workspace || !rounded) { + fprintf(stderr, "Unable to allocate solver buffers.\n"); + goto cleanup; + } + + if (free_count == 0) { + compute_solution_from_free( + matrix_copy, + nVars, + pivot_cols, + rank, + free_cols, + free_count, + NULL, + solution); + } else { + if (free_count >= 6) { + printf("Warning: large nullspace (%d free variables); integer search radius +/-20 may be expensive.\n", free_count); + } + if (!try_integer_solution( + matrix_copy, + nEqus, + nVars, + pivot_cols, + rank, + free_cols, + free_count, + pMatrix, + VERIFY_TOLERANCE, + workspace, + rounded, + solution, + require_nonzero_integer, + require_distinct_first_two)) { + for (int i = 0; i < free_count; ++i) { + workspace[i] = 0.0; + } + compute_solution_from_free( + matrix_copy, + nVars, + pivot_cols, + rank, + free_cols, + free_count, + workspace, + solution); + if (require_nonzero_integer && require_distinct_first_two) { + printf("Note: integer solution meeting non-negative and distinct-first-two constraints not found; returning floating-point solution.\n"); + } else if (require_nonzero_integer) { + printf("Note: non-negative integer solution with mixed zero/positive entries not found; returning floating-point solution.\n"); + } else if (require_distinct_first_two) { + printf("Note: integer solution with distinct first two variables not found; returning floating-point solution.\n"); + } else { + printf("Note: integer solution not found; returning floating-point solution.\n"); + } + } + } + + double max_residual = 0.0; + if (!verify_solution(pMatrix, nEqus, nVars, solution, VERIFY_TOLERANCE, &max_residual)) { + printf("Verification: failure (max residual = %.6f)\n", max_residual); + goto cleanup; + } + //printf("Verification: success (max residual = %.6f)\n", max_residual); + + result = solution; + solution = NULL; + +cleanup: + free(matrix_copy); + free(pivot_cols); + free(pivot_column_used); + free(free_cols); + free(workspace); + free(rounded); + free(solution); + return result; +} + +/* + +int main(int argc, char **argv) { + if (argc != 2) { + fprintf(stderr, "Usage: %s \n", argv[0]); + return EXIT_FAILURE; + } + + double *matrix = NULL; + int nEqus = 0; + int nVars = 0; + + if (!load_augmented_matrix(argv[1], &matrix, &nEqus, &nVars)) { + return EXIT_FAILURE; + } + + printf("Equations: %d, Variables: %d\n", nEqus, nVars); + + struct timespec start_time; + struct timespec end_time; + if (clock_gettime(CLOCK_MONOTONIC, &start_time) != 0) { + perror("clock_gettime"); + free(matrix); + return EXIT_FAILURE; + } + + double *solution = linear_equation_solver(matrix, nEqus, nVars); + + if (clock_gettime(CLOCK_MONOTONIC, &end_time) != 0) { + perror("clock_gettime"); + free(matrix); + free(solution); + return EXIT_FAILURE; + } + + if (!solution) { + free(matrix); + return EXIT_FAILURE; + } + + double elapsed = (double)(end_time.tv_sec - start_time.tv_sec); + elapsed += (double)(end_time.tv_nsec - start_time.tv_nsec) / 1e9; + printf("Solve time: %.6f seconds\n", elapsed); + + for (int i = 0; i < nVars; ++i) { + printf("x%d = %.6f\n", i, solution[i]); + } + + free(matrix); + free(solution); + + return EXIT_SUCCESS; +} +*/ + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + + +ABC_NAMESPACE_IMPL_END + From f897673f68184e3564ef3991b2937cc6eb3f8326 Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Sat, 1 Nov 2025 23:33:25 -0700 Subject: [PATCH 15/17] Fixing compilier issues. --- src/misc/util/utilLinear.c | 43 ++++++++++++++++++++++---------------- 1 file changed, 25 insertions(+), 18 deletions(-) diff --git a/src/misc/util/utilLinear.c b/src/misc/util/utilLinear.c index 4a543c190..b0f03d4a8 100644 --- a/src/misc/util/utilLinear.c +++ b/src/misc/util/utilLinear.c @@ -47,7 +47,7 @@ ABC_NAMESPACE_IMPL_START static char *read_line(FILE *fp) { size_t capacity = 128; size_t length = 0; - char *buffer = malloc(capacity); + char *buffer = (char *)malloc(capacity); if (!buffer) { errno = ENOMEM; return NULL; @@ -63,7 +63,7 @@ static char *read_line(FILE *fp) { } if (length + 1 >= capacity) { size_t new_capacity = capacity * 2; - char *tmp = realloc(buffer, new_capacity); + char *tmp = (char *)realloc(buffer, new_capacity); if (!tmp) { free(buffer); errno = ENOMEM; @@ -125,7 +125,7 @@ static int load_augmented_matrix(const char *path, double **outMatrix, int *outE if (count == capacity) { size_t new_capacity = capacity == 0 ? 64 : capacity * 2; - double *tmp = realloc(data, new_capacity * sizeof(double)); + double *tmp = (double *)realloc(data, new_capacity * sizeof(double)); if (!tmp) { fprintf(stderr, "Out of memory while loading matrix.\n"); free(data); @@ -473,7 +473,7 @@ static int try_integer_solution( int exploration_limit = 200000; int explored = 0; - double *free_values = malloc((size_t)free_count * sizeof(double)); + double *free_values = (double *)malloc((size_t)free_count * sizeof(double)); if (!free_values) { return 0; } @@ -545,15 +545,22 @@ double *linear_equation_solver(double *pMatrix, int nEqus, int nVars) { int *pivot_cols = NULL; int *pivot_column_used = NULL; int *free_cols = NULL; + int free_count = 0; + int homogeneous_rhs = 0; + int require_nonzero_integer = 0; + int require_distinct_first_two = 0; + int pivot_row_index = 0; + int rank = 0; + double max_residual = 0.0; - matrix_copy = malloc(matrix_bytes); + matrix_copy = (double *)malloc(matrix_bytes); if (!matrix_copy) { fprintf(stderr, "Unable to allocate memory for solver workspace.\n"); goto cleanup; } memcpy(matrix_copy, pMatrix, matrix_bytes); - pivot_cols = malloc((size_t)nEqus * sizeof(int)); + pivot_cols = (int *)malloc((size_t)nEqus * sizeof(int)); if (!pivot_cols) { fprintf(stderr, "Unable to allocate memory for pivot tracking.\n"); goto cleanup; @@ -562,7 +569,7 @@ double *linear_equation_solver(double *pMatrix, int nEqus, int nVars) { pivot_cols[i] = -1; } - int pivot_row_index = 0; + pivot_row_index = 0; for (int col = 0; col < nVars && pivot_row_index < nEqus; ++col) { int best_row = pivot_row_index; double max_value = fabs(matrix_copy[best_row * row_len + col]); @@ -606,7 +613,7 @@ double *linear_equation_solver(double *pMatrix, int nEqus, int nVars) { ++pivot_row_index; } - int rank = pivot_row_index; + rank = pivot_row_index; //printf("Rank: %d\n", rank); for (int r = 0; r < nEqus; ++r) { @@ -623,7 +630,7 @@ double *linear_equation_solver(double *pMatrix, int nEqus, int nVars) { } } - pivot_column_used = calloc((size_t)nVars, sizeof(int)); + pivot_column_used = (int *)calloc((size_t)nVars, sizeof(int)); if (!pivot_column_used) { fprintf(stderr, "Unable to allocate memory for pivot metadata.\n"); goto cleanup; @@ -635,7 +642,7 @@ double *linear_equation_solver(double *pMatrix, int nEqus, int nVars) { } } - int free_count = 0; + free_count = 0; for (int c = 0; c < nVars; ++c) { if (!pivot_column_used[c]) { ++free_count; @@ -643,7 +650,7 @@ double *linear_equation_solver(double *pMatrix, int nEqus, int nVars) { } if (free_count > 0) { - free_cols = malloc((size_t)free_count * sizeof(int)); + free_cols = (int *)malloc((size_t)free_count * sizeof(int)); if (!free_cols) { fprintf(stderr, "Unable to allocate memory for free column list.\n"); goto cleanup; @@ -656,7 +663,7 @@ double *linear_equation_solver(double *pMatrix, int nEqus, int nVars) { } } - int homogeneous_rhs = 1; + homogeneous_rhs = 1; for (int r = 0; r < nEqus; ++r) { if (fabs(pMatrix[r * row_len + nVars]) > EPSILON) { homogeneous_rhs = 0; @@ -664,13 +671,13 @@ double *linear_equation_solver(double *pMatrix, int nEqus, int nVars) { } } // Only demand integer solutions when the system is homogeneous with free variables. - int require_nonzero_integer = homogeneous_rhs && free_count > 0; + require_nonzero_integer = homogeneous_rhs && free_count > 0; // Enforce distinct first two variables whenever multiple variables remain free. - int require_distinct_first_two = (free_count > 0 && nVars >= 2); + require_distinct_first_two = (free_count > 0 && nVars >= 2); - solution = malloc((size_t)nVars * sizeof(double)); - workspace = malloc((size_t)nVars * sizeof(double)); - rounded = malloc((size_t)nVars * sizeof(double)); + solution = (double *)malloc((size_t)nVars * sizeof(double)); + workspace = (double *)malloc((size_t)nVars * sizeof(double)); + rounded = (double *)malloc((size_t)nVars * sizeof(double)); if (!solution || !workspace || !rounded) { fprintf(stderr, "Unable to allocate solver buffers.\n"); goto cleanup; @@ -729,7 +736,7 @@ double *linear_equation_solver(double *pMatrix, int nEqus, int nVars) { } } - double max_residual = 0.0; + max_residual = 0.0; if (!verify_solution(pMatrix, nEqus, nVars, solution, VERIFY_TOLERANCE, &max_residual)) { printf("Verification: failure (max residual = %.6f)\n", max_residual); goto cleanup; From 8f06ce91124bf9488c80a39a4d9a4bd3c4889c73 Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Sun, 2 Nov 2025 19:08:59 -0800 Subject: [PATCH 16/17] Enabling runtime limit in "lutexact". --- src/sat/bmc/bmcMaj2.c | 8 ++++++++ 1 file changed, 8 insertions(+) diff --git a/src/sat/bmc/bmcMaj2.c b/src/sat/bmc/bmcMaj2.c index c9403e037..ffc6946ae 100644 --- a/src/sat/bmc/bmcMaj2.c +++ b/src/sat/bmc/bmcMaj2.c @@ -1411,6 +1411,8 @@ void Exa3_ManExactSynthesis2( Bmc_EsPar_t * pPars ) status = Exa3_ManAddCnfStart( p, pPars->fOnlyAnd ); assert( status ); printf( "Running exact synthesis for %d-input function with %d %d-input LUTs...\n", p->nVars, p->nNodes, p->nLutSize ); + abctime nTimeToStop = pPars->RuntimeLim ? pPars->RuntimeLim * CLOCKS_PER_SEC + Abc_Clock(): 0; + sat_solver_set_runtime_limit( p->pSat, nTimeToStop ); for ( i = 0; iMint != -1; i++ ) { abctime clk = Abc_Clock(); @@ -1426,6 +1428,12 @@ void Exa3_ManExactSynthesis2( Bmc_EsPar_t * pPars ) printf( "Conf =%9d ", sat_solver_nconflicts(p->pSat) ); Abc_PrintTime( 1, "Time", Abc_Clock() - clk ); } + if ( nTimeToStop && Abc_Clock() > nTimeToStop ) + { + printf( "Runtime limit (%d sec) is reached. ", pPars->RuntimeLim ); + status = l_Undef; + break; + } if ( status == l_False ) { printf( "The problem has no solution.\n" ); From f8981d48f512c6900e2ac9b1095b2e406f8f5731 Mon Sep 17 00:00:00 2001 From: Baruch Sterin Date: Tue, 4 Nov 2025 02:52:02 +0200 Subject: [PATCH 17/17] Reduce the amount of text printed when building `abc`. * introduce a user-defined function `abc_info` that only prints out text when ABC_MAKE_VERBOSE is set * replace all calls to $(info ...) with calls to $(call abc_info, ...) To show the output build with ABC_MAKE_VERBOSE. for example ``` make ABC_MAKE_VERBOSE=1 ... ``` --- Makefile | 46 ++++++++++++++++++++++++---------------------- 1 file changed, 24 insertions(+), 22 deletions(-) diff --git a/Makefile b/Makefile index 2dfc1c691..3e4d02719 100644 --- a/Makefile +++ b/Makefile @@ -8,10 +8,19 @@ MSG_PREFIX ?= ABCSRC ?= . VPATH = $(ABCSRC) -$(info $(MSG_PREFIX)Using CC=$(CC)) -$(info $(MSG_PREFIX)Using CXX=$(CXX)) -$(info $(MSG_PREFIX)Using AR=$(AR)) -$(info $(MSG_PREFIX)Using LD=$(LD)) +# whether to print build options, tools, and echo commands while building +ifdef ABC_MAKE_VERBOSE + VERBOSE= + abc_info = $(info $(1)) +else + VERBOSE=@ + abc_info = +endif + +$(call abc_info,$(MSG_PREFIX)Using CC=$(CC)) +$(call abc_info,$(MSG_PREFIX)Using CXX=$(CXX)) +$(call abc_info,$(MSG_PREFIX)Using AR=$(AR)) +$(call abc_info,$(MSG_PREFIX)Using LD=$(LD)) PROG := abc OS := $(shell uname -s) @@ -66,14 +75,14 @@ endif ifdef ABC_USE_NAMESPACE CFLAGS += -DABC_NAMESPACE=$(ABC_USE_NAMESPACE) -fpermissive -x c++ CC := $(CXX) - $(info $(MSG_PREFIX)Compiling in namespace $(ABC_USE_NAMESPACE)) + $(call abc_info,$(MSG_PREFIX)Compiling in namespace $(ABC_USE_NAMESPACE)) endif # compile CUDD with ABC ifndef ABC_USE_NO_CUDD CFLAGS += -DABC_USE_CUDD=1 MODULES += src/bdd/cudd src/bdd/extrab src/bdd/dsd src/bdd/epd src/bdd/mtr src/bdd/reo src/bdd/cas src/bdd/bbr src/bdd/llb - $(info $(MSG_PREFIX)Compiling with CUDD) + $(call abc_info,$(MSG_PREFIX)Compiling with CUDD) endif ABC_READLINE_INCLUDES ?= @@ -87,28 +96,21 @@ ifndef ABC_USE_NO_READLINE CFLAGS += -I/usr/local/include LDFLAGS += -L/usr/local/lib endif - $(info $(MSG_PREFIX)Using libreadline) + $(call abc_info,$(MSG_PREFIX)Using libreadline) endif # whether to compile with thread support ifndef ABC_USE_NO_PTHREADS CFLAGS += -DABC_USE_PTHREADS LIBS += -lpthread - $(info $(MSG_PREFIX)Using pthreads) + $(call abc_info,$(MSG_PREFIX)Using pthreads) endif # whether to compile into position independent code ifdef ABC_USE_PIC CFLAGS += -fPIC LIBS += -fPIC - $(info $(MSG_PREFIX)Compiling position independent code) -endif - -# whether to echo commands while building -ifdef ABC_MAKE_VERBOSE - VERBOSE= -else - VERBOSE=@ + $(call abc_info,$(MSG_PREFIX)Compiling position independent code) endif # Set -Wno-unused-bug-set-variable for GCC 4.6.0 and greater only @@ -120,16 +122,16 @@ GCC_VERSION=$(shell $(CC) -dumpversion) GCC_MAJOR=$(word 1,$(subst .,$(space),$(GCC_VERSION))) GCC_MINOR=$(word 2,$(subst .,$(space),$(GCC_VERSION))) -$(info $(MSG_PREFIX)Found GCC_VERSION $(GCC_VERSION)) +$(call abc_info,$(MSG_PREFIX)Found GCC_VERSION $(GCC_VERSION)) ifeq ($(findstring $(GCC_MAJOR),0 1 2 3),) ifeq ($(GCC_MAJOR),4) -$(info $(MSG_PREFIX)Found GCC_MAJOR==4) +$(call abc_info,$(MSG_PREFIX)Found GCC_MAJOR==4) ifeq ($(findstring $(GCC_MINOR),0 1 2 3 4 5),) -$(info $(MSG_PREFIX)Found GCC_MINOR>=6) +$(call abc_info,$(MSG_PREFIX)Found GCC_MINOR>=6) CFLAGS += -Wno-unused-but-set-variable endif else -$(info $(MSG_PREFIX)Found GCC_MAJOR>=5) +$(call abc_info,$(MSG_PREFIX)Found GCC_MAJOR>=5) CFLAGS += -Wno-unused-but-set-variable endif endif @@ -148,10 +150,10 @@ endif ifdef ABC_USE_LIBSTDCXX LIBS += -lstdc++ - $(info $(MSG_PREFIX)Using explicit -lstdc++) + $(call abc_info,$(MSG_PREFIX)Using explicit -lstdc++) endif -$(info $(MSG_PREFIX)Using CFLAGS=$(CFLAGS)) +$(call abc_info,$(MSG_PREFIX)Using CFLAGS=$(CFLAGS)) CXXFLAGS += $(CFLAGS) -std=c++17 -fno-exceptions SRC :=