From 5700bff205d3827d98b0b021de136d3cddc81c57 Mon Sep 17 00:00:00 2001 From: jiunhaochen Date: Wed, 9 Apr 2025 19:27:32 +0800 Subject: [PATCH] command rewire add external care --- src/base/abci/abc.c | 69 ++++++++++++++++--- src/opt/rar/rewire_miaig.cpp | 130 +++++++++++++++++++++++------------ src/opt/rar/rewire_miaig.h | 43 ++++++++---- src/opt/rar/rewire_rar.c | 12 ++-- src/opt/rar/rewire_rar.h | 12 ++-- src/opt/rar/rewire_tt.h | 6 ++ 6 files changed, 193 insertions(+), 79 deletions(-) diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c index f0ac69548..00eb766b7 100644 --- a/src/base/abci/abc.c +++ b/src/base/abci/abc.c @@ -20664,15 +20664,17 @@ usage: ***********************************************************************/ int Abc_CommandRewire( Abc_Frame_t * pAbc, int argc, char ** argv ) { - extern Abc_Ntk_t *Abc_ManRewire(Abc_Ntk_t *pNtk, int nIters, float levelGrowRatio, int nExpands, int nGrowth, int nDivs, int nFaninMax, int nTimeOut, int nMode, int nMappedMode, int nDist, int nSeed, int fVerbose); + extern Abc_Ntk_t *Abc_ManRewire(Abc_Ntk_t *pNtk, Gia_Man_t *pExc, int nIters, float levelGrowRatio, int nExpands, int nGrowth, int nDivs, int nFaninMax, int nTimeOut, int nMode, int nMappedMode, int nDist, int nSeed, int fCheck, int fVerbose); Abc_Ntk_t *pNtk, *pTemp; - int c, nIters = 100000, nExpands = 128, nGrowth = 4, nDivs = -1, nFaninMax = 8, nSeed = 1, nTimeOut = 0, nVerbose = 1, nMode = 0, nMappedMode = 0, nDist = 0; + Gia_Man_t *pExc = NULL; + FILE *pFile = NULL; + int c, nIters = 100000, nExpands = 128, nGrowth = 4, nDivs = -1, nFaninMax = 8, nSeed = 1, nTimeOut = 0, nVerbose = 1, nMode = 0, nMappedMode = 0, nDist = 0, fCheck = 0; float nLevelGrowRatio = 0; Extra_UtilGetoptReset(); pNtk = Abc_FrameReadNtk(pAbc); - while ( ( c = Extra_UtilGetopt( argc, argv, "IEGDFSTMALRVh" ) ) != EOF ) { + while ( ( c = Extra_UtilGetopt( argc, argv, "IEGDFSTMALRCVch" ) ) != EOF ) { switch ( c ) { case 'I': if ( globalUtilOptind >= argc ) @@ -20773,6 +20775,22 @@ int Abc_CommandRewire( Abc_Frame_t * pAbc, int argc, char ** argv ) nLevelGrowRatio = atof(argv[globalUtilOptind]); globalUtilOptind++; break; + case 'C': + pFile = fopen( argv[globalUtilOptind], "rb" ); + if ( pFile == NULL ) + { + Abc_Print( -1, "Cannot open input file \"%s\". ", argv[globalUtilOptind] ); + return 1; + } + fclose( pFile ); + pExc = Gia_AigerRead( argv[globalUtilOptind], 0, 0, 0 ); + if ( pExc == NULL ) + { + Abc_Print( -1, "Reading Exc AIGER has failed.\n" ); + return 1; + } + globalUtilOptind++; + break; case 'V': if ( globalUtilOptind >= argc ) { @@ -20782,6 +20800,9 @@ int Abc_CommandRewire( Abc_Frame_t * pAbc, int argc, char ** argv ) nVerbose = atoi(argv[globalUtilOptind]); globalUtilOptind++; break; + case 'c': + fCheck ^= 1; + break; case 'h': default: goto usage; @@ -20803,7 +20824,9 @@ int Abc_CommandRewire( Abc_Frame_t * pAbc, int argc, char ** argv ) return 1; } - pTemp = Abc_ManRewire( pNtk, nIters, nLevelGrowRatio, nExpands, nGrowth, nDivs, nFaninMax, nTimeOut, nMode, nMappedMode, nDist, nSeed, nVerbose ); + pTemp = Abc_ManRewire( pNtk, pExc, nIters, nLevelGrowRatio, nExpands, nGrowth, nDivs, nFaninMax, nTimeOut, nMode, nMappedMode, nDist, nSeed, fCheck, nVerbose ); + if ( pExc ) + Gia_ManStop( pExc ); Abc_FrameReplaceCurrentNetwork( pAbc, pTemp ); return 0; @@ -20818,9 +20841,11 @@ usage: Abc_Print( -2, "\t-R : level constraint (0: unlimited, 1: preserve level) [default = %g]\n", nLevelGrowRatio); Abc_Print( -2, "\t-M : optimization target [default = %s]\n", nMode ? "area" : "AIG node" ); Abc_Print( -2, "\t-A : mapper (0: amap, 1: &nf, 2: &simap) (experimental) [default = %d]\n", nMappedMode ); + Abc_Print( -2, "\t-C : AIGER specifying external cares\n"); Abc_Print( -2, "\t-S : the random seed (0: random, >= 1: user defined) [default = %d]\n", nSeed ); Abc_Print( -2, "\t-T : the timeout in seconds (0: unlimited) [default = %d]\n", nTimeOut ); Abc_Print( -2, "\t-V : the verbosity level [default = %d]\n", nVerbose ); + Abc_Print( -2, "\t-c : check the equivalence [default = %s]\n", fCheck ? "yes" : "no" ); Abc_Print( -2, "\t-h : prints the command usage\n" ); Abc_Print( -2, "\n\tThis command was contributed by Jiun-Hao Chen from National Taiwan University.\n" ); return 1; @@ -46326,13 +46351,14 @@ usage: ***********************************************************************/ int Abc_CommandAbc9Rewire( Abc_Frame_t * pAbc, int argc, char ** argv ) { - extern Gia_Man_t *Gia_ManRewire(Gia_Man_t *pGia, int nIters, float levelGrowRatio, int nExpands, int nGrowth, int nDivs, int nFaninMax, int nTimeOut, int nMode, int nMappedMode, int nDist, int nSeed, int fVerbose); - Gia_Man_t *pTemp; - int c, nIters = 100000, nExpands = 128, nGrowth = 4, nDivs = -1, nFaninMax = 8, nSeed = 1, nTimeOut = 0, nVerbose = 1, nMode = 0, nMappedMode = 0, nDist = 0; + extern Gia_Man_t *Gia_ManRewire(Gia_Man_t *pGia, Gia_Man_t *pExc, int nIters, float levelGrowRatio, int nExpands, int nGrowth, int nDivs, int nFaninMax, int nTimeOut, int nMode, int nMappedMode, int nDist, int nSeed, int fCheck, int fVerbose); + FILE *pFile = NULL; + Gia_Man_t *pTemp, *pExc = NULL; + int c, nIters = 100000, nExpands = 128, nGrowth = 4, nDivs = -1, nFaninMax = 8, nSeed = 1, nTimeOut = 0, nVerbose = 1, nMode = 0, nMappedMode = 0, nDist = 0, fCheck = 0; float nLevelGrowRatio = 0; Extra_UtilGetoptReset(); - while ( ( c = Extra_UtilGetopt( argc, argv, "IEGDFSTMALRVh" ) ) != EOF ) { + while ( ( c = Extra_UtilGetopt( argc, argv, "IEGDFSTMALRCVch" ) ) != EOF ) { switch ( c ) { case 'I': if ( globalUtilOptind >= argc ) @@ -46433,6 +46459,22 @@ int Abc_CommandAbc9Rewire( Abc_Frame_t * pAbc, int argc, char ** argv ) nLevelGrowRatio = atof(argv[globalUtilOptind]); globalUtilOptind++; break; + case 'C': + pFile = fopen( argv[globalUtilOptind], "rb" ); + if ( pFile == NULL ) + { + Abc_Print( -1, "Cannot open input file \"%s\". ", argv[globalUtilOptind] ); + return 1; + } + fclose( pFile ); + pExc = Gia_AigerRead( argv[globalUtilOptind], 0, 0, 0 ); + if ( pExc == NULL ) + { + Abc_Print( -1, "Reading Exc AIGER has failed.\n" ); + return 1; + } + globalUtilOptind++; + break; case 'V': if ( globalUtilOptind >= argc ) { @@ -46442,6 +46484,9 @@ int Abc_CommandAbc9Rewire( Abc_Frame_t * pAbc, int argc, char ** argv ) nVerbose = atoi(argv[globalUtilOptind]); globalUtilOptind++; break; + case 'c': + fCheck ^= 1; + break; case 'h': default: goto usage; @@ -46463,9 +46508,9 @@ int Abc_CommandAbc9Rewire( Abc_Frame_t * pAbc, int argc, char ** argv ) return 1; } - pTemp = Gia_ManRewire( pAbc->pGia, nIters, nLevelGrowRatio, nExpands, nGrowth, nDivs, nFaninMax, nTimeOut, nMode, nMappedMode, nDist, nSeed, nVerbose ); - if ( pTemp->pName == NULL ) - pTemp->pName = Abc_UtilStrsav(Extra_FileNameWithoutPath(pAbc->pGia->pName)); + pTemp = Gia_ManRewire( pAbc->pGia, pExc, nIters, nLevelGrowRatio, nExpands, nGrowth, nDivs, nFaninMax, nTimeOut, nMode, nMappedMode, nDist, nSeed, fCheck, nVerbose ); + if ( pExc ) + Gia_ManStop( pExc ); Abc_FrameUpdateGia( pAbc, pTemp ); return 0; @@ -46481,9 +46526,11 @@ usage: Abc_Print( -2, "\t-R : level constraint (0: unlimited, 1: preserve level) [default = %g]\n", nLevelGrowRatio); Abc_Print( -2, "\t-M : optimization target [default = %s]\n", nMode ? "area" : "AIG node" ); Abc_Print( -2, "\t-A : mapper (0: amap, 1: &nf, 2: &simap) (experimental) [default = %d]\n", nMappedMode ); + Abc_Print( -2, "\t-C : AIGER specifying external cares\n"); Abc_Print( -2, "\t-S : the random seed (0: random, >= 1: user defined) [default = %d]\n", nSeed ); Abc_Print( -2, "\t-T : the timeout in seconds (0: unlimited) [default = %d]\n", nTimeOut ); Abc_Print( -2, "\t-V : the verbosity level [default = %d]\n", nVerbose ); + Abc_Print( -2, "\t-c : check the equivalence [default = %s]\n", fCheck ? "yes" : "no" ); Abc_Print( -2, "\t-h : prints the command usage\n" ); Abc_Print( -2, "\n\tThis command was contributed by Jiun-Hao Chen from National Taiwan University.\n" ); return 1; diff --git a/src/opt/rar/rewire_miaig.cpp b/src/opt/rar/rewire_miaig.cpp index 59070349f..dffb29fa7 100644 --- a/src/opt/rar/rewire_miaig.cpp +++ b/src/opt/rar/rewire_miaig.cpp @@ -26,22 +26,28 @@ ABC_NAMESPACE_IMPL_START #endif // RW_ABC #ifdef RW_ABC -Gia_Man_t *Gia_ManRewireInt(Gia_Man_t *pGia, int nIters, float levelGrowRatio, int nExpands, int nGrowth, int nDivs, int nFaninMax, int nTimeOut, int nMode, int nMappedMode, int nDist, int nSeed, int fVerbose) { +Gia_Man_t *Gia_ManRewireInt(Gia_Man_t *pGia, Gia_Man_t *pExc, int nIters, float levelGrowRatio, int nExpands, int nGrowth, int nDivs, int nFaninMax, int nTimeOut, int nMode, int nMappedMode, int nDist, int nSeed, int fCheck, int fVerbose) { Random_Num(nSeed == 0 ? Abc_Random(0) % 10 : nSeed); + assert(Gia_ManCiNum(pGia) <= 58); Rewire::Miaig pNtkMiaig(pGia); - Rewire::Miaig pNew = pNtkMiaig.rewire(nIters, levelGrowRatio, nExpands, nGrowth, nDivs, nFaninMax, nTimeOut, nMode, nMappedMode, nDist, fVerbose); + if (pExc) + pNtkMiaig.setExc(pExc); + Rewire::Miaig pNew = pNtkMiaig.rewire(nIters, levelGrowRatio, nExpands, nGrowth, nDivs, nFaninMax, nTimeOut, nMode, nMappedMode, nDist, fCheck, fVerbose); pNew.setName(Gia_ManName(pGia)); return pNew.toGia(); } -Abc_Ntk_t *Abc_ManRewireInt(Abc_Ntk_t *pNtk, int nIters, float levelGrowRatio, int nExpands, int nGrowth, int nDivs, int nFaninMax, int nTimeOut, int nMode, int nMappedMode, int nDist, int nSeed, int fVerbose) { +Abc_Ntk_t *Abc_ManRewireInt(Abc_Ntk_t *pNtk, Gia_Man_t *pExc, int nIters, float levelGrowRatio, int nExpands, int nGrowth, int nDivs, int nFaninMax, int nTimeOut, int nMode, int nMappedMode, int nDist, int nSeed, int fCheck, int fVerbose) { Random_Num(nSeed == 0 ? Abc_Random(0) % 10 : nSeed); + assert(Abc_NtkCiNum(pNtk) <= 58); int fMapped = nMode == 1; Rewire::Miaig pNtkMiaig(pNtk); - Rewire::Miaig pNew = pNtkMiaig.rewire(nIters, levelGrowRatio, nExpands, nGrowth, nDivs, nFaninMax, nTimeOut, fMapped, nMappedMode, nDist, fVerbose); + if (pExc) + pNtkMiaig.setExc(pExc); + Rewire::Miaig pNew = pNtkMiaig.rewire(nIters, levelGrowRatio, nExpands, nGrowth, nDivs, nFaninMax, nTimeOut, fMapped, nMappedMode, nDist, fCheck, fVerbose); pNew.setName(Abc_NtkName(pNtk)); if (nMode == 2) { pNew.countTransistors(1, nMappedMode); @@ -50,11 +56,14 @@ Abc_Ntk_t *Abc_ManRewireInt(Abc_Ntk_t *pNtk, int nIters, float levelGrowRatio, i return pNew.toNtk(nMode >= 1); } -Mini_Aig_t *MiniAig_ManRewireInt(Mini_Aig_t *pAig, int nIters, float levelGrowRatio, int nExpands, int nGrowth, int nDivs, int nFaninMax, int nTimeOut, int nMode, int nMappedMode, int nDist, int nSeed, int fVerbose) { +Mini_Aig_t *MiniAig_ManRewireInt(Mini_Aig_t *pAig, Gia_Man_t *pExc, int nIters, float levelGrowRatio, int nExpands, int nGrowth, int nDivs, int nFaninMax, int nTimeOut, int nMode, int nMappedMode, int nDist, int nSeed, int fCheck, int fVerbose) { Random_Num(nSeed == 0 ? Abc_Random(0) % 10 : nSeed); + assert(Mini_AigPiNum(pAig) <= 58); Rewire::Miaig pNtkMiaig(pAig); - Rewire::Miaig pNew = pNtkMiaig.rewire(nIters, levelGrowRatio, nExpands, nGrowth, nDivs, nFaninMax, nTimeOut, nMode, nMappedMode, nDist, fVerbose); + if (pExc) + pNtkMiaig.setExc(pExc); + Rewire::Miaig pNew = pNtkMiaig.rewire(nIters, levelGrowRatio, nExpands, nGrowth, nDivs, nFaninMax, nTimeOut, nMode, nMappedMode, nDist, fCheck, fVerbose); return pNew.toMiniAig(); } @@ -234,6 +243,21 @@ vi *moveVecToVi(Vec_Int_t *v) { free(v); return p; } + +void Miaig::setExc(Gia_Man_t *pExc) { + int i; + assert(Gia_ManCiNum(pExc) == nIns()); + assert(Gia_ManCoNum(pExc) == nOuts()); + if (!_data->pExc) { + _data->pExc = (word *)malloc(sizeof(word) * nWords() * nOuts()); + } + Miaig Exc(pExc); + Exc.initializeTruth(); + for (i = 0; i < nOuts(); ++i) { + word *pExc = Exc.objTruth(Exc.nObjs() - Exc.nOuts() + i, 0); + Tt_Dup(_data->pExc + nWords() * i, pExc, nWords()); + } +} #endif // RW_ABC // technology mapping @@ -753,15 +777,24 @@ void Miaig::initializeTruth(void) { Tt_Dup(objTruth(i, 2), objTruth(i, 0), nWords()); } -void Miaig::truthUpdate(vi *vTfo) { +void Miaig::truthUpdate(vi *vTfo, word *pExc, int fCheck) { int i, iTemp, nFails = 0; nTravIds()++; - Vi_ForEachEntry(vTfo, iTemp, i) { - truthSimNode(iTemp); - if (objIsPo(iTemp) && !Tt_Equal(objTruth(iTemp, 2), objTruth(iTemp, 0), nWords())) - printf("Verification failed at output %d.\n", iTemp - (nObjs() - nOuts())), nFails++; + if (!pExc) { + Vi_ForEachEntry(vTfo, iTemp, i) { + truthSimNode(iTemp); + if (fCheck && objIsPo(iTemp) && !Tt_Equal(objTruth(iTemp, 2), objTruth(iTemp, 0), nWords())) + printf("Verification failed at output %d.\n", iTemp - (nObjs() - nOuts())), nFails++; + } + } else { + Vi_ForEachEntry(vTfo, iTemp, i) { + truthSimNode(iTemp); + if (fCheck && objIsPo(iTemp) && !Tt_EqualOnCare(pExc + objPoIdx(iTemp) * nWords(), objTruth(iTemp, 2), objTruth(iTemp, 0), nWords())) { + printf("Verification failed at output %d.\n", iTemp - (nObjs() - nOuts())), nFails++; + } + } } - if (nFails) + if (fCheck && nFails) printf("Verification failed for %d outputs after updating node %d.\n", nFails, Vi_Read(vTfo, 0)); } @@ -795,15 +828,23 @@ vi *Miaig::computeTfo(int iObj) { return _data->vTfo; } -word *Miaig::computeCareSet(int iObj) { +word *Miaig::computeCareSet(int iObj, word *pExc) { vi *vTfo = computeTfo(iObj); int i, iTemp; Tt_Not(objTruth(iObj, 1), objTruth(iObj, 0), nWords()); Tt_Clear(_data->pCare, nWords()); - Vi_ForEachEntryStart(vTfo, iTemp, i, 1) { - truthSimNode(iTemp); - if (objIsPo(iTemp)) - Tt_OrXor(_data->pCare, objTruth(iTemp, 0), objTruth(iTemp, 1), nWords()); + if (!pExc) { + Vi_ForEachEntryStart(vTfo, iTemp, i, 1) { + truthSimNode(iTemp); + if (objIsPo(iTemp)) + Tt_OrXor(_data->pCare, objTruth(iTemp, 0), objTruth(iTemp, 1), nWords()); + } + } else { + Vi_ForEachEntryStart(vTfo, iTemp, i, 1) { + truthSimNode(iTemp); + if (objIsPo(iTemp)) + Tt_OrXorAnd(_data->pCare, objTruth(iTemp, 0), objTruth(iTemp, 1), pExc + objPoIdx(iTemp) * nWords(), nWords()); + } } return _data->pCare; } @@ -916,13 +957,13 @@ int Miaig::findShared(int nNewNodesMax) { return i; } -int Miaig::checkConst(int iObj, word *pCare, int fVerbose) { +int Miaig::checkConst(int iObj, word *pCare, word *pExc, int fCheck, int fVerbose) { word *pFunc = objTruth(iObj, 0); if (!Tt_IntersectC(pCare, pFunc, 0, nWords())) { derefObj_rec(iObj, -1); Vi_Fill(_data->pvFans + iObj, 1, 0); // const0 refObj(iObj); - truthUpdate(_data->vTfo); + truthUpdate(_data->vTfo, pExc, fCheck); if (fVerbose) printf("Detected Const0 at node %d.\n", iObj); return 1; } @@ -930,16 +971,16 @@ int Miaig::checkConst(int iObj, word *pCare, int fVerbose) { derefObj_rec(iObj, -1); Vi_Fill(_data->pvFans + iObj, 1, 1); // const1 refObj(iObj); - truthUpdate(_data->vTfo); + truthUpdate(_data->vTfo, pExc, fCheck); if (fVerbose) printf("Detected Const1 at node %d.\n", iObj); return 1; } return 0; } -int Miaig::expandOne(int iObj, int nAddedMax, int nDist, int nExpandableLevel, int fVerbose) { +int Miaig::expandOne(int iObj, int nAddedMax, int nDist, int nExpandableLevel, word *pExc, int fCheck, int fVerbose) { int i, k, n, iLit, nAdded = 0; - word *pCare = computeCareSet(iObj); + word *pCare = computeCareSet(iObj, pExc); assert(nAddedMax > 0); assert(nAddedMax <= Vi_Space(_data->pvFans + iObj)); // mark node's fanins @@ -986,15 +1027,15 @@ int Miaig::expandOne(int iObj, int nAddedMax, int nDist, int nExpandableLevel, i break; } //printf( "Updating TFO of node %d: ", iObj ); Vi_Print(_data->vTfo); - truthUpdate(_data->vTfo); + truthUpdate(_data->vTfo, pExc, fCheck); //assert( objFaninNum(iObj) <= nFaninMax ); return nAdded; } -int Miaig::reduceOne(int iObj, int fOnlyConst, int fOnlyBuffer, int fHeuristic, int fVerbose) { +int Miaig::reduceOne(int iObj, int fOnlyConst, int fOnlyBuffer, int fHeuristic, word *pExc, int fCheck, int fVerbose) { int n, k, iLit, nFans = objFaninNum(iObj); - word *pCare = computeCareSet(iObj); - if (checkConst(iObj, pCare, fVerbose)) + word *pCare = computeCareSet(iObj, pExc); + if (checkConst(iObj, pCare, pExc, fCheck, fVerbose)) return nFans; if (fOnlyConst) return 0; @@ -1008,7 +1049,7 @@ int Miaig::reduceOne(int iObj, int fOnlyConst, int fOnlyBuffer, int fHeuristic, derefObj(iObj); Vi_Fill(_data->pvFans + iObj, 1, iLit); refObj(iObj); - truthUpdate(_data->vTfo); + truthUpdate(_data->vTfo, pExc, fCheck); if (fVerbose) printf("Reducing node %d fanin count from %d to %d.\n", iObj, nFans, objFaninNum(iObj)); return nFans - 1; } @@ -1049,16 +1090,16 @@ int Miaig::reduceOne(int iObj, int fOnlyConst, int fOnlyBuffer, int fHeuristic, Vi_ForEachEntry(_data->vOrderF, iLit, k) Vi_PushOrder(_data->pvFans + iObj, iLit); refObj(iObj); - truthUpdate(_data->vTfo); + truthUpdate(_data->vTfo, pExc, fCheck); if (fVerbose) printf("Reducing node %d fanin count from %d to %d.\n", iObj, nFans, objFaninNum(iObj)); return nFans - Vi_Size(_data->vOrderF); } return 0; } -int Miaig::expandThenReduceOne(int iNode, int nFaninAddLimit, int nDist, int nExpandableLevel, int fVerbose) { - expandOne(iNode, Abc_MinInt(Vi_Space(_data->pvFans + iNode), nFaninAddLimit), nDist, nExpandableLevel, fVerbose); - reduceOne(iNode, 0, 0, 0, fVerbose); +int Miaig::expandThenReduceOne(int iNode, int nFaninAddLimit, int nDist, int nExpandableLevel, word *pExc, int fCheck, int fVerbose) { + expandOne(iNode, Abc_MinInt(Vi_Space(_data->pvFans + iNode), nFaninAddLimit), nDist, nExpandableLevel, pExc, fCheck, fVerbose); + reduceOne(iNode, 0, 0, 0, pExc, fCheck, fVerbose); return 0; } @@ -1071,7 +1112,7 @@ vi *Miaig::createRandomOrder(void) { return _data->vOrder; } -Miaig Miaig::expand(int nFaninAddLimitAll, int nDist, int nExpandableLevel, int fVerbose) { +Miaig Miaig::expand(int nFaninAddLimitAll, int nDist, int nExpandableLevel, word *pExc, int fCheck, int fVerbose) { int i, iNode, nAdded = 0; assert(nFaninAddLimitAll > 0); vi *vOrder = createRandomOrder(); @@ -1081,7 +1122,7 @@ Miaig Miaig::expand(int nFaninAddLimitAll, int nDist, int nExpandableLevel, int initializeLevels(); if (nDist) initializeDists(); Vi_ForEachEntry(vOrder, iNode, i) { - nAdded += expandOne(iNode, Abc_MinInt(Vi_Space(_data->pvFans + iNode), nFaninAddLimitAll - nAdded), nDist, nExpandableLevel, fVerbose); + nAdded += expandOne(iNode, Abc_MinInt(Vi_Space(_data->pvFans + iNode), nFaninAddLimitAll - nAdded), nDist, nExpandableLevel, pExc, fCheck, fVerbose); if (nAdded >= nFaninAddLimitAll) break; } @@ -1103,7 +1144,7 @@ Miaig Miaig::share(int nNewNodesMax) { return pNew; } -Miaig Miaig::reduce(int fVerbose) { +Miaig Miaig::reduce(word *pExc, int fCheck, int fVerbose) { int i, iNode; vi *vOrder = topoCollect(); @@ -1112,12 +1153,12 @@ Miaig Miaig::reduce(int fVerbose) { initializeLevels(); // works best for final Vi_ForEachEntry(vOrder, iNode, i) - reduceOne(iNode, 0, 0, 1, fVerbose); + reduceOne(iNode, 0, 0, 1, pExc, fCheck, fVerbose); verifyRefs(); return dupStrash(1, 1, 1); } -Miaig Miaig::expandThenReduce(int nFaninAddLimit, int nDist, int nExpandableLevel, int fVerbose) { +Miaig Miaig::expandThenReduce(int nFaninAddLimit, int nDist, int nExpandableLevel, word *pExc, int fCheck, int fVerbose) { Miaig pTemp; int i, iNode; vi *vOrder = topoCollect(); @@ -1127,19 +1168,19 @@ Miaig Miaig::expandThenReduce(int nFaninAddLimit, int nDist, int nExpandableLeve initializeLevels(); if (nDist) initializeDists(); Vi_ForEachEntry(vOrder, iNode, i) { - expandThenReduceOne(iNode, nFaninAddLimit, nDist, nExpandableLevel, fVerbose); + expandThenReduceOne(iNode, nFaninAddLimit, nDist, nExpandableLevel, pExc, fCheck, fVerbose); } verifyRefs(); return dupDfs().dupStrash(1, 1, 1); } -Miaig Miaig::expandShareReduce(int nFaninAddLimitAll, int nDivs, int nDist, int nExpandableLevel, int nVerbose) { +Miaig Miaig::expandShareReduce(int nFaninAddLimitAll, int nDivs, int nDist, int nExpandableLevel, word *pExc, int fCheck, int nVerbose) { // expand - Miaig pNew = expand(nFaninAddLimitAll, nDist, nExpandableLevel, nVerbose); + Miaig pNew = expand(nFaninAddLimitAll, nDist, nExpandableLevel, pExc, fCheck, nVerbose); // share pNew = pNew.share(nDivs == -1 ? pNew.nObjs() : nDivs); // reduce - pNew = pNew.reduce(nVerbose); + pNew = pNew.reduce(pExc, fCheck, nVerbose); return pNew; } @@ -1156,7 +1197,7 @@ Miaig randomRead(std::vector &pBests) { return pBests[Random_Num(0) % pBests.size()]; } -Miaig Miaig::rewire(int nIters, float levelGrowRatio, int nExpands, int nGrowth, int nDivs, int nFaninMax, int nTimeOut, int nMode, int nMappedMode, int nDist, int nVerbose) { +Miaig Miaig::rewire(int nIters, float levelGrowRatio, int nExpands, int nGrowth, int nDivs, int nFaninMax, int nTimeOut, int nMode, int nMappedMode, int nDist, int fCheck, int nVerbose) { const int nRootSave = 8; const int nBestSave = 4; int nRestart = 5000; @@ -1169,6 +1210,7 @@ Miaig Miaig::rewire(int nIters, float levelGrowRatio, int nExpands, int nGrowth, float (Miaig::*Miaig_ObjectiveFunction)(int, int) = (nMode == 0) ? &Miaig::countAnd2 : &Miaig::countTransistors; int maxLevel = levelGrowRatio != 0 ? this->countLevel() * levelGrowRatio : 0; int nExpandableLevel = maxLevel ? maxLevel - this->countLevel() : 0; + word *pExc = _data->pExc; float PrevBest = ((&pBest)->*Miaig_ObjectiveFunction)(1, nMappedMode); int iterNotImproveAfterRestart = 0; @@ -1180,9 +1222,9 @@ Miaig Miaig::rewire(int nIters, float levelGrowRatio, int nExpands, int nGrowth, pNew = pRoot.dupMulti(nFaninMax, nGrowth); if (i % 2 == 0) { - pNew = pNew.expandThenReduce(nGrowth, nDist, nExpandableLevel, nVerbose > 1); + pNew = pNew.expandThenReduce(nGrowth, nDist, nExpandableLevel, pExc, fCheck, nVerbose > 1); } - pNew = pNew.expandShareReduce(nExpands, nDivs, nDist, nExpandableLevel, nVerbose > 1); + pNew = pNew.expandShareReduce(nExpands, nDivs, nDist, nExpandableLevel, pExc, fCheck, nVerbose > 1); ++iterNotImproveAfterRestart; // report @@ -1204,7 +1246,7 @@ Miaig Miaig::rewire(int nIters, float levelGrowRatio, int nExpands, int nGrowth, } else if (rootTarget < newTarget) { if (iterNotImproveAfterRestart > nRestart) { pNew = randomRead(pBests).dupMulti(nFaninMax, nGrowth); - pNew = pNew.expand(nExpands, nDist, nExpandableLevel, nVerbose > 1); + pNew = pNew.expand(nExpands, nDist, nExpandableLevel, pExc, fCheck, nVerbose > 1); pNew = pNew.share(nDivs == -1 ? pNew.nObjs() : nDivs); pNew = pNew.dupStrash(1, 1, 0); pRoots = {pNew}; diff --git a/src/opt/rar/rewire_miaig.h b/src/opt/rar/rewire_miaig.h index 7cec02054..bdfd532fa 100644 --- a/src/opt/rar/rewire_miaig.h +++ b/src/opt/rar/rewire_miaig.h @@ -157,6 +157,7 @@ struct Miaig_Data { word *pTruths[3]; // truth tables word *pCare; // careset word *pProd; // product + word *pExc; // Exc vi *vOrder; // node order vi *vOrderF; // fanin order vi *vOrderF2; // fanin order @@ -181,6 +182,11 @@ public: Miaig(Mini_Aig_t *pMiniAig); #endif // RW_ABC +public: +#ifdef RW_ABC + void setExc(Gia_Man_t *pExc); +#endif // RW_ABC + public: void addref(void); void release(void); @@ -200,6 +206,8 @@ public: int objIsPi(int i); int objIsPo(int i); int objIsNode(int i); + int objPiIdx(int i); // No check isPi + int objPoIdx(int i); // No check isPo void print(void); int appendObj(void); void appendFanin(int i, int iLit); @@ -238,14 +246,14 @@ private: void reduceFanins(vi *v); int *createStops(void); void collectSuper_rec(int iLit, int *pStop, vi *vSuper); - int checkConst(int iObj, word *pCare, int fVerbose); + int checkConst(int iObj, word *pCare, word *pExc, int fCheck, int fVerbose); void truthSimNode(int i); word *truthSimNodeSubset(int i, int m); word *truthSimNodeSubset2(int i, vi *vFanins, int nFanins); - void truthUpdate(vi *vTfo); + void truthUpdate(vi *vTfo, word *pExc = NULL, int fCheck = 0); int computeTfo_rec(int iObj); vi *computeTfo(int iObj); - word *computeCareSet(int iObj); + word *computeCareSet(int iObj, word *pExc = NULL); vi *createRandomOrder(void); void addPair(vi *vPair, int iFan1, int iFan2); int findPair(vi *vPair); @@ -272,22 +280,22 @@ private: int buildNodeCascade(Miaig &pNew, vi *vFanins, int fCprop, int fStrash); private: - int expandOne(int iObj, int nAddedMax, int nDist, int nExpandableLevel, int fVerbose); - int reduceOne(int iObj, int fOnlyConst, int fOnlyBuffer, int fHeuristic, int fVerbose); - int expandThenReduceOne(int iNode, int nFaninAddLimit, int nDist, int nExpandableLevel, int fVerbose); + int expandOne(int iObj, int nAddedMax, int nDist, int nExpandableLevel, word *pExc, int fCheck, int fVerbose); + int reduceOne(int iObj, int fOnlyConst, int fOnlyBuffer, int fHeuristic, word *pExc, int fCheck, int fVerbose); + int expandThenReduceOne(int iNode, int nFaninAddLimit, int nDist, int nExpandableLevel, word *pExc, int fCheck, int fVerbose); public: Miaig dup(int fRemDangle, int fMapped = 0); Miaig dupDfs(void); Miaig dupStrash(int fCprop, int fStrash, int fCascade); Miaig dupMulti(int nFaninMax_, int nGrowth); - Miaig expand(int nFaninAddLimitAll, int nDist, int nExpandableLevel, int nVerbose); + Miaig expand(int nFaninAddLimitAll, int nDist, int nExpandableLevel, word *pExc, int fCheck, int nVerbose); Miaig share(int nNewNodesMax); - Miaig reduce(int fVerbose); - Miaig expandThenReduce(int nFaninAddLimit, int nDist, int nExpandableLevel, int fVerbose); - Miaig expandShareReduce(int nFaninAddLimitAll, int nDivs, int nDist, int nExpandableLevel, int nVerbose); - Miaig rewire(int nIters, float levelGrowRatio, int nExpands, int nGrowth, int nDivs, int nFaninMax, int nTimeOut, int nMode, int nMappedMode, int nDist, int nVerbose); - #ifdef RW_ABC + Miaig reduce(word *pExc, int fCheck, int fVerbose); + Miaig expandThenReduce(int nFaninAddLimit, int nDist, int nExpandableLevel, word *pExc, int fCheck, int fVerbose); + Miaig expandShareReduce(int nFaninAddLimitAll, int nDivs, int nDist, int nExpandableLevel, word *pExc, int fCheck, int nVerbose); + Miaig rewire(int nIters, float levelGrowRatio, int nExpands, int nGrowth, int nDivs, int nFaninMax, int nTimeOut, int nMode, int nMappedMode, int nDist, int fCheck, int nVerbose); +#ifdef RW_ABC Gia_Man_t *toGia(void); Abc_Ntk_t *toNtk(int fMapped = 0); Mini_Aig_t *toMiniAig(void); @@ -373,6 +381,7 @@ inline void Miaig::release(void) { free(_data->pTruths[0]); if (_data->pCare) free(_data->pCare); if (_data->pProd) free(_data->pProd); + if (_data->pExc) free(_data->pExc); if (_data->pLevel) free(_data->pLevel); if (_data->pDist) free(_data->pDist); if (_data->pTable) free(_data->pTable); @@ -413,6 +422,16 @@ inline int Miaig::objIsNode(int i) { return i > _data->nIns && i < _data->nObjs - _data->nOuts; } +inline int Miaig::objPiIdx(int i) { + // assert(objIsPi(i)); + return i - 1; +} + +inline int Miaig::objPoIdx(int i) { + // assert(objIsPo(i)); + return i - (_data->nObjs - _data->nOuts); +} + inline int Miaig::appendObj(void) { assert(_data->nObjs < _data->nObjsAlloc); return _data->nObjs++; diff --git a/src/opt/rar/rewire_rar.c b/src/opt/rar/rewire_rar.c index c9c23f6d3..d0f51e746 100644 --- a/src/opt/rar/rewire_rar.c +++ b/src/opt/rar/rewire_rar.c @@ -22,16 +22,16 @@ ABC_NAMESPACE_IMPL_START -Gia_Man_t *Gia_ManRewire(Gia_Man_t *pGia, int nIters, float levelGrowRatio, int nExpands, int nGrowth, int nDivs, int nFaninMax, int nTimeOut, int nMode, int nMappedMode, int nDist, int nSeed, int fVerbose) { - return Gia_ManRewireInt(pGia, nIters, levelGrowRatio, nExpands, nGrowth, nDivs, nFaninMax, nTimeOut, nMode, nMappedMode, nDist, nSeed, fVerbose); +Gia_Man_t *Gia_ManRewire(Gia_Man_t *pGia, Gia_Man_t *pExc, int nIters, float levelGrowRatio, int nExpands, int nGrowth, int nDivs, int nFaninMax, int nTimeOut, int nMode, int nMappedMode, int nDist, int nSeed, int fCheck, int fVerbose) { + return Gia_ManRewireInt(pGia, pExc, nIters, levelGrowRatio, nExpands, nGrowth, nDivs, nFaninMax, nTimeOut, nMode, nMappedMode, nDist, nSeed, fCheck, fVerbose); } -Abc_Ntk_t *Abc_ManRewire(Abc_Ntk_t *pNtk, int nIters, float levelGrowRatio, int nExpands, int nGrowth, int nDivs, int nFaninMax, int nTimeOut, int nMode, int nMappedMode, int nDist, int nSeed, int fVerbose) { - return Abc_ManRewireInt(pNtk, nIters, levelGrowRatio, nExpands, nGrowth, nDivs, nFaninMax, nTimeOut, nMode, nMappedMode, nDist, nSeed, fVerbose); +Abc_Ntk_t *Abc_ManRewire(Abc_Ntk_t *pNtk, Gia_Man_t *pExc, int nIters, float levelGrowRatio, int nExpands, int nGrowth, int nDivs, int nFaninMax, int nTimeOut, int nMode, int nMappedMode, int nDist, int nSeed, int fCheck, int fVerbose) { + return Abc_ManRewireInt(pNtk, pExc, nIters, levelGrowRatio, nExpands, nGrowth, nDivs, nFaninMax, nTimeOut, nMode, nMappedMode, nDist, nSeed, fCheck, fVerbose); } -Mini_Aig_t *MiniAig_ManRewire(Mini_Aig_t *pAig, int nIters, float levelGrowRatio, int nExpands, int nGrowth, int nDivs, int nFaninMax, int nTimeOut, int nMode, int nMappedMode, int nDist, int nSeed, int fVerbose) { - return MiniAig_ManRewireInt(pAig, nIters, levelGrowRatio, nExpands, nGrowth, nDivs, nFaninMax, nTimeOut, nMode, nMappedMode, nDist, nSeed, fVerbose); +Mini_Aig_t *MiniAig_ManRewire(Mini_Aig_t *pAig, Gia_Man_t *pExc, int nIters, float levelGrowRatio, int nExpands, int nGrowth, int nDivs, int nFaninMax, int nTimeOut, int nMode, int nMappedMode, int nDist, int nSeed, int fCheck, int fVerbose) { + return MiniAig_ManRewireInt(pAig, pExc, nIters, levelGrowRatio, nExpands, nGrowth, nDivs, nFaninMax, nTimeOut, nMode, nMappedMode, nDist, nSeed, fCheck, fVerbose); } ABC_NAMESPACE_IMPL_END \ No newline at end of file diff --git a/src/opt/rar/rewire_rar.h b/src/opt/rar/rewire_rar.h index dfe47712f..15a19d8c6 100644 --- a/src/opt/rar/rewire_rar.h +++ b/src/opt/rar/rewire_rar.h @@ -35,12 +35,12 @@ ABC_NAMESPACE_HEADER_START -Gia_Man_t *Gia_ManRewire(Gia_Man_t *pGia, int nIters, float levelGrowRatio, int nExpands, int nGrowth, int nDivs, int nFaninMax, int nTimeOut, int nMode, int nMappedMode, int nDist, int nSeed, int fVerbose); -Gia_Man_t *Gia_ManRewireInt(Gia_Man_t *pGia, int nIters, float levelGrowRatio, int nExpands, int nGrowth, int nDivs, int nFaninMax, int nTimeOut, int nMode, int nMappedMode, int nDist, int nSeed, int fVerbose); -Abc_Ntk_t *Abc_ManRewire(Abc_Ntk_t *pNtk, int nIters, float levelGrowRatio, int nExpands, int nGrowth, int nDivs, int nFaninMax, int nTimeOut, int nMode, int nMappedMode, int nDist, int nSeed, int fVerbose); -Abc_Ntk_t *Abc_ManRewireInt(Abc_Ntk_t *pNtk, int nIters, float levelGrowRatio, int nExpands, int nGrowth, int nDivs, int nFaninMax, int nTimeOut, int nMode, int nMappedMode, int nDist, int nSeed, int fVerbose); -Mini_Aig_t *MiniAig_ManRewire(Mini_Aig_t *pAig, int nIters, float levelGrowRatio, int nExpands, int nGrowth, int nDivs, int nFaninMax, int nTimeOut, int nMode, int nMappedMode, int nDist, int nSeed, int fVerbose); -Mini_Aig_t *MiniAig_ManRewireInt(Mini_Aig_t *pAig, int nIters, float levelGrowRatio, int nExpands, int nGrowth, int nDivs, int nFaninMax, int nTimeOut, int nMode, int nMappedMode, int nDist, int nSeed, int fVerbose); +Gia_Man_t *Gia_ManRewire(Gia_Man_t *pGia, Gia_Man_t *pExc, int nIters, float levelGrowRatio, int nExpands, int nGrowth, int nDivs, int nFaninMax, int nTimeOut, int nMode, int nMappedMode, int nDist, int nSeed, int fCheck, int fVerbose); +Gia_Man_t *Gia_ManRewireInt(Gia_Man_t *pGia, Gia_Man_t *pExc, int nIters, float levelGrowRatio, int nExpands, int nGrowth, int nDivs, int nFaninMax, int nTimeOut, int nMode, int nMappedMode, int nDist, int nSeed, int fCheck, int fVerbose); +Abc_Ntk_t *Abc_ManRewire(Abc_Ntk_t *pNtk, Gia_Man_t *pExc, int nIters, float levelGrowRatio, int nExpands, int nGrowth, int nDivs, int nFaninMax, int nTimeOut, int nMode, int nMappedMode, int nDist, int nSeed, int fCheck, int fVerbose); +Abc_Ntk_t *Abc_ManRewireInt(Abc_Ntk_t *pNtk, Gia_Man_t *pExc, int nIters, float levelGrowRatio, int nExpands, int nGrowth, int nDivs, int nFaninMax, int nTimeOut, int nMode, int nMappedMode, int nDist, int nSeed, int fCheck, int fVerbose); +Mini_Aig_t *MiniAig_ManRewire(Mini_Aig_t *pAig, Gia_Man_t *pExc, int nIters, float levelGrowRatio, int nExpands, int nGrowth, int nDivs, int nFaninMax, int nTimeOut, int nMode, int nMappedMode, int nDist, int nSeed, int fCheck, int fVerbose); +Mini_Aig_t *MiniAig_ManRewireInt(Mini_Aig_t *pAig, Gia_Man_t *pExc, int nIters, float levelGrowRatio, int nExpands, int nGrowth, int nDivs, int nFaninMax, int nTimeOut, int nMode, int nMappedMode, int nDist, int nSeed, int fCheck, int fVerbose); ABC_NAMESPACE_HEADER_END diff --git a/src/opt/rar/rewire_tt.h b/src/opt/rar/rewire_tt.h index 49fb9a0cd..ea8cc578c 100644 --- a/src/opt/rar/rewire_tt.h +++ b/src/opt/rar/rewire_tt.h @@ -152,6 +152,12 @@ static inline void Tt_OrXor(word *pOut, word *pIn1, word *pIn2, int nWords) { pOut[w] |= pIn1[w] ^ pIn2[w]; } +static inline void Tt_OrXorAnd(word *pOut, word *pIn1, word *pIn2, word *pIn3, int nWords) { + int w; + for (w = 0; w < nWords; w++) + pOut[w] |= (pIn1[w] ^ pIn2[w]) & pIn3[w]; +} + static inline int Tt_WordNum(int n) { return n > 6 ? (1 << (n - 6)) : 1; }