From 96b9ef2ce5347f380c1a07e1de1887a177f7e37e Mon Sep 17 00:00:00 2001 From: Yukio Miyasaka Date: Sat, 17 Sep 2022 15:42:36 -0700 Subject: import ttopt --- src/aig/gia/giaTtopt.cpp | 1207 ++++++++++++++++++++++++++++++++++++++++++++++ src/aig/gia/module.make | 1 + src/base/abci/abc.c | 109 +++++ 3 files changed, 1317 insertions(+) create mode 100644 src/aig/gia/giaTtopt.cpp diff --git a/src/aig/gia/giaTtopt.cpp b/src/aig/gia/giaTtopt.cpp new file mode 100644 index 00000000..eca0989d --- /dev/null +++ b/src/aig/gia/giaTtopt.cpp @@ -0,0 +1,1207 @@ +// Author : Yukio Miyasaka +#include +#include +#include +#include +#include +#include +#include +#include +#include +#include +#include +#include + +#include "gia.h" + +ABC_NAMESPACE_IMPL_START + +namespace Ttopt { + +struct PairHasher { + std::size_t operator()(const std::pair & k) const { + std::hash hasher; + std::size_t seed = hasher(k.first) + 0x9e3779b9; + seed = hasher(k.second) + 0x9e3779b9 + (seed << 6) + (seed >> 2); + return seed; + } +}; + +class TruthTable { +public: + const int ww = 64; // word width + const int lww = 6; // log word width + typedef std::bitset<64> bsw; + + int nInputs; + int nSize; + int nTotalSize; + int nOutputs; + std::vector t; + + std::vector > vvIndices; + std::vector > vvRedundantIndices; + std::vector vLevels; + + std::vector > savedt; + std::vector > > vvIndicesSaved; + std::vector > > vvRedundantIndicesSaved; + std::vector > vLevelsSaved; + + std::mt19937 rng; + static const word ones[]; + static const word swapmask[]; + + TruthTable(int nInputs, int nOutputs): nInputs(nInputs), nOutputs(nOutputs) { + if(nInputs >= lww) { + nSize = 1 << (nInputs - lww); + nTotalSize = nSize * nOutputs; + t.resize(nTotalSize); + } else { + nSize = 0; + nTotalSize = ((1 << nInputs) * nOutputs + ww - 1) / ww; + t.resize(nTotalSize); + } + vLevels.resize(nInputs); + std::iota(vLevels.begin(), vLevels.end(), 0); + } + + std::string BinaryToString(int bin, int size) { + std::string str; + for(int i = 0; i < size; i++) { + str += (bin & 1) + '0'; + bin = bin >> 1; + } + return str; + } + void GeneratePla(std::string filename) { + std::ofstream f(filename); + f << ".i " << nInputs << std::endl; + f << ".o " << nOutputs << std::endl; + if(nSize) { + for(int index = 0; index < nSize; index++) { + for(int pos = 0; pos < ww; pos++) { + int pat = (index << lww) + pos; + f << BinaryToString(pat, nInputs) << " "; + for(int i = 0; i < nOutputs; i++) { + f << ((t[nSize * i + index] >> pos) & 1); + } + f << std::endl; + } + } + } else { + for(int pos = 0; pos < (1 << nInputs); pos++) { + f << BinaryToString(pos, nInputs) << " "; + for(int i = 0; i < nOutputs; i++) { + int padding = i * (1 << nInputs); + f << ((t[padding / ww] >> (pos + padding % ww)) & 1); + } + f << std::endl; + } + } + } + + virtual void Save(uint i) { + if(savedt.size() < i + 1) { + savedt.resize(i + 1); + vLevelsSaved.resize(i + 1); + } + savedt[i] = t; + vLevelsSaved[i] = vLevels; + } + + virtual void Load(uint i) { + assert(i < savedt.size()); + t = savedt[i]; + vLevels = vLevelsSaved[i]; + } + + virtual void SaveIndices(uint i) { + if(vvIndicesSaved.size() < i + 1) { + vvIndicesSaved.resize(i + 1); + vvRedundantIndicesSaved.resize(i + 1); + } + vvIndicesSaved[i] = vvIndices; + vvRedundantIndicesSaved[i] = vvRedundantIndices; + } + + virtual void LoadIndices(uint i) { + vvIndices = vvIndicesSaved[i]; + vvRedundantIndices = vvRedundantIndicesSaved[i]; + } + + word GetValue(int index_lev, int lev) { + assert(index_lev >= 0); + assert(nInputs - lev <= lww); + int logwidth = nInputs - lev; + int index = index_lev >> (lww - logwidth); + int pos = (index_lev % (1 << (lww - logwidth))) << logwidth; + return (t[index] >> pos) & ones[logwidth]; + } + + int IsEq(int index1, int index2, int lev, bool fCompl = false) { + assert(index1 >= 0); + assert(index2 >= 0); + int logwidth = nInputs - lev; + bool fEq = true; + if(logwidth > lww) { + int nScopeSize = 1 << (logwidth - lww); + for(int i = 0; i < nScopeSize && (fEq || fCompl); i++) { + fEq &= t[nScopeSize * index1 + i] == t[nScopeSize * index2 + i]; + fCompl &= t[nScopeSize * index1 + i] == ~t[nScopeSize * index2 + i]; + } + } else { + word value = GetValue(index1, lev) ^ GetValue(index2, lev); + fEq &= !value; + fCompl &= !(value ^ ones[logwidth]); + } + return 2 * fCompl + fEq; + } + + bool Imply(int index1, int index2, int lev) { + assert(index1 >= 0); + assert(index2 >= 0); + int logwidth = nInputs - lev; + if(logwidth > lww) { + int nScopeSize = 1 << (logwidth - lww); + for(int i = 0; i < nScopeSize; i++) { + if(t[nScopeSize * index1 + i] & ~t[nScopeSize * index2 + i]) { + return false; + } + } + return true; + } + return !(GetValue(index1, lev) & (GetValue(index2, lev) ^ ones[logwidth])); + } + + int BDDNodeCountLevel(int lev) { + return vvIndices[lev].size() - vvRedundantIndices[lev].size(); + } + + int BDDNodeCount() { + int count = 1; // const node + for(int i = 0; i < nInputs; i++) { + count += BDDNodeCountLevel(i); + } + return count; + } + + int BDDFind(int index, int lev) { + int logwidth = nInputs - lev; + if(logwidth > lww) { + int nScopeSize = 1 << (logwidth - lww); + bool fZero = true; + bool fOne = true; + for(int i = 0; i < nScopeSize && (fZero || fOne); i++) { + word value = t[nScopeSize * index + i]; + fZero &= !value; + fOne &= !(~value); + } + if(fZero || fOne) { + return -2 ^ fOne; + } + for(uint j = 0; j < vvIndices[lev].size(); j++) { + int index2 = vvIndices[lev][j]; + bool fEq = true; + bool fCompl = true; + for(int i = 0; i < nScopeSize && (fEq || fCompl); i++) { + fEq &= t[nScopeSize * index + i] == t[nScopeSize * index2 + i]; + fCompl &= t[nScopeSize * index + i] == ~t[nScopeSize * index2 + i]; + } + if(fEq || fCompl) { + return (j << 1) ^ fCompl; + } + } + } else { + word value = GetValue(index, lev); + if(!value) { + return -2; + } + if(!(value ^ ones[logwidth])) { + return -1; + } + for(uint j = 0; j < vvIndices[lev].size(); j++) { + int index2 = vvIndices[lev][j]; + word value2 = value ^ GetValue(index2, lev); + if(!(value2)) { + return j << 1; + } + if(!(value2 ^ ones[logwidth])) { + return (j << 1) ^ 1; + } + } + } + return -3; + } + + virtual int BDDBuildOne(int index, int lev) { + int r = BDDFind(index, lev); + if(r >= -2) { + return r; + } + vvIndices[lev].push_back(index); + return (vvIndices[lev].size() - 1) << 1; + } + + virtual void BDDBuildStartup() { + vvIndices.clear(); + vvIndices.resize(nInputs); + vvRedundantIndices.clear(); + vvRedundantIndices.resize(nInputs); + for(int i = 0; i < nOutputs; i++) { + BDDBuildOne(i, 0); + } + } + + virtual void BDDBuildLevel(int lev) { + for(int index: vvIndices[lev-1]) { + int cof0 = BDDBuildOne(index << 1, lev); + int cof1 = BDDBuildOne((index << 1) ^ 1, lev); + if(cof0 == cof1) { + vvRedundantIndices[lev-1].push_back(index); + } + } + } + + virtual int BDDBuild() { + BDDBuildStartup(); + for(int i = 1; i < nInputs; i++) { + BDDBuildLevel(i); + } + return BDDNodeCount(); + } + + virtual int BDDRebuild(int lev) { + vvIndices[lev].clear(); + vvIndices[lev+1].clear(); + for(int i = lev; i < lev + 2; i++) { + if(!i) { + for(int j = 0; j < nOutputs; j++) { + BDDBuildOne(j, 0); + } + } else { + vvRedundantIndices[i-1].clear(); + BDDBuildLevel(i); + } + } + if(lev < nInputs - 2) { + vvRedundantIndices[lev+1].clear(); + for(int index: vvIndices[lev+1]) { + if(IsEq(index << 1, (index << 1) ^ 1, lev + 2)) { + vvRedundantIndices[lev+1].push_back(index); + } + } + } + return BDDNodeCount(); + } + + virtual void Swap(int lev) { + assert(lev < nInputs - 1); + auto it0 = std::find(vLevels.begin(), vLevels.end(), lev); + auto it1 = std::find(vLevels.begin(), vLevels.end(), lev + 1); + std::swap(*it0, *it1); + if(nInputs - lev - 1 > lww) { + int nScopeSize = 1 << (nInputs - lev - 2 - lww); + for(int i = nScopeSize; i < nTotalSize; i += (nScopeSize << 2)) { + for(int j = 0; j < nScopeSize; j++) { + std::swap(t[i + j], t[i + nScopeSize + j]); + } + } + } else if(nInputs - lev - 1 == lww) { + for(int i = 0; i < nTotalSize; i += 2) { + t[i+1] ^= t[i] >> (ww / 2); + t[i] ^= t[i+1] << (ww / 2); + t[i+1] ^= t[i] >> (ww / 2); + } + } else { + for(int i = 0; i < nTotalSize; i++) { + int d = nInputs - lev - 2; + int shamt = 1 << d; + t[i] ^= (t[i] >> shamt) & swapmask[d]; + t[i] ^= (t[i] & swapmask[d]) << shamt; + t[i] ^= (t[i] >> shamt) & swapmask[d]; + } + } + } + + void SwapIndex(int &index, int d) { + if((index >> d) % 4 == 1) { + index += 1 << d; + } else if((index >> d) % 4 == 2) { + index -= 1 << d; + } + } + + virtual int BDDSwap(int lev) { + Swap(lev); + for(int i = lev + 2; i < nInputs; i++) { + for(uint j = 0; j < vvIndices[i].size(); j++) { + SwapIndex(vvIndices[i][j], i - (lev + 2)); + } + } + // swapping vvRedundantIndices is unnecessary for node counting + return BDDRebuild(lev); + } + + int SiftReo() { + int best = BDDBuild(); + Save(0); + SaveIndices(0); + std::vector vars(nInputs); + std::iota(vars.begin(), vars.end(), 0); + std::sort(vars.begin(), vars.end(), [&](int i1, int i2) {return BDDNodeCountLevel(vLevels[i1]) > BDDNodeCountLevel(vLevels[i2]);}); + bool turn = true; + for(int var: vars) { + bool updated = false; + int lev = vLevels[var]; + for(int i = lev; i < nInputs - 1; i++) { + int count = BDDSwap(i); + if(best > count) { + best = count; + updated = true; + Save(turn); + SaveIndices(turn); + } + } + if(lev) { + Load(!turn); + LoadIndices(!turn); + for(int i = lev - 1; i >= 0; i--) { + int count = BDDSwap(i); + if(best > count) { + best = count; + updated = true; + Save(turn); + SaveIndices(turn); + } + } + } + turn ^= updated; + Load(!turn); + LoadIndices(!turn); + } + return best; + } + + void Reo(std::vector vLevelsNew) { + for(int i = 0; i < nInputs; i++) { + int var = std::find(vLevelsNew.begin(), vLevelsNew.end(), i) - vLevelsNew.begin(); + int lev = vLevels[var]; + if(lev < i) { + for(int j = lev; j < i; j++) { + Swap(j); + } + } else if(lev > i) { + for(int j = lev - 1; j >= i; j--) { + Swap(j); + } + } + } + assert(vLevels == vLevelsNew); + } + + int RandomSiftReo(int nRound) { + int best = SiftReo(); + Save(2); + for(int i = 0; i < nRound; i++) { + std::vector vLevelsNew(nInputs); + std::iota(vLevelsNew.begin(), vLevelsNew.end(), 0); + std::shuffle(vLevelsNew.begin(), vLevelsNew.end(), rng); + Reo(vLevelsNew); + int r = SiftReo(); + if(best > r) { + best = r; + Save(2); + } + } + Load(2); + return best; + } + + int BDDGenerateAigRec(Gia_Man_t *pNew, std::vector const &vInputs, std::vector > &vvNodes, int index, int lev) { + int r = BDDFind(index, lev); + if(r >= 0) { + return vvNodes[lev][r >> 1] ^ (r & 1); + } + if(r >= -2) { + return r + 2; + } + int cof0 = BDDGenerateAigRec(pNew, vInputs, vvNodes, index << 1, lev + 1); + int cof1 = BDDGenerateAigRec(pNew, vInputs, vvNodes, (index << 1) ^ 1, lev + 1); + if(cof0 == cof1) { + return cof0; + } + int node; + if(Imply(index << 1, (index << 1) ^ 1, lev + 1)) { + node = Gia_ManHashOr(pNew, Gia_ManHashAnd(pNew, vInputs[lev], cof1), cof0); + } else if(Imply((index << 1) ^ 1, index << 1, lev + 1)) { + node = Gia_ManHashOr(pNew, Gia_ManHashAnd(pNew, vInputs[lev] ^ 1, cof0), cof1); + } else { + node = Gia_ManHashMux(pNew, vInputs[lev], cof1, cof0); + } + vvIndices[lev].push_back(index); + vvNodes[lev].push_back(node); + return node; + } + + virtual void BDDGenerateAig(Gia_Man_t *pNew, Vec_Int_t *vSupp) { + vvIndices.clear(); + vvIndices.resize(nInputs); + std::vector > vvNodes(nInputs); + std::vector vInputs(nInputs); + for(int i = 0; i < nInputs; i++) { + vInputs[vLevels[i]] = Vec_IntEntry(vSupp, nInputs - i - 1) << 1; + } + for(int i = 0; i < nOutputs; i++) { + int node = BDDGenerateAigRec(pNew, vInputs, vvNodes, i, 0); + Gia_ManAppendCo(pNew, node); + } + } +}; + +const word TruthTable::ones[7] = {ABC_CONST(0x0000000000000001), + ABC_CONST(0x0000000000000003), + ABC_CONST(0x000000000000000f), + ABC_CONST(0x00000000000000ff), + ABC_CONST(0x000000000000ffff), + ABC_CONST(0x00000000ffffffff), + ABC_CONST(0xffffffffffffffff)}; + +const word TruthTable::swapmask[5] = {ABC_CONST(0x2222222222222222), + ABC_CONST(0x0c0c0c0c0c0c0c0c), + ABC_CONST(0x00f000f000f000f0), + ABC_CONST(0x0000ff000000ff00), + ABC_CONST(0x00000000ffff0000)}; + +class TruthTableReo : public TruthTable { +public: + bool fBuilt = false; + std::vector > vvChildren; + std::vector > > vvChildrenSaved; + + TruthTableReo(int nInputs, int nOutputs): TruthTable(nInputs, nOutputs) {} + + void Save(uint i) override { + if(vLevelsSaved.size() < i + 1) { + vLevelsSaved.resize(i + 1); + } + vLevelsSaved[i] = vLevels; + } + + void Load(uint i) override { + assert(i < vLevelsSaved.size()); + vLevels = vLevelsSaved[i]; + } + + void SaveIndices(uint i) override { + TruthTable::SaveIndices(i); + if(vvChildrenSaved.size() < i + 1) { + vvChildrenSaved.resize(i + 1); + } + vvChildrenSaved[i] = vvChildren; + } + + void LoadIndices(uint i) override { + TruthTable::LoadIndices(i); + vvChildren = vvChildrenSaved[i]; + } + + void BDDBuildStartup() override { + vvChildren.clear(); + vvChildren.resize(nInputs); + TruthTable::BDDBuildStartup(); + } + + void BDDBuildLevel(int lev) override { + for(int index: vvIndices[lev-1]) { + int cof0 = BDDBuildOne(index << 1, lev); + int cof1 = BDDBuildOne((index << 1) ^ 1, lev); + vvChildren[lev-1].push_back(cof0); + vvChildren[lev-1].push_back(cof1); + if(cof0 == cof1) { + vvRedundantIndices[lev-1].push_back(index); + } + } + } + + int BDDBuild() override { + if(fBuilt) { + return BDDNodeCount(); + } + fBuilt = true; + BDDBuildStartup(); + for(int i = 1; i < nInputs + 1; i++) { + BDDBuildLevel(i); + } + return BDDNodeCount(); + } + + int BDDRebuildOne(int index, int cof0, int cof1, int lev, std::unordered_map, int, PairHasher> &unique, std::vector &vChildrenLow) { + if(cof0 < 0 && cof0 == cof1) { + return cof0; + } + bool fCompl = cof0 & 1; + if(fCompl) { + cof0 ^= 1; + cof1 ^= 1; + } + if(unique.count({cof0, cof1})) { + return (unique[{cof0, cof1}] << 1) ^ fCompl; + } + vvIndices[lev].push_back(index); + unique[{cof0, cof1}] = vvIndices[lev].size() - 1; + vChildrenLow.push_back(cof0); + vChildrenLow.push_back(cof1); + if(cof0 == cof1) { + vvRedundantIndices[lev].push_back(index); + } + return ((vvIndices[lev].size() - 1) << 1) ^ fCompl; + } + + int BDDRebuild(int lev) override { + vvRedundantIndices[lev].clear(); + vvRedundantIndices[lev+1].clear(); + std::vector vChildrenHigh; + std::vector vChildrenLow; + std::unordered_map, int, PairHasher> unique; + unique.reserve(2 * vvIndices[lev+1].size()); + vvIndices[lev+1].clear(); + for(uint i = 0; i < vvIndices[lev].size(); i++) { + int index = vvIndices[lev][i]; + int cof0index = vvChildren[lev][i+i] >> 1; + int cof1index = vvChildren[lev][i+i+1] >> 1; + bool cof0c = vvChildren[lev][i+i] & 1; + bool cof1c = vvChildren[lev][i+i+1] & 1; + int cof00, cof01, cof10, cof11; + if(cof0index < 0) { + cof00 = -2 ^ cof0c; + cof01 = -2 ^ cof0c; + } else { + cof00 = vvChildren[lev+1][cof0index+cof0index] ^ cof0c; + cof01 = vvChildren[lev+1][cof0index+cof0index+1] ^ cof0c; + } + if(cof1index < 0) { + cof10 = -2 ^ cof1c; + cof11 = -2 ^ cof1c; + } else { + cof10 = vvChildren[lev+1][cof1index+cof1index] ^ cof1c; + cof11 = vvChildren[lev+1][cof1index+cof1index+1] ^ cof1c; + } + int newcof0 = BDDRebuildOne(index << 1, cof00, cof10, lev + 1, unique, vChildrenLow); + int newcof1 = BDDRebuildOne((index << 1) ^ 1, cof01, cof11, lev + 1, unique, vChildrenLow); + vChildrenHigh.push_back(newcof0); + vChildrenHigh.push_back(newcof1); + if(newcof0 == newcof1) { + vvRedundantIndices[lev].push_back(index); + } + } + vvChildren[lev] = vChildrenHigh; + vvChildren[lev+1] = vChildrenLow; + return BDDNodeCount(); + } + + void Swap(int lev) override { + assert(lev < nInputs - 1); + auto it0 = std::find(vLevels.begin(), vLevels.end(), lev); + auto it1 = std::find(vLevels.begin(), vLevels.end(), lev + 1); + std::swap(*it0, *it1); + BDDRebuild(lev); + } + + int BDDSwap(int lev) override { + Swap(lev); + return BDDNodeCount(); + } + + virtual void BDDGenerateAig(Gia_Man_t *pNew, Vec_Int_t *vSupp) override { + abort(); + } +}; + +class TruthTableRewrite : public TruthTable { +public: + TruthTableRewrite(int nInputs, int nOutputs): TruthTable(nInputs, nOutputs) {} + + void SetValue(int index_lev, int lev, word value) { + assert(index_lev >= 0); + assert(nInputs - lev <= lww); + int logwidth = nInputs - lev; + int index = index_lev >> (lww - logwidth); + int pos = (index_lev % (1 << (lww - logwidth))) << logwidth; + t[index] &= ~(ones[logwidth] << pos); + t[index] ^= value << pos; + } + + void CopyFunc(int index1, int index2, int lev, bool fCompl) { + assert(index1 >= 0); + int logwidth = nInputs - lev; + if(logwidth > lww) { + int nScopeSize = 1 << (logwidth - lww); + if(!fCompl) { + if(index2 < 0) { + for(int i = 0; i < nScopeSize; i++) { + t[nScopeSize * index1 + i] = 0; + } + } else { + for(int i = 0; i < nScopeSize; i++) { + t[nScopeSize * index1 + i] = t[nScopeSize * index2 + i]; + } + } + } else { + if(index2 < 0) { + for(int i = 0; i < nScopeSize; i++) { + t[nScopeSize * index1 + i] = ones[lww]; + } + } else { + for(int i = 0; i < nScopeSize; i++) { + t[nScopeSize * index1 + i] = ~t[nScopeSize * index2 + i]; + } + } + } + } else { + word value = 0; + if(index2 >= 0) { + value = GetValue(index2, lev); + } + if(fCompl) { + value ^= ones[logwidth]; + } + SetValue(index1, lev, value); + } + } + + void ShiftToMajority(int index, int lev) { + assert(index >= 0); + int logwidth = nInputs - lev; + int count = 0; + if(logwidth > lww) { + int nScopeSize = 1 << (logwidth - lww); + for(int i = 0; i < nScopeSize; i++) { + count += bsw(t[nScopeSize * index + i]).count(); + } + } else { + count = bsw(GetValue(index, lev)).count(); + } + bool majority = count > (1 << (logwidth - 1)); + CopyFunc(index, -1, lev, majority); + } +}; + +class TruthTableCare : public TruthTableRewrite { +public: + std::vector originalt; + std::vector caret; + std::vector care; + + std::vector > > vvMergedIndices; + + std::vector > savedcare; + std::vector > > > vvMergedIndicesSaved; + + TruthTableCare(int nInputs, int nOutputs): TruthTableRewrite(nInputs, nOutputs) { + if(nSize) { + care.resize(nSize); + } else { + care.resize(1); + } + } + + void Save(uint i) override { + TruthTable::Save(i); + if(savedcare.size() < i + 1) { + savedcare.resize(i + 1); + } + savedcare[i] = care; + } + + void Load(uint i) override { + TruthTable::Load(i); + care = savedcare[i]; + } + + void SaveIndices(uint i) override { + TruthTable::SaveIndices(i); + if(vvMergedIndicesSaved.size() < i + 1) { + vvMergedIndicesSaved.resize(i + 1); + } + vvMergedIndicesSaved[i] = vvMergedIndices; + } + + void LoadIndices(uint i) override { + TruthTable::LoadIndices(i); + vvMergedIndices = vvMergedIndicesSaved[i]; + } + + void Swap(int lev) override { + TruthTable::Swap(lev); + if(nInputs - lev - 1 > lww) { + int nScopeSize = 1 << (nInputs - lev - 2 - lww); + for(int i = nScopeSize; i < nSize; i += (nScopeSize << 2)) { + for(int j = 0; j < nScopeSize; j++) { + std::swap(care[i + j], care[i + nScopeSize + j]); + } + } + } else if(nInputs - lev - 1 == lww) { + for(int i = 0; i < nSize; i += 2) { + care[i+1] ^= care[i] >> (ww / 2); + care[i] ^= care[i+1] << (ww / 2); + care[i+1] ^= care[i] >> (ww / 2); + } + } else { + for(int i = 0; i < nSize || (i == 0 && !nSize); i++) { + int d = nInputs - lev - 2; + int shamt = 1 << d; + care[i] ^= (care[i] >> shamt) & swapmask[d]; + care[i] ^= (care[i] & swapmask[d]) << shamt; + care[i] ^= (care[i] >> shamt) & swapmask[d]; + } + } + } + + void RestoreCare() { + caret.clear(); + if(nSize) { + for(int i = 0; i < nOutputs; i++) { + caret.insert(caret.end(), care.begin(), care.end()); + } + } else { + caret.resize(nTotalSize); + for(int i = 0; i < nOutputs; i++) { + int padding = i * (1 << nInputs); + caret[padding / ww] |= care[0] << (padding % ww); + } + } + } + + word GetCare(int index_lev, int lev) { + assert(index_lev >= 0); + assert(nInputs - lev <= lww); + int logwidth = nInputs - lev; + int index = index_lev >> (lww - logwidth); + int pos = (index_lev % (1 << (lww - logwidth))) << logwidth; + return (caret[index] >> pos) & ones[logwidth]; + } + + void CopyFuncMasked(int index1, int index2, int lev, bool fCompl) { + assert(index1 >= 0); + assert(index2 >= 0); + int logwidth = nInputs - lev; + if(logwidth > lww) { + int nScopeSize = 1 << (logwidth - lww); + for(int i = 0; i < nScopeSize; i++) { + word value = t[nScopeSize * index2 + i]; + if(fCompl) { + value = ~value; + } + word cvalue = caret[nScopeSize * index2 + i]; + t[nScopeSize * index1 + i] &= ~cvalue; + t[nScopeSize * index1 + i] |= cvalue & value; + } + } else { + word one = ones[logwidth]; + word value1 = GetValue(index1, lev); + word value2 = GetValue(index2, lev); + if(fCompl) { + value2 ^= one; + } + word cvalue = GetCare(index2, lev); + value1 &= cvalue ^ one; + value1 |= cvalue & value2; + SetValue(index1, lev, value1); + } + } + + bool IsDC(int index, int lev) { + if(nInputs - lev > lww) { + int nScopeSize = 1 << (nInputs - lev - lww); + for(int i = 0; i < nScopeSize; i++) { + if(caret[nScopeSize * index + i]) { + return false; + } + } + } else if(GetCare(index, lev)) { + return false; + } + return true; + } + + int Include(int index1, int index2, int lev, bool fCompl) { + assert(index1 >= 0); + assert(index2 >= 0); + int logwidth = nInputs - lev; + bool fEq = true; + if(logwidth > lww) { + int nScopeSize = 1 << (logwidth - lww); + for(int i = 0; i < nScopeSize && (fEq || fCompl); i++) { + word cvalue = caret[nScopeSize * index2 + i]; + if(~caret[nScopeSize * index1 + i] & cvalue) { + return 0; + } + word value = t[nScopeSize * index1 + i] ^ t[nScopeSize * index2 + i]; + fEq &= !(value & cvalue); + fCompl &= !(~value & cvalue); + } + } else { + word cvalue = GetCare(index2, lev); + if((GetCare(index1, lev) ^ ones[logwidth]) & cvalue) { + return 0; + } + word value = GetValue(index1, lev) ^ GetValue(index2, lev); + fEq &= !(value & cvalue); + fCompl &= !((value ^ ones[logwidth]) & cvalue); + } + return 2 * fCompl + fEq; + } + + int Intersect(int index1, int index2, int lev, bool fCompl, bool fEq = true) { + assert(index1 >= 0); + assert(index2 >= 0); + int logwidth = nInputs - lev; + if(logwidth > lww) { + int nScopeSize = 1 << (logwidth - lww); + for(int i = 0; i < nScopeSize && (fEq || fCompl); i++) { + word value = t[nScopeSize * index1 + i] ^ t[nScopeSize * index2 + i]; + word cvalue = caret[nScopeSize * index1 + i] & caret[nScopeSize * index2 + i]; + fEq &= !(value & cvalue); + fCompl &= !(~value & cvalue); + } + } else { + word value = GetValue(index1, lev) ^ GetValue(index2, lev); + word cvalue = GetCare(index1, lev) & GetCare(index2, lev); + fEq &= !(value & cvalue); + fCompl &= !((value ^ ones[logwidth]) & cvalue); + } + return 2 * fCompl + fEq; + } + + void MergeCare(int index1, int index2, int lev) { + assert(index1 >= 0); + assert(index2 >= 0); + int logwidth = nInputs - lev; + if(logwidth > lww) { + int nScopeSize = 1 << (logwidth - lww); + for(int i = 0; i < nScopeSize; i++) { + caret[nScopeSize * index1 + i] |= caret[nScopeSize * index2 + i]; + } + } else { + word value = GetCare(index2, lev); + int index = index1 >> (lww - logwidth); + int pos = (index1 % (1 << (lww - logwidth))) << logwidth; + caret[index] |= value << pos; + } + } + + void Merge(int index1, int index2, int lev, bool fCompl) { + MergeCare(index1, index2, lev); + vvMergedIndices[lev].push_back({(index1 << 1) ^ fCompl, index2}); + } + + int BDDBuildOne(int index, int lev) override { + int r = BDDFind(index, lev); + if(r >= -2) { + if(r >= 0) { + Merge(vvIndices[lev][r >> 1], index, lev, r & 1); + } + return r; + } + vvIndices[lev].push_back(index); + return (vvIndices[lev].size() - 1) << 1; + } + + void CompleteMerge() { + for(int i = nInputs - 1; i >= 0; i--) { + for(auto it = vvMergedIndices[i].rbegin(); it != vvMergedIndices[i].rend(); it++) { + CopyFunc((*it).second, (*it).first >> 1, i, (*it).first & 1); + } + } + } + + void BDDBuildStartup() override { + RestoreCare(); + vvIndices.clear(); + vvIndices.resize(nInputs); + vvRedundantIndices.clear(); + vvRedundantIndices.resize(nInputs); + vvMergedIndices.clear(); + vvMergedIndices.resize(nInputs); + for(int i = 0; i < nOutputs; i++) { + if(!IsDC(i, 0)) { + BDDBuildOne(i, 0); + } + } + } + + virtual void BDDRebuildByMerge(int lev) { + for(auto &p: vvMergedIndices[lev]) { + MergeCare(p.first >> 1, p.second, lev); + } + } + + int BDDRebuild(int lev) override { + RestoreCare(); + for(int i = lev; i < nInputs; i++) { + vvIndices[i].clear(); + vvMergedIndices[i].clear(); + if(i) { + vvRedundantIndices[i-1].clear(); + } + } + for(int i = 0; i < lev; i++) { + BDDRebuildByMerge(i); + } + for(int i = lev; i < nInputs; i++) { + if(!i) { + for(int j = 0; j < nOutputs; j++) { + if(!IsDC(j, 0)) { + BDDBuildOne(j, 0); + } + } + } else { + BDDBuildLevel(i); + } + } + return BDDNodeCount(); + } + + int BDDSwap(int lev) override { + Swap(lev); + return BDDRebuild(lev); + } + + void OptimizationStartup() { + originalt = t; + RestoreCare(); + vvIndices.clear(); + vvIndices.resize(nInputs); + vvMergedIndices.clear(); + vvMergedIndices.resize(nInputs); + for(int i = 0; i < nOutputs; i++) { + if(!IsDC(i, 0)) { + BDDBuildOne(i, 0); + } else { + ShiftToMajority(i, 0); + } + } + } + + virtual void Optimize() { + OptimizationStartup(); + for(int i = 1; i < nInputs; i++) { + for(int index: vvIndices[i-1]) { + BDDBuildOne(index << 1, i); + BDDBuildOne((index << 1) ^ 1, i); + } + } + CompleteMerge(); + } +}; + +class TruthTableLevelTSM : public TruthTableCare { +public: + TruthTableLevelTSM(int nInputs, int nOutputs): TruthTableCare(nInputs, nOutputs) {} + + int BDDFindTSM(int index, int lev) { + int logwidth = nInputs - lev; + if(logwidth > lww) { + int nScopeSize = 1 << (logwidth - lww); + bool fZero = true; + bool fOne = true; + for(int i = 0; i < nScopeSize && (fZero || fOne); i++) { + word value = t[nScopeSize * index + i]; + word cvalue = caret[nScopeSize * index + i]; + fZero &= !(value & cvalue); + fOne &= !(~value & cvalue); + } + if(fZero || fOne) { + return -2 ^ fOne; + } + for(int index2: vvIndices[lev]) { + bool fEq = true; + bool fCompl = true; + for(int i = 0; i < nScopeSize && (fEq || fCompl); i++) { + word value = t[nScopeSize * index + i] ^ t[nScopeSize * index2 + i]; + word cvalue = caret[nScopeSize * index + i] & caret[nScopeSize * index2 + i]; + fEq &= !(value & cvalue); + fCompl &= !(~value & cvalue); + } + if(fEq || fCompl) { + return (index2 << 1) ^ !fEq; + } + } + } else { + word one = ones[logwidth]; + word value = GetValue(index, lev); + word cvalue = GetCare(index, lev); + if(!(value & cvalue)) { + return -2; + } + if(!((value ^ one) & cvalue)) { + return -1; + } + for(int index2: vvIndices[lev]) { + word value2 = value ^ GetValue(index2, lev); + word cvalue2 = cvalue & GetCare(index2, lev); + if(!(value2 & cvalue2)) { + return index2 << 1; + } + if(!((value2 ^ one) & cvalue2)) { + return (index2 << 1) ^ 1; + } + } + } + return -3; + } + + int BDDBuildOne(int index, int lev) override { + int r = BDDFindTSM(index, lev); + if(r >= -2) { + if(r >= 0) { + CopyFuncMasked(r >> 1, index, lev, r & 1); + Merge(r >> 1, index, lev, r & 1); + } else { + vvMergedIndices[lev].push_back({r, index}); + } + return r; + } + vvIndices[lev].push_back(index); + return index << 1; + } + + int BDDBuild() override { + TruthTable::Save(3); + int r = TruthTable::BDDBuild(); + TruthTable::Load(3); + return r; + } + + void BDDRebuildByMerge(int lev) override { + for(auto &p: vvMergedIndices[lev]) { + if(p.first >= 0) { + CopyFuncMasked(p.first >> 1, p.second, lev, p.first & 1); + MergeCare(p.first >> 1, p.second, lev); + } + } + } + + int BDDRebuild(int lev) override { + TruthTable::Save(3); + int r = TruthTableCare::BDDRebuild(lev); + TruthTable::Load(3); + return r; + } +}; + +} + +extern "C" +Vec_Int_t * Gia_ManCollectSuppNew( Gia_Man_t * p, int iOut, int nOuts ); + +extern "C" +Gia_Man_t * Gia_ManTtopt( Gia_Man_t * p, int nIns, int nOuts, int nRounds ) +{ + Gia_Man_t * pNew; + Gia_Obj_t * pObj; + Vec_Int_t * vSupp; + word v; + word * pTruth; + int i, g, k, nInputs; + 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 ); + for ( g = 0; g < Gia_ManCoNum(p); g += nOuts ) + { + vSupp = Gia_ManCollectSuppNew( p, g, nOuts ); + nInputs = Vec_IntSize( vSupp ); + Ttopt::TruthTableReo tt( nInputs, nOuts ); + for ( k = 0; k < nOuts; k++ ) + { + pObj = Gia_ManCo( p, g+k ); + pTruth = Gia_ObjComputeTruthTableCut( p, Gia_ObjFanin0(pObj), vSupp ); + if ( nInputs >= 6 ) + for ( i = 0; i < tt.nSize; i++ ) + tt.t[i + tt.nSize * k] = Gia_ObjFaninC0(pObj)? ~pTruth[i]: pTruth[i]; + else + { + i = k * (1 << nInputs); + v = (Gia_ObjFaninC0(pObj)? ~pTruth[0]: pTruth[0]) & tt.ones[nInputs]; + tt.t[i / tt.ww] |= v << (i % tt.ww); + } + } + tt.RandomSiftReo( nRounds ); + Ttopt::TruthTable tt2( nInputs, nOuts ); + tt2.t = tt.t; + tt2.Reo( tt.vLevels ); + tt2.BDDGenerateAig( pNew, vSupp ); + Vec_IntFree( vSupp ); + } + Gia_ObjComputeTruthTableStop( p ); + Gia_ManHashStop( pNew ); + Gia_ManSetRegNum( pNew, Gia_ManRegNum(p) ); + return pNew; +} + +extern "C" +word * Gia_ManCountFraction( Gia_Man_t * p, Vec_Wrd_t * vSimI, Vec_Int_t * vSupp, int Thresh, int fVerbose, int * pCare ); + +extern "C" +Gia_Man_t * Gia_ManTtoptCare( Gia_Man_t * p, int nIns, int nOuts, int nRounds, char * pFileName, int nRarity ) +{ + int fVerbose = 0; + Gia_Man_t * pNew; + Gia_Obj_t * pObj; + Vec_Int_t * vSupp; + word v; + word * pTruth, * pCare; + int i, g, k, nInputs; + Vec_Wrd_t * vSimI = Vec_WrdReadBin( pFileName, fVerbose ); + 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 ); + for ( g = 0; g < Gia_ManCoNum(p); g += nOuts ) + { + vSupp = Gia_ManCollectSuppNew( p, g, nOuts ); + nInputs = Vec_IntSize( vSupp ); + Ttopt::TruthTableLevelTSM tt( nInputs, nOuts ); + for ( k = 0; k < nOuts; k++ ) + { + pObj = Gia_ManCo( p, g+k ); + pTruth = Gia_ObjComputeTruthTableCut( p, Gia_ObjFanin0(pObj), vSupp ); + if ( nInputs >= 6 ) + for ( i = 0; i < tt.nSize; i++ ) + tt.t[i + tt.nSize * k] = Gia_ObjFaninC0(pObj)? ~pTruth[i]: pTruth[i]; + else + { + i = k * (1 << nInputs); + v = (Gia_ObjFaninC0(pObj)? ~pTruth[0]: pTruth[0]) & tt.ones[nInputs]; + tt.t[i / tt.ww] |= v << (i % tt.ww); + } + } + i = 1 << Vec_IntSize( vSupp ); + pCare = Gia_ManCountFraction( p, vSimI, vSupp, nRarity, fVerbose, &i ); + tt.care[0] = pCare[0]; + for ( i = 1; i < tt.nSize; i++ ) + tt.care[i] = pCare[i]; + ABC_FREE( pCare ); + tt.RandomSiftReo( nRounds ); + tt.Optimize(); + tt.BDDGenerateAig( pNew, vSupp ); + Vec_IntFree( vSupp ); + } + Gia_ObjComputeTruthTableStop( p ); + Gia_ManHashStop( pNew ); + Gia_ManSetRegNum( pNew, Gia_ManRegNum(p) ); + Vec_WrdFreeP( &vSimI ); + return pNew; +} + +ABC_NAMESPACE_IMPL_END diff --git a/src/aig/gia/module.make b/src/aig/gia/module.make index cd2e0afe..870da208 100644 --- a/src/aig/gia/module.make +++ b/src/aig/gia/module.make @@ -105,5 +105,6 @@ SRC += src/aig/gia/giaAig.c \ src/aig/gia/giaTis.c \ src/aig/gia/giaTruth.c \ src/aig/gia/giaTsim.c \ + src/aig/gia/giaTtopt.cpp \ src/aig/gia/giaUnate.c \ src/aig/gia/giaUtil.c diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c index b789be1f..ac8a97fc 100644 --- a/src/base/abci/abc.c +++ b/src/base/abci/abc.c @@ -499,6 +499,7 @@ static int Abc_CommandAbc9LNetRead ( Abc_Frame_t * pAbc, int argc, cha static int Abc_CommandAbc9LNetSim ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandAbc9LNetEval ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandAbc9LNetOpt ( Abc_Frame_t * pAbc, int argc, char ** argv ); +static int Abc_CommandAbc9Ttopt ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandAbc9LNetMap ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandAbc9Unmap ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandAbc9Struct ( Abc_Frame_t * pAbc, int argc, char ** argv ); @@ -1249,6 +1250,7 @@ void Abc_Init( Abc_Frame_t * pAbc ) Cmd_CommandAdd( pAbc, "ABC9", "&lnetsim", Abc_CommandAbc9LNetSim, 0 ); Cmd_CommandAdd( pAbc, "ABC9", "&lneteval", Abc_CommandAbc9LNetEval, 0 ); Cmd_CommandAdd( pAbc, "ABC9", "&lnetopt", Abc_CommandAbc9LNetOpt, 0 ); + Cmd_CommandAdd( pAbc, "ABC9", "&ttopt", Abc_CommandAbc9Ttopt, 0 ); Cmd_CommandAdd( pAbc, "ABC9", "&lnetmap", Abc_CommandAbc9LNetMap, 0 ); Cmd_CommandAdd( pAbc, "ABC9", "&unmap", Abc_CommandAbc9Unmap, 0 ); Cmd_CommandAdd( pAbc, "ABC9", "&struct", Abc_CommandAbc9Struct, 0 ); @@ -42191,6 +42193,113 @@ usage: return 1; } +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Abc_CommandAbc9Ttopt( Abc_Frame_t * pAbc, int argc, char ** argv ) +{ + extern Gia_Man_t * Gia_ManTtopt( Gia_Man_t * p, int nIns, int nOuts, int nRounds ); + extern Gia_Man_t * Gia_ManTtoptCare( Gia_Man_t * p, int nIns, int nOuts, int nRounds, char * pFileName, int nRarity ); + Gia_Man_t * pTemp; + char * pFileName = NULL; + int c, nIns = 6, nOuts = 2, Limit = 0, nRounds = 20, fVerbose = 0; + Extra_UtilGetoptReset(); + while ( ( c = Extra_UtilGetopt( argc, argv, "IORXvh" ) ) != EOF ) + { + switch ( c ) + { + case 'I': + if ( globalUtilOptind >= argc ) + { + Abc_Print( -1, "Command line switch \"-I\" should be followed by a positive integer.\n" ); + goto usage; + } + nIns = atoi(argv[globalUtilOptind]); + globalUtilOptind++; + break; + case 'O': + if ( globalUtilOptind >= argc ) + { + Abc_Print( -1, "Command line switch \"-O\" should be followed by a positive integer.\n" ); + goto usage; + } + nOuts = atoi(argv[globalUtilOptind]); + globalUtilOptind++; + break; + case 'R': + if ( globalUtilOptind >= argc ) + { + Abc_Print( -1, "Command line switch \"-R\" should be followed by a positive integer.\n" ); + goto usage; + } + Limit = atoi(argv[globalUtilOptind]); + globalUtilOptind++; + break; + case 'X': + if ( globalUtilOptind >= argc ) + { + Abc_Print( -1, "Command line switch \"-X\" should be followed by a positive integer.\n" ); + goto usage; + } + nRounds = atoi(argv[globalUtilOptind]); + globalUtilOptind++; + break; + case 'v': + fVerbose ^= 1; + break; + case 'h': + default: + goto usage; + } + } + if ( argc > globalUtilOptind + 1 ) + { + return 0; + } + if ( pAbc->pGia == NULL ) + { + Abc_Print( -1, "Empty GIA network.\n" ); + return 1; + } + if ( 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_ManTtoptCare( pAbc->pGia, nIns, nOuts, nRounds, pFileName, Limit ); + else + pTemp = Gia_ManTtopt( pAbc->pGia, nIns, nOuts, nRounds ); + Abc_FrameUpdateGia( pAbc, pTemp ); + return 0; + +usage: + Abc_Print( -2, "usage: &ttopt [-IORX num] [-vh] \n" ); + Abc_Print( -2, "\t performs specialized AIG optimization\n" ); + Abc_Print( -2, "\t-I num : the input support size [default = %d]\n", nIns ); + Abc_Print( -2, "\t-O num : the output group size [default = %d]\n", nOuts ); + Abc_Print( -2, "\t-R num : patterns are cares starting this value [default = %d]\n", Limit ); + Abc_Print( -2, "\t-X num : the number of optimization rounds [default = %d]\n", nRounds ); + Abc_Print( -2, "\t-v : toggles verbose output [default = %s]\n", fVerbose? "yes": "no" ); + Abc_Print( -2, "\t-h : prints the command usage\n"); + Abc_Print( -2, "\t : file name with simulation information\n"); + return 1; +} + /**Function************************************************************* Synopsis [] -- cgit v1.2.3