diff options
author | Alan Mishchenko <alanmi@berkeley.edu> | 2007-07-05 08:01:00 -0700 |
---|---|---|
committer | Alan Mishchenko <alanmi@berkeley.edu> | 2007-07-05 08:01:00 -0700 |
commit | 0c1e87bc9ae5c25278fe5715059404f3fb404809 (patch) | |
tree | b74f04be23cb1948e46e1025d3071a3976cc8551 /src | |
parent | a8db621dc96768cf2cf543be905d534579847020 (diff) | |
download | abc-0c1e87bc9ae5c25278fe5715059404f3fb404809.tar.gz abc-0c1e87bc9ae5c25278fe5715059404f3fb404809.tar.bz2 abc-0c1e87bc9ae5c25278fe5715059404f3fb404809.zip |
Version abc70705
Diffstat (limited to 'src')
-rw-r--r-- | src/base/abc/abc.h | 17 | ||||
-rw-r--r-- | src/base/abc/abcFunc.c | 28 | ||||
-rw-r--r-- | src/base/abci/abc.c | 64 | ||||
-rw-r--r-- | src/base/abci/abcDsdRes.c | 1774 | ||||
-rw-r--r-- | src/base/abci/abcIf.c | 6 | ||||
-rw-r--r-- | src/base/abci/module.make | 1 | ||||
-rw-r--r-- | src/base/io/io.c | 2 | ||||
-rw-r--r-- | src/map/if/if.h | 13 | ||||
-rw-r--r-- | src/map/if/ifMan.c | 39 | ||||
-rw-r--r-- | src/opt/kit/kit.h | 15 | ||||
-rw-r--r-- | src/opt/kit/kitDsd.c | 492 | ||||
-rw-r--r-- | src/opt/lpk/lpk.h | 82 | ||||
-rw-r--r-- | src/opt/lpk/lpkCore.c | 280 | ||||
-rw-r--r-- | src/opt/lpk/lpkCut.c | 584 | ||||
-rw-r--r-- | src/opt/lpk/lpkInt.h | 161 | ||||
-rw-r--r-- | src/opt/lpk/lpkMan.c | 96 | ||||
-rw-r--r-- | src/opt/lpk/lpkMap.c | 349 | ||||
-rw-r--r-- | src/opt/lpk/lpkMulti.c | 495 | ||||
-rw-r--r-- | src/opt/lpk/lpkMux.c | 257 | ||||
-rw-r--r-- | src/opt/lpk/lpkSets.c | 399 | ||||
-rw-r--r-- | src/opt/lpk/lpk_.c | 48 | ||||
-rw-r--r-- | src/opt/lpk/module.make | 7 |
22 files changed, 3267 insertions, 1942 deletions
diff --git a/src/base/abc/abc.h b/src/base/abc/abc.h index 3b309b43..30557259 100644 --- a/src/base/abc/abc.h +++ b/src/base/abc/abc.h @@ -227,23 +227,6 @@ struct Abc_Lib_t_ void * pGenlib; // the genlib library used to map this design }; -typedef struct Lut_Par_t_ Lut_Par_t; -struct Lut_Par_t_ -{ - // user-controlled parameters - int nLutsMax; // (N) the maximum number of LUTs in the structure - int nLutsOver; // (Q) the maximum number of LUTs not in the MFFC - int nVarsShared; // (S) the maximum number of shared variables (crossbars) - int nGrowthLevel; // (L) the maximum increase in the node level after resynthesis - int fSatur; // iterate till saturation - int fZeroCost; // accept zero-cost replacements - int fVerbose; // the verbosiness flag - int fVeryVerbose; // additional verbose info printout - // internal parameters - int nLutSize; // (K) the LUT size (determined by the input network) - int nVarsMax; // (V) the largest number of variables: V = N * (K-1) + 1 -}; - //////////////////////////////////////////////////////////////////////// /// MACRO DEFINITIONS /// //////////////////////////////////////////////////////////////////////// diff --git a/src/base/abc/abcFunc.c b/src/base/abc/abcFunc.c index 2bfad15b..f3297d8f 100644 --- a/src/base/abc/abcFunc.c +++ b/src/base/abc/abcFunc.c @@ -881,12 +881,20 @@ unsigned * Abc_ConvertAigToTruth( Hop_Man_t * p, Hop_Obj_t * pRoot, int nVars, V Hop_Obj_t * pObj; unsigned * pTruth, * pTruth2; int i, nWords, nNodes; + Vec_Ptr_t * vTtElems; + + // if the number of variables is more than 8, allocate truth tables + if ( nVars > 8 ) + vTtElems = Vec_PtrAllocTruthTables( nVars ); + else + vTtElems = NULL; + // clear the data fields and set marks nNodes = Abc_ConvertAigToTruth_rec1( pRoot ); // prepare memory nWords = Hop_TruthWordNum( nVars ); Vec_IntClear( vTruth ); - Vec_IntGrow( vTruth, nWords * nNodes ); + Vec_IntGrow( vTruth, nWords * (nNodes+1) ); pTruth = Vec_IntFetch( vTruth, nWords ); // check the case of a constant if ( Hop_ObjIsConst1( Hop_Regular(pRoot) ) ) @@ -900,21 +908,33 @@ unsigned * Abc_ConvertAigToTruth( Hop_Man_t * p, Hop_Obj_t * pRoot, int nVars, V } // set elementary truth tables at the leaves assert( nVars <= Hop_ManPiNum(p) ); - assert( Hop_ManPiNum(p) <= 8 ); +// assert( Hop_ManPiNum(p) <= 8 ); if ( fMsbFirst ) { Hop_ManForEachPi( p, pObj, i ) - pObj->pData = (void *)uTruths[nVars-1-i]; + { + if ( vTtElems ) + pObj->pData = Vec_PtrEntry(vTtElems, nVars-1-i); + else + pObj->pData = (void *)uTruths[nVars-1-i]; + } } else { Hop_ManForEachPi( p, pObj, i ) - pObj->pData = (void *)uTruths[i]; + { + if ( vTtElems ) + pObj->pData = Vec_PtrEntry(vTtElems, i); + else + pObj->pData = (void *)uTruths[i]; + } } // clear the marks and compute the truth table pTruth2 = Abc_ConvertAigToTruth_rec2( pRoot, vTruth, nWords ); // copy the result Extra_TruthCopy( pTruth, pTruth2, nVars ); + if ( vTtElems ) + Vec_PtrFree( vTtElems ); return pTruth; } diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c index d5bdd444..53566b7d 100644 --- a/src/base/abci/abc.c +++ b/src/base/abci/abc.c @@ -26,7 +26,7 @@ #include "fpga.h" #include "if.h" #include "res.h" -//#include "dar.h" +#include "lpk.h" //////////////////////////////////////////////////////////////////////// /// DECLARATIONS /// @@ -1509,23 +1509,37 @@ int Abc_CommandPrintDsd( Abc_Frame_t * pAbc, int argc, char ** argv ) FILE * pOut, * pErr; Abc_Ntk_t * pNtk; int c; - int fUseLibrary; + int fCofactor; + int nCofLevel; extern void Kit_DsdTest( unsigned * pTruth, int nVars ); + extern void Kit_DsdPrintCofactors( unsigned * pTruth, int nVars, int nCofLevel, int fVerbose ); pNtk = Abc_FrameReadNtk(pAbc); pOut = Abc_FrameReadOut(pAbc); pErr = Abc_FrameReadErr(pAbc); // set defaults - fUseLibrary = 1; + nCofLevel = 1; + fCofactor = 1; Extra_UtilGetoptReset(); - while ( ( c = Extra_UtilGetopt( argc, argv, "lh" ) ) != EOF ) + while ( ( c = Extra_UtilGetopt( argc, argv, "Nch" ) ) != EOF ) { switch ( c ) { - case 'l': - fUseLibrary ^= 1; + case 'N': + if ( globalUtilOptind >= argc ) + { + fprintf( pErr, "Command line switch \"-N\" should be followed by an integer.\n" ); + goto usage; + } + nCofLevel = atoi(argv[globalUtilOptind]); + globalUtilOptind++; + if ( nCofLevel < 0 ) + goto usage; + break; + case 'c': + fCofactor ^= 1; break; case 'h': goto usage; @@ -1549,16 +1563,16 @@ int Abc_CommandPrintDsd( Abc_Frame_t * pAbc, int argc, char ** argv ) // convert it to truth table { Abc_Obj_t * pObj = Abc_ObjFanin0( Abc_NtkPo(pNtk, 0) ); - Vec_Int_t * vMemory = Vec_IntAlloc( 10000 ); + Vec_Int_t * vMemory = Vec_IntAlloc(0); unsigned * pTruth; if ( !Abc_ObjIsNode(pObj) ) { fprintf( pErr, "The fanin of the first PO node does not have a logic function.\n" ); return 1; } - if ( Abc_ObjFaninNum(pObj) > 8 ) + if ( Abc_ObjFaninNum(pObj) > 16 ) { - fprintf( pErr, "Currently works only for up to 8 inputs.\n" ); + fprintf( pErr, "Currently works only for up to 16 inputs.\n" ); return 1; } pTruth = Abc_ConvertAigToTruth( pNtk->pManFunc, Hop_Regular(pObj->pData), Abc_ObjFaninNum(pObj), vMemory, 0 ); @@ -1566,16 +1580,20 @@ int Abc_CommandPrintDsd( Abc_Frame_t * pAbc, int argc, char ** argv ) Extra_TruthNot( pTruth, pTruth, Abc_ObjFaninNum(pObj) ); Extra_PrintBinary( stdout, pTruth, 1 << Abc_ObjFaninNum(pObj) ); printf( "\n" ); - Kit_DsdTest( pTruth, Abc_ObjFaninNum(pObj) ); + if ( fCofactor ) + Kit_DsdPrintCofactors( pTruth, Abc_ObjFaninNum(pObj), nCofLevel, 1 ); + else + Kit_DsdTest( pTruth, Abc_ObjFaninNum(pObj) ); Vec_IntFree( vMemory ); } return 0; usage: - fprintf( pErr, "usage: print_dsd [-h]\n" ); - fprintf( pErr, "\t print DSD formula for a single-output function with less than 16 variables\n" ); -// fprintf( pErr, "\t-l : used library gate names (if mapped) [default = %s]\n", fUseLibrary? "yes": "no" ); - fprintf( pErr, "\t-h : print the command usage\n"); + fprintf( pErr, "usage: print_dsd [-ch] [-N num]\n" ); + fprintf( pErr, "\t print DSD formula for a single-output function with less than 16 variables\n" ); + fprintf( pErr, "\t-c : toggle recursive cofactoring [default = %s]\n", fCofactor? "yes": "no" ); + fprintf( pErr, "\t-N num : the number of levels to cofactor [default = %d]\n", nCofLevel ); + fprintf( pErr, "\t-h : print the command usage\n"); return 1; } @@ -2906,26 +2924,22 @@ int Abc_CommandLutpack( Abc_Frame_t * pAbc, int argc, char ** argv ) { FILE * pOut, * pErr; Abc_Ntk_t * pNtk; - Lut_Par_t Pars, * pPars = &Pars; + Lpk_Par_t Pars, * pPars = &Pars; int c; - extern int Abc_LutResynthesize( Abc_Ntk_t * pNtk, Lut_Par_t * pPars ); - -// printf( "Implementation of this command is not finished.\n" ); -// return 1; - + pNtk = Abc_FrameReadNtk(pAbc); pOut = Abc_FrameReadOut(pAbc); pErr = Abc_FrameReadErr(pAbc); // set defaults - memset( pPars, 0, sizeof(Lut_Par_t) ); + memset( pPars, 0, sizeof(Lpk_Par_t) ); pPars->nLutsMax = 4; // (N) the maximum number of LUTs in the structure pPars->nLutsOver = 3; // (Q) the maximum number of LUTs not in the MFFC - pPars->nVarsShared = 3; // (S) the maximum number of shared variables (crossbars) - pPars->nGrowthLevel = 1; + pPars->nVarsShared = 0; // (S) the maximum number of shared variables (crossbars) + pPars->nGrowthLevel = 9; // (L) the maximum number of increased levels pPars->fSatur = 1; pPars->fZeroCost = 0; - pPars->fVerbose = 0; + pPars->fVerbose = 1; pPars->fVeryVerbose = 0; Extra_UtilGetoptReset(); while ( ( c = Extra_UtilGetopt( argc, argv, "NQSLszvwh" ) ) != EOF ) @@ -3007,7 +3021,7 @@ int Abc_CommandLutpack( Abc_Frame_t * pAbc, int argc, char ** argv ) } // modify the current network - if ( !Abc_LutResynthesize( pNtk, pPars ) ) + if ( !Lpk_Resynthesize( pNtk, pPars ) ) { fprintf( pErr, "Resynthesis has failed.\n" ); return 1; diff --git a/src/base/abci/abcDsdRes.c b/src/base/abci/abcDsdRes.c deleted file mode 100644 index 3aa71a15..00000000 --- a/src/base/abci/abcDsdRes.c +++ /dev/null @@ -1,1774 +0,0 @@ -/**CFile**************************************************************** - - FileName [abcDsdRes.c] - - SystemName [ABC: Logic synthesis and verification system.] - - PackageName [Network and node package.] - - Synopsis [] - - Author [Alan Mishchenko] - - Affiliation [UC Berkeley] - - Date [Ver. 1.0. Started - June 20, 2005.] - - Revision [$Id: abcDsdRes.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $] - -***********************************************************************/ - -#include "abc.h" -#include "kit.h" -#include "if.h" - -//////////////////////////////////////////////////////////////////////// -/// DECLARATIONS /// -//////////////////////////////////////////////////////////////////////// - -#define LUT_SIZE_MAX 16 // the largest size of the function -#define LUT_CUTS_MAX 1024 // the largest number of cuts considered - -typedef struct Lut_Man_t_ Lut_Man_t; -typedef struct Lut_Cut_t_ Lut_Cut_t; - -struct Lut_Cut_t_ -{ - unsigned nLeaves : 6; // (L) the number of leaves - unsigned nNodes : 6; // (M) the number of nodes - unsigned nNodesDup : 6; // (Q) nodes outside of MFFC - unsigned nLuts : 6; // (N) the number of LUTs to try - unsigned unused : 6; // unused - unsigned fHasDsd : 1; // set to 1 if the cut has structural DSD (and so cannot be used) - unsigned fMark : 1; // multipurpose mark - unsigned uSign[2]; // the signature - float Weight; // the weight of the cut: (M - Q)/N(V) (the larger the better) - int Gain; // the gain achieved using this cut - int pLeaves[LUT_SIZE_MAX]; // the leaves of the cut - int pNodes[LUT_SIZE_MAX]; // the nodes of the cut -}; - -struct Lut_Man_t_ -{ - // parameters - Lut_Par_t * pPars; // the set of parameters - // current representation - Abc_Ntk_t * pNtk; // the network - Abc_Obj_t * pObj; // the node to resynthesize - // cut representation - int nMffc; // the size of MFFC of the node - int nCuts; // the total number of cuts - int nCutsMax; // the largest possible number of cuts - int nEvals; // the number of good cuts - Lut_Cut_t pCuts[LUT_CUTS_MAX]; // the storage for cuts - int pEvals[LUT_CUTS_MAX]; // the good cuts - // visited nodes - Vec_Vec_t * vVisited; - // mapping manager - If_Man_t * pIfMan; - Vec_Int_t * vCover; - Vec_Vec_t * vLevels; - // temporary variables - int fCofactoring; // working in the cofactoring mode - int pRefs[LUT_SIZE_MAX]; // fanin reference counters - int pCands[LUT_SIZE_MAX]; // internal nodes pointing only to the leaves - // truth table representation - Vec_Ptr_t * vTtElems; // elementary truth tables - Vec_Ptr_t * vTtNodes; // storage for temporary truth tables of the nodes - // statistics - int nNodesTotal; // total number of nodes - int nNodesOver; // nodes with cuts over the limit - int nCutsTotal; // total number of cuts - int nCutsUseful; // useful cuts - int nGainTotal; // the gain in LUTs - int nChanges; // the number of changed nodes - // counter of non-DSD blocks - int nBlocks[17]; - // rutime - int timeCuts; - int timeTruth; - int timeEval; - int timeMap; - int timeOther; - int timeTotal; -}; - -#define Abc_LutCutForEachLeaf( pNtk, pCut, pObj, i ) \ - for ( i = 0; (i < (int)(pCut)->nLeaves) && (((pObj) = Abc_NtkObj(pNtk, (pCut)->pLeaves[i])), 1); i++ ) -#define Abc_LutCutForEachNode( pNtk, pCut, pObj, i ) \ - for ( i = 0; (i < (int)(pCut)->nNodes) && (((pObj) = Abc_NtkObj(pNtk, (pCut)->pNodes[i])), 1); i++ ) -#define Abc_LutCutForEachNodeReverse( pNtk, pCut, pObj, i ) \ - for ( i = (int)(pCut)->nNodes - 1; (i >= 0) && (((pObj) = Abc_NtkObj(pNtk, (pCut)->pNodes[i])), 1); i-- ) - -static inline If_Obj_t * If_Regular( If_Obj_t * p ) { return (If_Obj_t *)((unsigned long)(p) & ~01); } -static inline If_Obj_t * If_Not( If_Obj_t * p ) { return (If_Obj_t *)((unsigned long)(p) ^ 01); } -static inline If_Obj_t * If_NotCond( If_Obj_t * p, int c ) { return (If_Obj_t *)((unsigned long)(p) ^ (c)); } -static inline int If_IsComplement( If_Obj_t * p ) { return (int )(((unsigned long)p) & 01); } - -extern void Res_UpdateNetworkLevel( Abc_Obj_t * pObjNew, Vec_Vec_t * vLevels ); - -static If_Obj_t * Abc_LutIfManMapMulti( Lut_Man_t * p, unsigned * pTruth, int nLeaves, If_Obj_t ** ppLeaves ); - -//////////////////////////////////////////////////////////////////////// -/// FUNCTION DEFINITIONS /// -//////////////////////////////////////////////////////////////////////// - -/**Function************************************************************* - - Synopsis [] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -Lut_Man_t * Abc_LutManStart( Lut_Par_t * pPars ) -{ - Lut_Man_t * p; - assert( pPars->nLutsMax <= 16 ); - assert( pPars->nVarsMax > 0 ); - p = ALLOC( Lut_Man_t, 1 ); - memset( p, 0, sizeof(Lut_Man_t) ); - p->pPars = pPars; - p->nCutsMax = LUT_CUTS_MAX; - p->vTtElems = Vec_PtrAllocTruthTables( pPars->nVarsMax ); - p->vTtNodes = Vec_PtrAllocSimInfo( 256, Abc_TruthWordNum(pPars->nVarsMax) ); - p->vCover = Vec_IntAlloc( 1 << 12 ); - return p; -} - -/**Function************************************************************* - - Synopsis [] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Abc_LutManStop( Lut_Man_t * p ) -{ - if ( p->pIfMan ) - { - void * pPars = p->pIfMan->pPars; - If_ManStop( p->pIfMan ); - free( pPars ); - } - if ( p->vLevels ) - Vec_VecFree( p->vLevels ); - if ( p->vVisited ) - Vec_VecFree( p->vVisited ); - Vec_IntFree( p->vCover ); - Vec_PtrFree( p->vTtElems ); - Vec_PtrFree( p->vTtNodes ); - free( p ); -} - -/**Function************************************************************* - - Synopsis [Returns 1 if at least one entry has changed.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -int Abc_LutNodeHasChanged( Lut_Man_t * p, int iNode ) -{ - Vec_Ptr_t * vNodes; - Abc_Obj_t * pTemp; - int i; - vNodes = Vec_VecEntry( p->vVisited, iNode ); - if ( Vec_PtrSize(vNodes) == 0 ) - return 1; - Vec_PtrForEachEntry( vNodes, pTemp, i ) - { - // check if the node has changed - pTemp = Abc_NtkObj( p->pNtk, (int)pTemp ); - if ( pTemp == NULL ) - return 1; - // check if the number of fanouts has changed -// if ( Abc_ObjFanoutNum(pTemp) != (int)Vec_PtrEntry(vNodes, i+1) ) -// return 1; - i++; - } - return 0; -} - -/**Function************************************************************* - - Synopsis [Returns 1 if at least one entry has changed.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Abc_LutNodeRecordImpact( Lut_Man_t * p ) -{ - Lut_Cut_t * pCut; - Vec_Ptr_t * vNodes = Vec_VecEntry( p->vVisited, p->pObj->Id ); - Abc_Obj_t * pNode; - int i, k; - // collect the nodes that impact the given node - Vec_PtrClear( vNodes ); - for ( i = 0; i < p->nCuts; i++ ) - { - pCut = p->pCuts + i; - for ( k = 0; k < (int)pCut->nLeaves; k++ ) - { - pNode = Abc_NtkObj( p->pNtk, pCut->pLeaves[k] ); - if ( pNode->fMarkC ) - continue; - pNode->fMarkC = 1; - Vec_PtrPush( vNodes, (void *)pNode->Id ); - Vec_PtrPush( vNodes, (void *)Abc_ObjFanoutNum(pNode) ); - } - } - // clear the marks - Vec_PtrForEachEntry( vNodes, pNode, i ) - { - pNode = Abc_NtkObj( p->pNtk, (int)pNode ); - pNode->fMarkC = 0; - i++; - } -//printf( "%d ", Vec_PtrSize(vNodes) ); -} - -/**Function************************************************************* - - Synopsis [Returns 1 if the cut has structural DSD.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -int Abc_LutNodeCutsCheckDsd( Lut_Man_t * p, Lut_Cut_t * pCut ) -{ - Abc_Obj_t * pObj, * pFanin; - int i, k, nCands, fLeavesOnly, RetValue; - assert( pCut->nLeaves > 0 ); - // clear ref counters - memset( p->pRefs, 0, sizeof(int) * pCut->nLeaves ); - // mark cut leaves - Abc_LutCutForEachLeaf( p->pNtk, pCut, pObj, i ) - { - assert( pObj->fMarkA == 0 ); - pObj->fMarkA = 1; - pObj->pCopy = (void *)i; - } - // ref leaves pointed from the internal nodes - nCands = 0; - Abc_LutCutForEachNode( p->pNtk, pCut, pObj, i ) - { - fLeavesOnly = 1; - Abc_ObjForEachFanin( pObj, pFanin, k ) - if ( pFanin->fMarkA ) - p->pRefs[(int)pFanin->pCopy]++; - else - fLeavesOnly = 0; - if ( fLeavesOnly ) - p->pCands[nCands++] = pObj->Id; - } - // look at the nodes that only point to the leaves - RetValue = 0; - for ( i = 0; i < nCands; i++ ) - { - pObj = Abc_NtkObj( p->pNtk, p->pCands[i] ); - Abc_ObjForEachFanin( pObj, pFanin, k ) - { - assert( pFanin->fMarkA == 1 ); - if ( p->pRefs[(int)pFanin->pCopy] > 1 ) - break; - } - if ( k == Abc_ObjFaninNum(pObj) ) - { - RetValue = 1; - break; - } - } - // unmark cut leaves - Abc_LutCutForEachLeaf( p->pNtk, pCut, pObj, i ) - pObj->fMarkA = 0; - return RetValue; -} - -/**Function************************************************************* - - Synopsis [Returns 1 if pDom is contained in pCut.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -static inline int Abc_LutNodeCutsOneDominance( Lut_Cut_t * pDom, Lut_Cut_t * pCut ) -{ - int i, k; - for ( i = 0; i < (int)pDom->nLeaves; i++ ) - { - for ( k = 0; k < (int)pCut->nLeaves; k++ ) - if ( pDom->pLeaves[i] == pCut->pLeaves[k] ) - break; - if ( k == (int)pCut->nLeaves ) // node i in pDom is not contained in pCut - return 0; - } - // every node in pDom is contained in pCut - return 1; -} - -/**Function************************************************************* - - Synopsis [Check if the cut exists.] - - Description [Returns 1 if the cut exists.] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -int Abc_LutNodeCutsOneFilter( Lut_Cut_t * pCuts, int nCuts, Lut_Cut_t * pCutNew ) -{ - Lut_Cut_t * pCut; - int i, k; - assert( pCutNew->uSign[0] || pCutNew->uSign[1] ); - // try to find the cut - for ( i = 0; i < nCuts; i++ ) - { - pCut = pCuts + i; - if ( pCut->nLeaves == 0 ) - continue; - if ( pCut->nLeaves == pCutNew->nLeaves ) - { - if ( pCut->uSign[0] == pCutNew->uSign[0] && pCut->uSign[1] == pCutNew->uSign[1] ) - { - for ( k = 0; k < (int)pCutNew->nLeaves; k++ ) - if ( pCut->pLeaves[k] != pCutNew->pLeaves[k] ) - break; - if ( k == (int)pCutNew->nLeaves ) - return 1; - } - continue; - } - if ( pCut->nLeaves < pCutNew->nLeaves ) - { - // skip the non-contained cuts - if ( (pCut->uSign[0] & pCutNew->uSign[0]) != pCut->uSign[0] ) - continue; - if ( (pCut->uSign[1] & pCutNew->uSign[1]) != pCut->uSign[1] ) - continue; - // check containment seriously - if ( Abc_LutNodeCutsOneDominance( pCut, pCutNew ) ) - return 1; - continue; - } - // check potential containment of other cut - - // skip the non-contained cuts - if ( (pCut->uSign[0] & pCutNew->uSign[0]) != pCutNew->uSign[0] ) - continue; - if ( (pCut->uSign[1] & pCutNew->uSign[1]) != pCutNew->uSign[1] ) - continue; - // check containment seriously - if ( Abc_LutNodeCutsOneDominance( pCutNew, pCut ) ) - pCut->nLeaves = 0; // removed - } - return 0; -} - -/**Function************************************************************* - - Synopsis [Prints the given cut.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Abc_LutNodePrintCut( Lut_Man_t * p, Lut_Cut_t * pCut ) -{ - Abc_Obj_t * pObj; - int i; - printf( "LEAVES:\n" ); - Abc_LutCutForEachLeaf( p->pNtk, pCut, pObj, i ) - { - Abc_ObjPrint( stdout, pObj ); - } - printf( "NODES:\n" ); - Abc_LutCutForEachNode( p->pNtk, pCut, pObj, i ) - { - Abc_ObjPrint( stdout, pObj ); - assert( Abc_ObjIsNode(pObj) ); - } - printf( "\n" ); -} - -/**Function************************************************************* - - Synopsis [Set the cut signature.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Abc_LutNodeCutSignature( Lut_Cut_t * pCut ) -{ - unsigned i; - pCut->uSign[0] = pCut->uSign[1] = 0; - for ( i = 0; i < pCut->nLeaves; i++ ) - { - pCut->uSign[(pCut->pLeaves[i] & 32) > 0] |= (1 << (pCut->pLeaves[i] & 31)); - if ( i != pCut->nLeaves - 1 ) - assert( pCut->pLeaves[i] < pCut->pLeaves[i+1] ); - } -} - - -/**Function************************************************************* - - Synopsis [Computes the set of all cuts.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Abc_LutNodeCutsOne( Lut_Man_t * p, Lut_Cut_t * pCut, int Node ) -{ - Lut_Cut_t * pCutNew; - Abc_Obj_t * pObj, * pFanin; - int i, k, j, nLeavesNew; - - // check if the cut can stand adding one more internal node - if ( pCut->nNodes == LUT_SIZE_MAX ) - return; - - // if the node is a PI, quit - pObj = Abc_NtkObj( p->pNtk, Node ); - if ( Abc_ObjIsCi(pObj) ) - return; - assert( Abc_ObjIsNode(pObj) ); - assert( Abc_ObjFaninNum(pObj) <= p->pPars->nLutSize ); - - // if the node is not in the MFFC, check the limit - if ( !Abc_NodeIsTravIdCurrent(pObj) ) - { - if ( (int)pCut->nNodesDup == p->pPars->nLutsOver ) - return; - assert( (int)pCut->nNodesDup < p->pPars->nLutsOver ); - } - - // check the possibility of adding this node using the signature - nLeavesNew = pCut->nLeaves - 1; - Abc_ObjForEachFanin( pObj, pFanin, i ) - { - if ( (pCut->uSign[(pFanin->Id & 32) > 0] & (1 << (pFanin->Id & 31))) ) - continue; - if ( ++nLeavesNew > p->pPars->nVarsMax ) - return; - } - - // initialize the set of leaves to the nodes in the cut - assert( p->nCuts < LUT_CUTS_MAX ); - pCutNew = p->pCuts + p->nCuts; -/* -if ( p->pObj->Id == 31 && Node == 38 && pCut->pNodes[0] == 31 && pCut->pNodes[1] == 34 && pCut->pNodes[2] == 35 )//p->nCuts == 48 ) -{ - int x = 0; - printf( "Start:\n" ); - Abc_LutNodePrintCut( p, pCut ); -} -*/ - pCutNew->nLeaves = 0; - for ( i = 0; i < (int)pCut->nLeaves; i++ ) - if ( pCut->pLeaves[i] != Node ) - pCutNew->pLeaves[pCutNew->nLeaves++] = pCut->pLeaves[i]; - - // add new nodes - Abc_ObjForEachFanin( pObj, pFanin, i ) - { - // find the place where this node belongs - for ( k = 0; k < (int)pCutNew->nLeaves; k++ ) - if ( pCutNew->pLeaves[k] >= pFanin->Id ) - break; - if ( k < (int)pCutNew->nLeaves && pCutNew->pLeaves[k] == pFanin->Id ) - continue; - // check if there is room - if ( (int)pCutNew->nLeaves == p->pPars->nVarsMax ) - return; - // move all the nodes - for ( j = pCutNew->nLeaves; j > k; j-- ) - pCutNew->pLeaves[j] = pCutNew->pLeaves[j-1]; - pCutNew->pLeaves[k] = pFanin->Id; - pCutNew->nLeaves++; - assert( pCutNew->nLeaves <= LUT_SIZE_MAX ); - } - - // skip the contained cuts - Abc_LutNodeCutSignature( pCutNew ); - if ( Abc_LutNodeCutsOneFilter( p->pCuts, p->nCuts, pCutNew ) ) - return; - - // update the set of internal nodes - assert( pCut->nNodes < LUT_SIZE_MAX ); - memcpy( pCutNew->pNodes, pCut->pNodes, pCut->nNodes * sizeof(int) ); - pCutNew->nNodes = pCut->nNodes; - pCutNew->pNodes[ pCutNew->nNodes++ ] = Node; - - // add the marked node - pCutNew->nNodesDup = pCut->nNodesDup + !Abc_NodeIsTravIdCurrent(pObj); -/* -if ( p->pObj->Id == 31 && Node == 38 )//p->nCuts == 48 ) -{ - int x = 0; - printf( "Finish:\n" ); - Abc_LutNodePrintCut( p, pCutNew ); -} -*/ - // add the cut to storage - assert( p->nCuts < LUT_CUTS_MAX ); - p->nCuts++; - - assert( pCut->nNodes <= p->nMffc + pCutNew->nNodesDup ); -} - -/**Function************************************************************* - - Synopsis [Computes the set of all cuts.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -int Abc_LutNodeCuts( Lut_Man_t * p ) -{ - Lut_Cut_t * pCut, * pCut2; - int i, k, Temp, nMffc, fChanges; - - // mark the MFFC of the node with the current trav ID - nMffc = p->nMffc = Abc_NodeMffcLabel( p->pObj ); - assert( nMffc > 0 ); - if ( nMffc == 1 ) - return 0; - - // initialize the first cut - pCut = p->pCuts; p->nCuts = 1; - pCut->nNodes = 0; - pCut->nNodesDup = 0; - pCut->nLeaves = 1; - pCut->pLeaves[0] = p->pObj->Id; - // assign the signature - Abc_LutNodeCutSignature( pCut ); - - // perform the cut computation - for ( i = 0; i < p->nCuts; i++ ) - { - pCut = p->pCuts + i; - if ( pCut->nLeaves == 0 ) - continue; - // try to expand the fanins of this cut - for ( k = 0; k < (int)pCut->nLeaves; k++ ) - { - // create a new cut - Abc_LutNodeCutsOne( p, pCut, pCut->pLeaves[k] ); - // quit if the number of cuts has exceeded the limit - if ( p->nCuts == LUT_CUTS_MAX ) - break; - } - if ( p->nCuts == LUT_CUTS_MAX ) - break; - } - if ( p->nCuts == LUT_CUTS_MAX ) - p->nNodesOver++; - - // record the impact of this node - if ( p->pPars->fSatur ) - Abc_LutNodeRecordImpact( p ); - - // compress the cuts by removing empty ones, those with negative Weight, and decomposable ones - p->nEvals = 0; - for ( i = 0; i < p->nCuts; i++ ) - { - pCut = p->pCuts + i; - if ( pCut->nLeaves < 2 ) - continue; - // compute the number of LUTs neede to implement this cut - // V = N * (K-1) + 1 ~~~~~ N = Ceiling[(V-1)/(K-1)] = (V-1)/(K-1) + [(V-1)%(K-1) > 0] - pCut->nLuts = (pCut->nLeaves-1)/(p->pPars->nLutSize-1) + ( (pCut->nLeaves-1)%(p->pPars->nLutSize-1) > 0 ); - pCut->Weight = (float)1.0 * (pCut->nNodes - pCut->nNodesDup) / pCut->nLuts; //p->pPars->nLutsMax; - if ( pCut->Weight <= 1.0 ) - continue; - pCut->fHasDsd = Abc_LutNodeCutsCheckDsd( p, pCut ); - if ( pCut->fHasDsd ) - continue; - p->pEvals[p->nEvals++] = i; - } - if ( p->nEvals == 0 ) - return 0; - - // sort the cuts by Weight - do { - fChanges = 0; - for ( i = 0; i < p->nEvals - 1; i++ ) - { - pCut = p->pCuts + p->pEvals[i]; - pCut2 = p->pCuts + p->pEvals[i+1]; - if ( pCut->Weight >= pCut2->Weight ) - continue; - Temp = p->pEvals[i]; - p->pEvals[i] = p->pEvals[i+1]; - p->pEvals[i+1] = Temp; - fChanges = 1; - } - } while ( fChanges ); - return 1; -} - -/**Function************************************************************* - - Synopsis [Computes the truth able of one cut.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -unsigned * Abc_LutCutTruth_rec( Hop_Man_t * pMan, Hop_Obj_t * pObj, int nVars, Vec_Ptr_t * vTtNodes, int * iCount ) -{ - unsigned * pTruth, * pTruth0, * pTruth1; - assert( !Hop_IsComplement(pObj) ); - if ( pObj->pData ) - { - assert( ((unsigned)pObj->pData) & 0xffff0000 ); - return pObj->pData; - } - // get the plan for a new truth table - pTruth = Vec_PtrEntry( vTtNodes, (*iCount)++ ); - if ( Hop_ObjIsConst1(pObj) ) - Extra_TruthFill( pTruth, nVars ); - else - { - assert( Hop_ObjIsAnd(pObj) ); - // compute the truth tables of the fanins - pTruth0 = Abc_LutCutTruth_rec( pMan, Hop_ObjFanin0(pObj), nVars, vTtNodes, iCount ); - pTruth1 = Abc_LutCutTruth_rec( pMan, Hop_ObjFanin1(pObj), nVars, vTtNodes, iCount ); - // creat the truth table of the node - Extra_TruthAndPhase( pTruth, pTruth0, pTruth1, nVars, Hop_ObjFaninC0(pObj), Hop_ObjFaninC1(pObj) ); - } - pObj->pData = pTruth; - return pTruth; -} - -/**Function************************************************************* - - Synopsis [Computes the truth able of one cut.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -unsigned * Abc_LutCutTruth( Lut_Man_t * p, Lut_Cut_t * pCut ) -{ - Hop_Man_t * pManHop = p->pNtk->pManFunc; - Hop_Obj_t * pObjHop; - Abc_Obj_t * pObj, * pFanin; - unsigned * pTruth; - int i, k, iCount = 0; -// Abc_LutNodePrintCut( p, pCut ); - - // initialize the leaves - Abc_LutCutForEachLeaf( p->pNtk, pCut, pObj, i ) - pObj->pCopy = Vec_PtrEntry( p->vTtElems, i ); - - // construct truth table in the topological order - Abc_LutCutForEachNodeReverse( p->pNtk, pCut, pObj, i ) - { - // get the local AIG - pObjHop = Hop_Regular(pObj->pData); - // clean the data field of the nodes in the AIG subgraph - Hop_ObjCleanData_rec( pObjHop ); - // set the initial truth tables at the fanins - Abc_ObjForEachFanin( pObj, pFanin, k ) - { - assert( ((unsigned)pFanin->pCopy) & 0xffff0000 ); - Hop_ManPi( pManHop, k )->pData = pFanin->pCopy; - } - // compute the truth table of internal nodes - pTruth = Abc_LutCutTruth_rec( pManHop, pObjHop, pCut->nLeaves, p->vTtNodes, &iCount ); - if ( Hop_IsComplement(pObj->pData) ) - Extra_TruthNot( pTruth, pTruth, pCut->nLeaves ); - // set the truth table at the node - pObj->pCopy = (Abc_Obj_t *)pTruth; - } - - return pTruth; -} - - - -/**Function************************************************************* - - Synopsis [Prepares the mapping manager.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Abc_LutIfManStart( Lut_Man_t * p ) -{ - If_Par_t * pPars; - assert( p->pIfMan == NULL ); - // set defaults - pPars = ALLOC( If_Par_t, 1 ); - memset( pPars, 0, sizeof(If_Par_t) ); - // user-controlable paramters - pPars->nLutSize = p->pPars->nLutSize; - pPars->nCutsMax = 8; - pPars->nFlowIters = 0; // 1 - pPars->nAreaIters = 0; // 1 - pPars->DelayTarget = -1; - pPars->fPreprocess = 0; - pPars->fArea = 1; - pPars->fFancy = 0; - pPars->fExpRed = 0; // - pPars->fLatchPaths = 0; - pPars->fSeqMap = 0; - pPars->fVerbose = 0; - // internal parameters - pPars->fTruth = 0; - pPars->fUsePerm = 0; - pPars->nLatches = 0; - pPars->pLutLib = NULL; // Abc_FrameReadLibLut(); - pPars->pTimesArr = NULL; - pPars->pTimesArr = NULL; - pPars->fUseBdds = 0; - pPars->fUseSops = 0; - pPars->fUseCnfs = 0; - pPars->fUseMv = 0; - // start the mapping manager and set its parameters - p->pIfMan = If_ManStart( pPars ); - If_ManSetupSetAll( p->pIfMan, 1000 ); - p->pIfMan->pPars->pTimesArr = ALLOC( float, 32 ); -} - -/**Function************************************************************* - - Synopsis [Transforms the decomposition graph into the AIG.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -If_Obj_t * Abc_LutIfManMapPrimeInternal( If_Man_t * pIfMan, Kit_Graph_t * pGraph ) -{ - Kit_Node_t * pNode; - If_Obj_t * pAnd0, * pAnd1; - int i; - // check for constant function - if ( Kit_GraphIsConst(pGraph) ) - return If_ManConst1(pIfMan); - // check for a literal - if ( Kit_GraphIsVar(pGraph) ) - return Kit_GraphVar(pGraph)->pFunc; - // build the AIG nodes corresponding to the AND gates of the graph - Kit_GraphForEachNode( pGraph, pNode, i ) - { - pAnd0 = Kit_GraphNode(pGraph, pNode->eEdge0.Node)->pFunc; - pAnd1 = Kit_GraphNode(pGraph, pNode->eEdge1.Node)->pFunc; - pNode->pFunc = If_ManCreateAnd( pIfMan, - If_Regular(pAnd0), If_IsComplement(pAnd0) ^ pNode->eEdge0.fCompl, - If_Regular(pAnd1), If_IsComplement(pAnd1) ^ pNode->eEdge1.fCompl ); - } - return pNode->pFunc; -} - -/**Function************************************************************* - - Synopsis [Strashes one logic node using its SOP.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -If_Obj_t * Abc_LutIfManMapPrime( If_Man_t * pIfMan, If_Obj_t ** ppLeaves, Kit_Graph_t * pGraph ) -{ - Kit_Node_t * pNode; - If_Obj_t * pRes; - int i; - // collect the fanins - Kit_GraphForEachLeaf( pGraph, pNode, i ) - pNode->pFunc = ppLeaves[i]; - // perform strashing - pRes = Abc_LutIfManMapPrimeInternal( pIfMan, pGraph ); - return If_NotCond( pRes, Kit_GraphIsComplement(pGraph) ); -} - -/**Function************************************************************* - - Synopsis [Creates the choice node for the given number.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -If_Obj_t * Abc_LutIfManChoiceOne( If_Man_t * pIfMan, If_Obj_t ** pNodes, int iNode, int nLeaves, int fXor ) -{ - If_Obj_t * pPrev, * pAnd, * pOne, * pMany; - int v; - pPrev = NULL; - for ( v = 0; v < nLeaves; v++ ) - { - if ( (iNode & (1 << v)) == 0 ) - continue; - pOne = pNodes[1 << v]; - pMany = pNodes[iNode & ~(1 << v)]; - if ( fXor ) - pAnd = If_ManCreateXnor( pIfMan, If_Regular(pOne), pMany ); - else - pAnd = If_ManCreateAnd( pIfMan, If_Regular(pOne), If_IsComplement(pOne), If_Regular(pMany), If_IsComplement(pMany) ); - pAnd->pEquiv = pPrev; - pPrev = pAnd; - } - return pPrev; -} - -/**Function************************************************************* - - Synopsis [Creates the choice node for the given number.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -If_Obj_t * Abc_LutIfManChoice( If_Man_t * pIfMan, If_Obj_t ** pLeaves, int nLeaves, int fXor ) -{ - If_Obj_t ** pNodes, * pRes; - int v, m, nMints; - // allocate room for nodes - assert( nLeaves >= 2 ); - nMints = (1 << nLeaves); - pNodes = ALLOC( If_Obj_t *, nMints ); - // set elementary ones - pNodes[0] = NULL; - for ( v = 0; v < nLeaves; v++ ) - pNodes[1<<v] = pLeaves[v]; - // set triples and so on - for ( v = 2; v <= nLeaves; v++ ) - for ( m = 0; m < nMints; m++ ) - if ( Kit_WordCountOnes(m) == v ) - { - pNodes[m] = Abc_LutIfManChoiceOne( pIfMan, pNodes, m, nLeaves, fXor ); - if ( v > 2 ) - If_ManCreateChoice( pIfMan, pNodes[m] ); - } - pRes = pNodes[nMints-1]; - free( pNodes ); - return pRes; -} - -/**Function************************************************************* - - Synopsis [Creates the choice node for the given number.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -If_Obj_t * Abc_LutIfManPart_rec( If_Man_t * pIfMan, If_Obj_t ** pLeaves, int nLeaves, int fXor ) -{ - If_Obj_t * pObjNew1, * pObjNew2; - if ( nLeaves <= 5 ) - return Abc_LutIfManChoice( pIfMan, pLeaves, nLeaves, fXor ); - pObjNew1 = Abc_LutIfManPart_rec( pIfMan, pLeaves, nLeaves / 2, fXor ); - pObjNew2 = Abc_LutIfManPart_rec( pIfMan, pLeaves + nLeaves / 2, nLeaves - (nLeaves / 2), fXor ); - if ( fXor ) - return If_ManCreateXnor( pIfMan, pObjNew1, pObjNew2 ); - else - return If_ManCreateAnd( pIfMan, pObjNew1, 0, pObjNew2, 0 ); -} - -/**Function************************************************************* - - Synopsis [Prepares the mapping manager.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -If_Obj_t * Abc_LutIfManMap_New_rec( Lut_Man_t * p, Kit_DsdNtk_t * pNtk, int iLit ) -{ - Kit_Graph_t * pGraph; - Kit_DsdObj_t * pObj; - If_Obj_t * pObjNew, * pFansNew[16]; - unsigned i, iLitFanin, fCompl; - - // remember the complement - fCompl = Kit_DsdLitIsCompl(iLit); - iLit = Kit_DsdLitRegular(iLit); - assert( !Kit_DsdLitIsCompl(iLit) ); - - // consider the case of simple gate - pObj = Kit_DsdNtkObj( pNtk, Kit_DsdLit2Var(iLit) ); - if ( pObj == NULL ) - { - pObjNew = If_ManCi( p->pIfMan, Kit_DsdLit2Var(iLit) ); - return If_NotCond( pObjNew, fCompl ); - } - - // solve for the inputs - Kit_DsdObjForEachFanin( pNtk, pObj, iLitFanin, i ) - pFansNew[i] = Abc_LutIfManMap_New_rec( p, pNtk, iLitFanin ); - - // generate choices for multi-input gate - if ( pObj->Type == KIT_DSD_AND || pObj->Type == KIT_DSD_XOR ) - { - assert( pObj->nFans >= 2 ); - if ( pObj->Type == KIT_DSD_XOR ) - { - fCompl ^= ((pObj->nFans-1) & 1); // flip if the number of operations is odd - for ( i = 0; i < pObj->nFans; i++ ) - { - fCompl ^= If_IsComplement(pFansNew[i]); - pFansNew[i] = If_Regular(pFansNew[i]); - } - } - pObjNew = Abc_LutIfManPart_rec( p->pIfMan, pFansNew, pObj->nFans, pObj->Type == KIT_DSD_XOR ); - return If_NotCond( pObjNew, fCompl ); - } - assert( pObj->Type == KIT_DSD_PRIME ); - - // derive the factored form - pGraph = Kit_TruthToGraph( Kit_DsdObjTruth(pObj), pObj->nFans, p->vCover ); - // convert factored form into the AIG - pObjNew = Abc_LutIfManMapPrime( p->pIfMan, pFansNew, pGraph ); - Kit_GraphFree( pGraph ); - return If_NotCond( pObjNew, fCompl ); -} - -/**Function************************************************************* - - Synopsis [Find the best cofactoring variable.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -int Abc_LutFindBestCofactoring( Lut_Man_t * p, Kit_DsdNtk_t * pNtk, unsigned * pTruth, int nVars ) -{ - Kit_DsdNtk_t * pNtk0, * pNtk1;//, * pTemp; - unsigned * pCofs2[3] = { pNtk->pMem, pNtk->pMem + Kit_TruthWordNum(pNtk->nVars), pNtk->pMem + 2 * Kit_TruthWordNum(pNtk->nVars) }; - int i, MaxBlock0, MaxBlock1, MaxBlockBest = 1000, VarBest = -1; - int fVerbose = 1; - - if ( fVerbose ) - { -// printf( "Function: " ); -// Extra_PrintBinary( stdout, pTruth, (1 << nVars) ); -// Extra_PrintHexadecimal( stdout, pTruth, nVars ); - printf( "\n" ); - printf( "\n" ); - printf( "V =%2d: ", pNtk->nVars ); - Kit_DsdPrint( stdout, pNtk ); - } - for ( i = 0; i < nVars; i++ ) - { - Kit_TruthCofactor0New( pCofs2[0], pTruth, nVars, i ); - Kit_TruthCofactor1New( pCofs2[1], pTruth, nVars, i ); - Kit_TruthXor( pCofs2[2], pCofs2[0], pCofs2[1], nVars ); - - pNtk0 = Kit_DsdDecompose( pCofs2[0], nVars ); - MaxBlock0 = Kit_DsdNonDsdSizeMax( pNtk0 ); -// pNtk0 = Kit_DsdExpand( pTemp = pNtk0 ); -// Kit_DsdNtkFree( pTemp ); - if ( fVerbose ) - { - printf( "Variable %2d: Diff = %6d.\n", i, Kit_TruthCountOnes(pCofs2[2], nVars) ); - - printf( "Cof%d0: ", i ); - Kit_DsdPrint( stdout, pNtk0 ); - } - - pNtk1 = Kit_DsdDecompose( pCofs2[1], nVars ); - MaxBlock1 = Kit_DsdNonDsdSizeMax( pNtk1 ); -// pNtk1 = Kit_DsdExpand( pTemp = pNtk1 ); -// Kit_DsdNtkFree( pTemp ); - if ( fVerbose ) - { - printf( "Cof%d1: ", i ); - Kit_DsdPrint( stdout, pNtk1 ); - } - - if ( fVerbose ) - { - printf( "MaxBlock0 = %2d. MaxBlock1 = %2d. ", MaxBlock0, MaxBlock1 ); - if ( MaxBlock0 < p->pPars->nLutSize && MaxBlock1 < p->pPars->nLutSize ) - printf( " feasible\n" ); - else - printf( "infeasible\n" ); - } - - if ( MaxBlock0 < p->pPars->nLutSize && MaxBlock1 < p->pPars->nLutSize ) - { - if ( MaxBlockBest > ABC_MAX(MaxBlock0, MaxBlock1) ) - { - MaxBlockBest = ABC_MAX(MaxBlock0, MaxBlock1); - VarBest = i; - } - } - - Kit_DsdNtkFree( pNtk0 ); - Kit_DsdNtkFree( pNtk1 ); - } - if ( fVerbose ) - { - printf( "Best variable = %d.\n", VarBest ); - printf( "\n" ); - } - return VarBest; - -} - -/**Function************************************************************* - - Synopsis [Prepares the mapping manager.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -If_Obj_t * Abc_LutIfManMap_rec( Lut_Man_t * p, Kit_DsdNtk_t * pNtk, int iLit, If_Obj_t * pResult ) -{ - Kit_Graph_t * pGraph; - Kit_DsdObj_t * pObj; - If_Obj_t * pObjNew, * pFansNew[16]; - unsigned i, iLitFanin, fCompl; - - // remember the complement - fCompl = Kit_DsdLitIsCompl(iLit); - iLit = Kit_DsdLitRegular(iLit); - assert( !Kit_DsdLitIsCompl(iLit) ); - - // consider the case of simple gate - pObj = Kit_DsdNtkObj( pNtk, Kit_DsdLit2Var(iLit) ); - if ( pObj == NULL ) - { - pObjNew = If_ManCi( p->pIfMan, Kit_DsdLit2Var(iLit) ); - return If_NotCond( pObjNew, fCompl ); - } - if ( pObj->Type == KIT_DSD_AND ) - { - assert( pObj->nFans == 2 ); - pFansNew[0] = pResult? pResult : Abc_LutIfManMap_rec( p, pNtk, pObj->pFans[0], NULL ); - pFansNew[1] = Abc_LutIfManMap_rec( p, pNtk, pObj->pFans[1], NULL ); - if ( pFansNew[0] == NULL || pFansNew[1] == NULL ) - return NULL; - pObjNew = If_ManCreateAnd( p->pIfMan, If_Regular(pFansNew[0]), If_IsComplement(pFansNew[0]), If_Regular(pFansNew[1]), If_IsComplement(pFansNew[1]) ); - return If_NotCond( pObjNew, fCompl ); - } - if ( pObj->Type == KIT_DSD_XOR ) - { - assert( pObj->nFans == 2 ); - pFansNew[0] = pResult? pResult : Abc_LutIfManMap_rec( p, pNtk, pObj->pFans[0], NULL ); - pFansNew[1] = Abc_LutIfManMap_rec( p, pNtk, pObj->pFans[1], NULL ); - if ( pFansNew[0] == NULL || pFansNew[1] == NULL ) - return NULL; - fCompl ^= 1 ^ If_IsComplement(pFansNew[0]) ^ If_IsComplement(pFansNew[1]); - pObjNew = If_ManCreateXnor( p->pIfMan, If_Regular(pFansNew[0]), If_Regular(pFansNew[1]) ); - return If_NotCond( pObjNew, fCompl ); - } - assert( pObj->Type == KIT_DSD_PRIME ); - p->nBlocks[pObj->nFans]++; - - // solve for the inputs - Kit_DsdObjForEachFanin( pNtk, pObj, iLitFanin, i ) - { - if ( i == 0 ) - pFansNew[i] = pResult? pResult : Abc_LutIfManMap_rec( p, pNtk, iLitFanin, NULL ); - else - pFansNew[i] = Abc_LutIfManMap_rec( p, pNtk, iLitFanin, NULL ); - if ( pFansNew[i] == NULL ) - return NULL; - } - - // find best cofactoring variable -// if ( pObj->nFans > 3 ) -// Kit_DsdCofactoring( Kit_DsdObjTruth(pObj), pObj->nFans, NULL, 4, 1 ); - if ( !p->fCofactoring && p->pPars->nVarsShared > 0 && (int)pObj->nFans > p->pPars->nLutSize ) -// return Abc_LutIfManMapMulti( p, Kit_DsdObjTruth(pObj), pObj->nFans, pFansNew ); - Abc_LutIfManMapMulti( p, Kit_DsdObjTruth(pObj), pObj->nFans, pFansNew ); - - - // derive the factored form - pGraph = Kit_TruthToGraph( Kit_DsdObjTruth(pObj), pObj->nFans, p->vCover ); - if ( pGraph == NULL ) - return NULL; - // convert factored form into the AIG - pObjNew = Abc_LutIfManMapPrime( p->pIfMan, pFansNew, pGraph ); - Kit_GraphFree( pGraph ); - return If_NotCond( pObjNew, fCompl ); -} - -/**Function************************************************************* - - Synopsis [Prepares the mapping manager.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -int Abc_LutCutUpdate( Lut_Man_t * p, Lut_Cut_t * pCut, Kit_DsdNtk_t * pNtk ) -{ - extern Abc_Obj_t * Abc_NodeFromIf_rec( Abc_Ntk_t * pNtkNew, If_Man_t * pIfMan, If_Obj_t * pIfObj, Vec_Int_t * vCover ); - Kit_DsdObj_t * pRoot; - If_Obj_t * pDriver; - Abc_Obj_t * pLeaf, * pObjNew; - int nGain, i; - - // check special cases - pRoot = Kit_DsdNtkRoot( pNtk ); - if ( pRoot->Type == KIT_DSD_CONST1 ) - { - pObjNew = Abc_NtkCreateNodeConst1( p->pNtk ); - pObjNew = Abc_ObjNotCond( pObjNew, Kit_DsdLitIsCompl(pNtk->Root) ); - - // perform replacement - pObjNew->Level = p->pObj->Level; - Abc_ObjReplace( p->pObj, pObjNew ); - Res_UpdateNetworkLevel( pObjNew, p->vLevels ); - p->nGainTotal += pCut->nNodes - pCut->nNodesDup; - return 1; - } - if ( pRoot->Type == KIT_DSD_VAR ) - { - pObjNew = Abc_NtkObj( p->pNtk, pCut->pLeaves[ Kit_DsdLit2Var(pRoot->pFans[0]) ] ); - pObjNew = Abc_ObjNotCond( pObjNew, Kit_DsdLitIsCompl(pNtk->Root) ^ Kit_DsdLitIsCompl(pRoot->pFans[0]) ); - - // perform replacement - pObjNew->Level = p->pObj->Level; - Abc_ObjReplace( p->pObj, pObjNew ); - Res_UpdateNetworkLevel( pObjNew, p->vLevels ); - p->nGainTotal += pCut->nNodes - pCut->nNodesDup; - return 1; - } - assert( pRoot->Type == KIT_DSD_AND || pRoot->Type == KIT_DSD_XOR || pRoot->Type == KIT_DSD_PRIME ); - - // start the mapping manager - if ( p->pIfMan == NULL ) - Abc_LutIfManStart( p ); - - // prepare the mapping manager - If_ManRestart( p->pIfMan ); - // create the PI variables - for ( i = 0; i < p->pPars->nVarsMax; i++ ) - If_ManCreateCi( p->pIfMan ); - // set the arrival times - Abc_LutCutForEachLeaf( p->pNtk, pCut, pLeaf, i ) - p->pIfMan->pPars->pTimesArr[i] = (float)pLeaf->Level; - // prepare the PI cuts - If_ManSetupCiCutSets( p->pIfMan ); - // create the internal nodes -// pDriver = Abc_LutIfManMap_New_rec( p, pNtk, pNtk->Root ); - pDriver = Abc_LutIfManMap_rec( p, pNtk, pNtk->Root, NULL ); - if ( pDriver == NULL ) - return 0; - // create the PO node - If_ManCreateCo( p->pIfMan, If_Regular(pDriver), 0 ); - - // perform mapping - p->pIfMan->pPars->fAreaOnly = 1; - If_ManPerformMappingComb( p->pIfMan ); - - // compute the gain in area - nGain = pCut->nNodes - pCut->nNodesDup - (int)p->pIfMan->AreaGlo; - if ( p->pPars->fVeryVerbose ) - printf( " Mffc = %2d. Mapped = %2d. Gain = %3d. Depth increase = %d.\n", - pCut->nNodes - pCut->nNodesDup, (int)p->pIfMan->AreaGlo, nGain, (int)p->pIfMan->RequiredGlo - (int)p->pObj->Level ); - - // quit if there is no gain - if ( !(nGain > 0 || (p->pPars->fZeroCost && nGain == 0)) ) - return 0; - // quit if depth increases too much - if ( (int)p->pIfMan->RequiredGlo - (int)p->pObj->Level > p->pPars->nGrowthLevel ) - return 0; - - // perform replacement - p->nGainTotal += nGain; - p->nChanges++; - - // prepare the mapping manager - If_ManCleanNodeCopy( p->pIfMan ); - If_ManCleanCutData( p->pIfMan ); - // set the PIs of the cut - Abc_LutCutForEachLeaf( p->pNtk, pCut, pLeaf, i ) - If_ObjSetCopy( If_ManCi(p->pIfMan, i), pLeaf ); - // get the area of mapping - pObjNew = Abc_NodeFromIf_rec( p->pNtk, p->pIfMan, If_Regular(pDriver), p->vCover ); - pObjNew->pData = Hop_NotCond( pObjNew->pData, If_IsComplement(pDriver) ); - - // perform replacement - pObjNew->Level = p->pObj->Level; - Abc_ObjReplace( p->pObj, pObjNew ); - Res_UpdateNetworkLevel( pObjNew, p->vLevels ); - return 1; -} - - - -/**Function************************************************************* - - Synopsis [Performs resynthesis for one node.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -int Abc_LutResynthesizeNode( Lut_Man_t * p ) -{ - extern void Kit_DsdTest( unsigned * pTruth, int nVars ); - extern int Kit_DsdEval( unsigned * pTruth, int nVars, int nLutSize ); - - Kit_DsdNtk_t * pDsdNtk; - Lut_Cut_t * pCut; - unsigned * pTruth; - void * pDsd = NULL; -// int Result, Gain; - int i, RetValue, clk; - - // compute the cuts -clk = clock(); - if ( !Abc_LutNodeCuts( p ) ) - { -p->timeCuts += clock() - clk; - return 0; - } -p->timeCuts += clock() - clk; - - if ( p->pPars->fVeryVerbose ) - printf( "Node %5d : Mffc size = %5d. Cuts = %5d.\n", p->pObj->Id, p->nMffc, p->nEvals ); - // try the good cuts - p->nCutsTotal += p->nCuts; - p->nCutsUseful += p->nEvals; - for ( i = 0; i < p->nEvals; i++ ) - { - // get the cut - pCut = p->pCuts + p->pEvals[i]; - - // compute the truth table -clk = clock(); - pTruth = Abc_LutCutTruth( p, pCut ); -p->timeTruth += clock() - clk; - - -/* - // evaluate the result of decomposition - Result = Kit_DsdEval( pTruth, pCut->nLeaves, 3 ); - // calculate expected gain - Gain = (Result < 0) ? -1 : pCut->nNodes - pCut->nNodesDup - Result; - if ( !(Gain < 0 || (Gain == 0 && p->pPars->fZeroCost)) ) - continue; -*/ - -clk = clock(); -// Kit_DsdTest( pTruth, pCut->nLeaves ); - pDsdNtk = Kit_DsdDeriveNtk( pTruth, pCut->nLeaves, p->pPars->nLutSize ); -p->timeEval += clock() - clk; - - if ( Kit_DsdNtkRoot(pDsdNtk)->nFans == 16 ) // skip 16-input non-DSD because ISOP will not work - { - Kit_DsdNtkFree( pDsdNtk ); - continue; - } -/* - // skip large non-DSD blocks - if ( Kit_DsdNonDsdSizeMax(pDsdNtk) > 7 ) - { - Kit_DsdNtkFree( pDsdNtk ); - continue; - } -*/ - -/* - if ( pCut->nLeaves > 6 && pCut->nLeaves < 12 && Kit_DsdNonDsdSizeMax(pDsdNtk) == pCut->nLeaves ) - { -// Abc_NtkPrintMeasures( pTruth, pCut->nLeaves ); -// Kit_DsdTestCofs( pDsdNtk, pTruth ); - -// Abc_NtkPrintOneDecomp( pTruth, pCut->nLeaves ); - Abc_NtkPrintOneDec( pTruth, pCut->nLeaves ); - } -*/ - - if ( p->pPars->fVeryVerbose ) - { -// Extra_PrintHexadecimal( stdout, pTruth, pCut->nLeaves ); printf( "\n" ); -// printf( " Cut %2d : L = %2d. S = %2d. Vol = %2d. Q = %d. N = %d. W = %4.2f. New = %2d. Gain = %2d.\n", -// i, pCut->nLeaves, Extra_TruthSupportSize(pTruth, pCut->nLeaves), pCut->nNodes, pCut->nNodesDup, pCut->nLuts, pCut->Weight, Result, Gain ); - printf( " C%02d: L= %2d/%2d V= %2d/%d N= %d W= %4.2f ", - i, pCut->nLeaves, Extra_TruthSupportSize(pTruth, pCut->nLeaves), pCut->nNodes, pCut->nNodesDup, pCut->nLuts, pCut->Weight ); - Kit_DsdPrint( stdout, pDsdNtk ); - } - - // update the network -clk = clock(); - RetValue = Abc_LutCutUpdate( p, pCut, pDsdNtk ); - Kit_DsdNtkFree( pDsdNtk ); -p->timeMap += clock() - clk; - if ( RetValue ) - break; - } - return 1; -} - - -/**Function************************************************************* - - Synopsis [Performs resynthesis for one network.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -int Abc_LutResynthesize( Abc_Ntk_t * pNtk, Lut_Par_t * pPars ) -{ - ProgressBar * pProgress; - Lut_Man_t * p; - Abc_Obj_t * pObj; - double Delta; - int i, Iter, nNodes, nNodesPrev, clk = clock(); - assert( Abc_NtkIsLogic(pNtk) ); - - // get the number of inputs - pPars->nLutSize = Abc_NtkGetFaninMax( pNtk ); - pPars->nVarsMax = pPars->nLutsMax * (pPars->nLutSize - 1) + 1; // V = N * (K-1) + 1 - if ( pPars->fVerbose ) - { - printf( "Resynthesis for %d %d-LUTs with %d non-MFFC LUTs, %d crossbars, and %d-input cuts.\n", - pPars->nLutsMax, pPars->nLutSize, pPars->nLutsOver, pPars->nVarsShared, pPars->nVarsMax ); - } - if ( pPars->nVarsMax > 16 ) - { - printf( "Currently cannot handle resynthesis with more than %d inputs (reduce \"-N <num>\").\n", 16 ); - return 1; - } - - // convert logic to AIGs - Abc_NtkToAig( pNtk ); - - // start the manager - p = Abc_LutManStart( pPars ); - p->pNtk = pNtk; - p->nNodesTotal = Abc_NtkNodeNum(pNtk); - p->vLevels = Vec_VecStart( 3 * Abc_NtkLevel(pNtk) ); // computes levels of all nodes - if ( p->pPars->fSatur ) - p->vVisited = Vec_VecStart( 0 ); - - // iterate over the network - nNodesPrev = p->nNodesTotal; - for ( Iter = 1; ; Iter++ ) - { - // expand storage for changed nodes - if ( p->pPars->fSatur ) - Vec_VecExpand( p->vVisited, Abc_NtkObjNumMax(pNtk) + 1 ); - - // consider all nodes - nNodes = Abc_NtkObjNumMax(pNtk); - if ( !pPars->fVeryVerbose ) - pProgress = Extra_ProgressBarStart( stdout, nNodes ); - Abc_NtkForEachNode( pNtk, pObj, i ) - { - if ( i >= nNodes ) - break; - if ( !pPars->fVeryVerbose ) - Extra_ProgressBarUpdate( pProgress, i, NULL ); - // skip the nodes that did not change - if ( p->pPars->fSatur && !Abc_LutNodeHasChanged(p, pObj->Id) ) - continue; - // resynthesize - p->pObj = pObj; - Abc_LutResynthesizeNode( p ); - } - if ( !pPars->fVeryVerbose ) - Extra_ProgressBarStop( pProgress ); - - // check the increase - Delta = 100.00 * (nNodesPrev - Abc_NtkNodeNum(pNtk)) / p->nNodesTotal; - if ( Delta < 0.05 ) - break; - nNodesPrev = Abc_NtkNodeNum(pNtk); - if ( !p->pPars->fSatur ) - break; - } - - if ( pPars->fVerbose ) - { - printf( "N = %5d (%3d) Cut = %5d (%4d) Change = %5d Gain = %5d (%5.2f %%) Iter = %2d\n", - p->nNodesTotal, p->nNodesOver, p->nCutsTotal, p->nCutsUseful, p->nChanges, p->nGainTotal, 100.0 * p->nGainTotal / p->nNodesTotal, Iter ); - printf( "Non_DSD blocks: " ); - for ( i = 3; i <= pPars->nVarsMax; i++ ) - if ( p->nBlocks[i] ) - printf( "%d=%d ", i, p->nBlocks[i] ); - printf( "\n" ); - p->timeTotal = clock() - clk; - p->timeOther = p->timeTotal - p->timeCuts - p->timeTruth - p->timeEval - p->timeMap; - PRTP( "Cuts ", p->timeCuts, p->timeTotal ); - PRTP( "Truth ", p->timeTruth, p->timeTotal ); - PRTP( "Eval ", p->timeEval, p->timeTotal ); - PRTP( "Map ", p->timeMap, p->timeTotal ); - PRTP( "Other ", p->timeOther, p->timeTotal ); - PRTP( "TOTAL ", p->timeTotal, p->timeTotal ); - } - - Abc_LutManStop( p ); - // check the resulting network - if ( !Abc_NtkCheck( pNtk ) ) - { - printf( "Abc_LutResynthesize: The network check has failed.\n" ); - return 0; - } - return 1; -} - - - - - - -/**Function************************************************************* - - Synopsis [Records variable order.] - - Description [Increaments Order[x][y] by 1 if x should be above y in the DSD.] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Abc_LutCreateVarOrder( Kit_DsdNtk_t * pNtk, char pTable[][16] ) -{ - Kit_DsdObj_t * pObj; - unsigned uSuppFanins, k; - int Above[16], Below[16]; - int nAbove, nBelow, iFaninLit, i, x, y; - // iterate through the nodes - Kit_DsdNtkForEachObj( pNtk, pObj, i ) - { - // collect fanin support of this node - nAbove = 0; - uSuppFanins = 0; - Kit_DsdObjForEachFanin( pNtk, pObj, iFaninLit, k ) - { - if ( Kit_DsdLitIsLeaf( pNtk, iFaninLit ) ) - Above[nAbove++] = Kit_DsdLit2Var(iFaninLit); - else - uSuppFanins |= Kit_DsdLitSupport( pNtk, iFaninLit ); - } - // find the below variables - nBelow = 0; - for ( y = 0; y < 16; y++ ) - if ( uSuppFanins & (1 << y) ) - Below[nBelow++] = y; - // create all pairs - for ( x = 0; x < nAbove; x++ ) - for ( y = 0; y < nBelow; y++ ) - pTable[Above[x]][Below[y]]++; - } -} - -/**Function************************************************************* - - Synopsis [Creates commmon variable order.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Abc_LutCreateCommonOrder( char pTable[][16], int pOrder[], int nLeaves ) -{ - int Score[16] = {0}; - int i, y, x; - // compute scores for each leaf - for ( i = 0; i < nLeaves; i++ ) - { - for ( y = 0; y < nLeaves; y++ ) - Score[i] += pTable[i][y]; - for ( x = 0; x < nLeaves; x++ ) - Score[i] -= pTable[x][i]; - } -/* - printf( "Scores: " ); - for ( i = 0; i < nLeaves; i++ ) - printf( "%d ", Score[i] ); - printf( "\n" ); -*/ - // sort the scores - Extra_BubbleSort( pOrder, Score, nLeaves, 0 ); -/* - printf( "Scores: " ); - for ( i = 0; i < nLeaves; i++ ) - printf( "%d ", Score[pOrder[i]] ); - printf( "\n" ); -*/ -} - -/**Function************************************************************* - - Synopsis [Prepares the mapping manager.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -If_Obj_t * Abc_LutIfManMapMulti_rec( Lut_Man_t * p, Kit_DsdNtk_t ** ppNtks, int * piLits, int * piCofVar, int nCBars, If_Obj_t ** ppLeaves, int nLeaves, int * pOrder ) -{ - Kit_DsdObj_t * pObj; - If_Obj_t * pObjsNew[4][8], * pResPrev; - unsigned uSupps[8], uSuppFanin; - int piLitsNew[8], pDecision[8] = {0}; - int i, v, k, nSize = (1 << nCBars); - - // find which of the variables is highest in the order - - // go though non-trivial components - for ( i = 0; i < nSize; i++ ) - { - if ( piLits[i] == -1 ) - continue; - pObj = Kit_DsdNtkObj( ppNtks[i], Kit_DsdLit2Var(piLits[i]) ); - uSuppFanin = pObj? Kit_DsdLitSupport( ppNtks[i], pObj->pFans[0] ) : 0; - uSupps[i] = Kit_DsdLitSupport( ppNtks[i], piLits[i] ) & ~uSuppFanin; - } - // find the variable that appears the highest in the order - for ( v = 0; v < nLeaves; v++ ) - { - for ( i = 0; i < nSize; i++ ) - if ( uSupps[i] & (1 << pOrder[v]) ) - break; - } - assert( v < nLeaves ); - // pull out all components that have this variable - for ( i = 0; i < nSize; i++ ) - pDecision[i] = ( uSupps[i] & (1 << pOrder[v]) ); - - - // iterate over the nodes - for ( i = 0; i < nSize; i++ ) - { - pObj = Kit_DsdNtkObj( ppNtks[i], Kit_DsdLit2Var(piLits[i]) ); - if ( pDecision[i] ) - piLitsNew[i] = pObj->pFans[0]; - else - piLitsNew[i] = piLits[i]; - } - - // call again - pResPrev = Abc_LutIfManMapMulti_rec( p, ppNtks, piLitsNew, piCofVar, nCBars, ppLeaves, nLeaves, pOrder ); - - // create new set of nodes - for ( i = 0; i < nSize; i++ ) - { - if ( pDecision[i] ) - pObjsNew[nCBars][i] = Abc_LutIfManMap_rec( p, ppNtks[i], piLits[i], pResPrev ); - else - pObjsNew[nCBars][i] = pResPrev; - } - - // create MUX using these outputs - for ( k = nCBars; k > 0; k-- ) - { - nSize /= 2; - for ( i = 0; i < nSize; i++ ) - pObjsNew[k-1][i] = If_ManCreateMnux( p->pIfMan, pObjsNew[k][2*i+0], pObjsNew[k][2*i+1], ppLeaves[piCofVar[k-1]] ); - } - assert( nCBars == 1 && nSize == 1 ); - return If_NotCond( pObjsNew[0][0], nCBars & 1 ); -} - -/**Function************************************************************* - - Synopsis [Prepares the mapping manager.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -If_Obj_t * Abc_LutIfManMapMulti( Lut_Man_t * p, unsigned * pTruth, int nVars, If_Obj_t ** ppLeaves ) -{ - If_Obj_t * pResult; - Kit_DsdNtk_t * ppNtks[8] = {0}, * pTemp; - int piCofVar[4], pOrder[16] = {0}, pPrios[16], pFreqs[16] = {0}, piLits[16]; - int i, k, nCBars, nSize, nMemSize; - unsigned * ppCofs[4][8], uSupport; - char pTable[16][16] = {0}; - int fVerbose = 1; - - // allocate storage for cofactors - nMemSize = Kit_TruthWordNum(nVars); - ppCofs[0][0] = ALLOC( unsigned, 32 * nMemSize ); - nSize = 0; - for ( i = 0; i < 4; i++ ) - for ( k = 0; k < 8; k++ ) - ppCofs[i][k] = ppCofs[0][0] + nMemSize * nSize++; - assert( nSize == 32 ); - - // find the best cofactoring variables - nCBars = Kit_DsdCofactoring( pTruth, nVars, piCofVar, p->pPars->nVarsShared, 0 ); - - // copy the function - Kit_TruthCopy( ppCofs[0][0], pTruth, nVars ); - - // decompose w.r.t. these variables - for ( k = 0; k < nCBars; k++ ) - { - nSize = (1 << k); - for ( i = 0; i < nSize; i++ ) - { - Kit_TruthCofactor0New( ppCofs[k+1][2*i+0], ppCofs[k][i], nVars, piCofVar[k] ); - Kit_TruthCofactor1New( ppCofs[k+1][2*i+1], ppCofs[k][i], nVars, piCofVar[k] ); - } - } - nSize = (1 << nCBars); - // compute variable frequences - for ( i = 0; i < nSize; i++ ) - { - uSupport = Kit_TruthSupport( ppCofs[nCBars][i], nVars ); - for ( k = 0; k < nVars; k++ ) - if ( uSupport & (1<<k) ) - pFreqs[k]++; - } - // compute DSD networks - for ( i = 0; i < nSize; i++ ) - { - ppNtks[i] = Kit_DsdDecompose( ppCofs[nCBars][i], nVars ); - ppNtks[i] = Kit_DsdExpand( pTemp = ppNtks[i] ); - Kit_DsdNtkFree( pTemp ); - if ( fVerbose ) - { - printf( "Cof%d%d: ", nCBars, i ); - Kit_DsdPrint( stdout, ppNtks[i] ); - } - } - free( ppCofs[0][0] ); - - // find common variable order - for ( i = 0; i < nSize; i++ ) - { - Kit_DsdGetSupports( ppNtks[i] ); - Abc_LutCreateVarOrder( ppNtks[i], pTable ); - } - Abc_LutCreateCommonOrder( pTable, pOrder, nVars ); - - printf( "Common variable order: " ); - for ( i = 0; i < nVars; i++ ) - printf( "%c ", 'a' + pOrder[i] ); - printf( "\n" ); - - // derive variable priority - for ( i = 0; i < 16; i++ ) - pPrios[i] = 16; - for ( i = 0; i < nVars; i++ ) - pPrios[pOrder[i]] = i; - - // transform all networks according to the variable order - for ( i = 0; i < nSize; i++ ) - { - ppNtks[i] = Kit_DsdShrink( pTemp = ppNtks[i], pPrios ); - Kit_DsdNtkFree( pTemp ); - Kit_DsdGetSupports( ppNtks[i] ); - // undec nodes should be rotated in such a way that the first input has as many shared inputs as possible - Kit_DsdRotate( ppNtks[i], pFreqs ); - // collect the roots - piLits[i] = ppNtks[i]->Root; - } -/* - p->fCofactoring = 1; - pResult = Abc_LutIfManMapMulti_rec( p, ppNtks[nCBars], piLits, piCofVar, nCBars, ppLeaves, nVars, pOrder ); - p->fCofactoring = 0; -*/ - // free the networks - for ( i = 0; i < 8; i++ ) - if ( ppNtks[i] ) - Kit_DsdNtkFree( ppNtks[i] ); - - return pResult; -} - -//////////////////////////////////////////////////////////////////////// -/// END OF FILE /// -//////////////////////////////////////////////////////////////////////// - - diff --git a/src/base/abci/abcIf.c b/src/base/abci/abcIf.c index b8c4a6c0..074b8ae8 100644 --- a/src/base/abci/abcIf.c +++ b/src/base/abci/abcIf.c @@ -145,8 +145,8 @@ If_Man_t * Abc_NtkToIf( Abc_Ntk_t * pNtk, If_Par_t * pPars ) Extra_ProgressBarUpdate( pProgress, i, "Initial" ); // add the node to the mapper pNode->pCopy = (Abc_Obj_t *)If_ManCreateAnd( pIfMan, - (If_Obj_t *)Abc_ObjFanin0(pNode)->pCopy, Abc_ObjFaninC0(pNode), - (If_Obj_t *)Abc_ObjFanin1(pNode)->pCopy, Abc_ObjFaninC1(pNode) ); + If_NotCond( (If_Obj_t *)Abc_ObjFanin0(pNode)->pCopy, Abc_ObjFaninC0(pNode) ), + If_NotCond( (If_Obj_t *)Abc_ObjFanin1(pNode)->pCopy, Abc_ObjFaninC1(pNode) ) ); // set up the choice node if ( Abc_AigNodeIsChoice( pNode ) ) { @@ -162,7 +162,7 @@ If_Man_t * Abc_NtkToIf( Abc_Ntk_t * pNtk, If_Par_t * pPars ) // set the primary outputs without copying the phase Abc_NtkForEachCo( pNtk, pNode, i ) - If_ManCreateCo( pIfMan, (If_Obj_t *)Abc_ObjFanin0(pNode)->pCopy, Abc_ObjFaninC0(pNode) ); + If_ManCreateCo( pIfMan, If_NotCond( (If_Obj_t *)Abc_ObjFanin0(pNode)->pCopy, Abc_ObjFaninC0(pNode) ) ); return pIfMan; } diff --git a/src/base/abci/module.make b/src/base/abci/module.make index 9bc51dbe..f6c73102 100644 --- a/src/base/abci/module.make +++ b/src/base/abci/module.make @@ -11,7 +11,6 @@ SRC += src/base/abci/abc.c \ src/base/abci/abcDebug.c \ src/base/abci/abcDress.c \ src/base/abci/abcDsd.c \ - src/base/abci/abcDsdRes.c \ src/base/abci/abcEspresso.c \ src/base/abci/abcExtract.c \ src/base/abci/abcFpga.c \ diff --git a/src/base/io/io.c b/src/base/io/io.c index e1d4de97..20caeb57 100644 --- a/src/base/io/io.c +++ b/src/base/io/io.c @@ -715,7 +715,7 @@ int IoCommandReadTruth( Abc_Frame_t * pAbc, int argc, char ** argv ) int fHex; int c; - fHex = 0; + fHex = 1; Extra_UtilGetoptReset(); while ( ( c = Extra_UtilGetopt( argc, argv, "xh" ) ) != EOF ) { diff --git a/src/map/if/if.h b/src/map/if/if.h index a5aa3356..706f8552 100644 --- a/src/map/if/if.h +++ b/src/map/if/if.h @@ -212,6 +212,11 @@ struct If_Obj_t_ If_Cut_t CutBest; // the best cut selected }; +static inline If_Obj_t * If_Regular( If_Obj_t * p ) { return (If_Obj_t *)((unsigned long)(p) & ~01); } +static inline If_Obj_t * If_Not( If_Obj_t * p ) { return (If_Obj_t *)((unsigned long)(p) ^ 01); } +static inline If_Obj_t * If_NotCond( If_Obj_t * p, int c ) { return (If_Obj_t *)((unsigned long)(p) ^ (c)); } +static inline int If_IsComplement( If_Obj_t * p ) { return (int )(((unsigned long)p) & 01); } + static inline int If_ManCiNum( If_Man_t * p ) { return p->nObjs[IF_CI]; } static inline int If_ManCoNum( If_Man_t * p ) { return p->nObjs[IF_CO]; } static inline int If_ManAndNum( If_Man_t * p ) { return p->nObjs[IF_AND]; } @@ -334,10 +339,10 @@ extern If_Man_t * If_ManStart( If_Par_t * pPars ); extern void If_ManRestart( If_Man_t * p ); extern void If_ManStop( If_Man_t * p ); extern If_Obj_t * If_ManCreateCi( If_Man_t * p ); -extern If_Obj_t * If_ManCreateCo( If_Man_t * p, If_Obj_t * pDriver, int fCompl0 ); -extern If_Obj_t * If_ManCreateAnd( If_Man_t * p, If_Obj_t * pFan0, int fCompl0, If_Obj_t * pFan1, int fCompl1 ); -extern If_Obj_t * If_ManCreateXnor( If_Man_t * p, If_Obj_t * pFan0, If_Obj_t * pFan1 ); -extern If_Obj_t * If_ManCreateMnux( If_Man_t * p, If_Obj_t * pFan0, If_Obj_t * pFan1, If_Obj_t * pCtrl ); +extern If_Obj_t * If_ManCreateCo( If_Man_t * p, If_Obj_t * pDriver ); +extern If_Obj_t * If_ManCreateAnd( If_Man_t * p, If_Obj_t * pFan0, If_Obj_t * pFan1 ); +extern If_Obj_t * If_ManCreateXor( If_Man_t * p, If_Obj_t * pFan0, If_Obj_t * pFan1 ); +extern If_Obj_t * If_ManCreateMux( If_Man_t * p, If_Obj_t * pFan0, If_Obj_t * pFan1, If_Obj_t * pCtrl ); extern void If_ManCreateChoice( If_Man_t * p, If_Obj_t * pRepr ); extern void If_ManSetupCutTriv( If_Man_t * p, If_Cut_t * pCut, int ObjId ); extern void If_ManSetupCiCutSets( If_Man_t * p ); diff --git a/src/map/if/ifMan.c b/src/map/if/ifMan.c index 923dd7d5..14267f8e 100644 --- a/src/map/if/ifMan.c +++ b/src/map/if/ifMan.c @@ -175,13 +175,13 @@ If_Obj_t * If_ManCreateCi( If_Man_t * p ) SeeAlso [] ***********************************************************************/ -If_Obj_t * If_ManCreateCo( If_Man_t * p, If_Obj_t * pDriver, int fCompl0 ) +If_Obj_t * If_ManCreateCo( If_Man_t * p, If_Obj_t * pDriver ) { If_Obj_t * pObj; pObj = If_ManSetupObj( p ); - pObj->Type = IF_CO; - pObj->fCompl0 = fCompl0; Vec_PtrPush( p->vCos, pObj ); + pObj->Type = IF_CO; + pObj->fCompl0 = If_IsComplement(pDriver); pDriver = If_Regular(pDriver); pObj->pFanin0 = pDriver; pDriver->nRefs++; p->nObjs[IF_CO]++; return pObj; @@ -198,17 +198,26 @@ If_Obj_t * If_ManCreateCo( If_Man_t * p, If_Obj_t * pDriver, int fCompl0 ) SeeAlso [] ***********************************************************************/ -If_Obj_t * If_ManCreateAnd( If_Man_t * p, If_Obj_t * pFan0, int fCompl0, If_Obj_t * pFan1, int fCompl1 ) +If_Obj_t * If_ManCreateAnd( If_Man_t * p, If_Obj_t * pFan0, If_Obj_t * pFan1 ) { If_Obj_t * pObj; + // perform constant propagation + if ( pFan0 == pFan1 ) + return pFan0; + if ( pFan0 == If_Not(pFan1) ) + return If_Not(p->pConst1); + if ( If_Regular(pFan0) == p->pConst1 ) + return pFan0 == p->pConst1 ? pFan1 : If_Not(p->pConst1); + if ( If_Regular(pFan1) == p->pConst1 ) + return pFan1 == p->pConst1 ? pFan0 : If_Not(p->pConst1); // get memory for the new object pObj = If_ManSetupObj( p ); pObj->Type = IF_AND; - pObj->fCompl0 = fCompl0; - pObj->fCompl1 = fCompl1; + pObj->fCompl0 = If_IsComplement(pFan0); pFan0 = If_Regular(pFan0); + pObj->fCompl1 = If_IsComplement(pFan1); pFan1 = If_Regular(pFan1); pObj->pFanin0 = pFan0; pFan0->nRefs++; pFan0->nVisits++; pFan0->nVisitsCopy++; pObj->pFanin1 = pFan1; pFan1->nRefs++; pFan1->nVisits++; pFan1->nVisitsCopy++; - pObj->fPhase = (fCompl0 ^ pFan0->fPhase) & (fCompl1 ^ pFan1->fPhase); + pObj->fPhase = (pObj->fCompl0 ^ pFan0->fPhase) & (pObj->fCompl1 ^ pFan1->fPhase); pObj->Level = 1 + IF_MAX( pFan0->Level, pFan1->Level ); if ( p->nLevelMax < (int)pObj->Level ) p->nLevelMax = (int)pObj->Level; @@ -227,12 +236,12 @@ If_Obj_t * If_ManCreateAnd( If_Man_t * p, If_Obj_t * pFan0, int fCompl0, If_Obj_ SeeAlso [] ***********************************************************************/ -If_Obj_t * If_ManCreateXnor( If_Man_t * p, If_Obj_t * pFan0, If_Obj_t * pFan1 ) +If_Obj_t * If_ManCreateXor( If_Man_t * p, If_Obj_t * pFan0, If_Obj_t * pFan1 ) { If_Obj_t * pRes1, * pRes2; - pRes1 = If_ManCreateAnd( p, pFan0, 0, pFan1, 1 ); - pRes2 = If_ManCreateAnd( p, pFan0, 1, pFan1, 0 ); - return If_ManCreateAnd( p, pRes1, 1, pRes2, 1 ); + pRes1 = If_ManCreateAnd( p, If_Not(pFan0), pFan1 ); + pRes2 = If_ManCreateAnd( p, pFan0, If_Not(pFan1) ); + return If_Not( If_ManCreateAnd( p, If_Not(pRes1), If_Not(pRes2) ) ); } /**Function************************************************************* @@ -246,12 +255,12 @@ If_Obj_t * If_ManCreateXnor( If_Man_t * p, If_Obj_t * pFan0, If_Obj_t * pFan1 ) SeeAlso [] ***********************************************************************/ -If_Obj_t * If_ManCreateMnux( If_Man_t * p, If_Obj_t * pFan0, If_Obj_t * pFan1, If_Obj_t * pCtrl ) +If_Obj_t * If_ManCreateMux( If_Man_t * p, If_Obj_t * pFan0, If_Obj_t * pFan1, If_Obj_t * pCtrl ) { If_Obj_t * pRes1, * pRes2; - pRes1 = If_ManCreateAnd( p, pFan0, 0, pCtrl, 1 ); - pRes2 = If_ManCreateAnd( p, pFan1, 0, pCtrl, 0 ); - return If_ManCreateAnd( p, pRes1, 1, pRes2, 1 ); + pRes1 = If_ManCreateAnd( p, pFan0, If_Not(pCtrl) ); + pRes2 = If_ManCreateAnd( p, pFan1, pCtrl ); + return If_Not( If_ManCreateAnd( p, If_Not(pRes1), If_Not(pRes2) ) ); } /**Function************************************************************* diff --git a/src/opt/kit/kit.h b/src/opt/kit/kit.h index a0552b19..229b0bce 100644 --- a/src/opt/kit/kit.h +++ b/src/opt/kit/kit.h @@ -159,6 +159,7 @@ static inline unsigned Kit_DsdLitSupport( Kit_DsdNtk_t * pNtk, int Lit ) #define KIT_MIN(a,b) (((a) < (b))? (a) : (b)) #define KIT_MAX(a,b) (((a) > (b))? (a) : (b)) +#define KIT_INFINITY (100000000) #ifndef ALLOC #define ALLOC(type, num) ((type *) malloc(sizeof(type) * (num))) @@ -235,6 +236,10 @@ static inline int Kit_WordFindFirstBit( unsigned uWord ) return i; return -1; } +static inline int Kit_WordHasOneBit( unsigned uWord ) +{ + return (uWord & (uWord - 1)) == 0; +} static inline int Kit_WordCountOnes( unsigned uWord ) { uWord = (uWord & 0x55555555) + ((uWord>>1) & 0x55555555); @@ -250,6 +255,14 @@ static inline int Kit_TruthCountOnes( unsigned * pIn, int nVars ) Counter += Kit_WordCountOnes(pIn[w]); return Counter; } +static inline int Kit_TruthFindFirstBit( unsigned * pIn, int nVars ) +{ + int w; + for ( w = 0; w < Kit_TruthWordNum(nVars); w++ ) + if ( pIn[w] ) + return Kit_WordFindFirstBit(pIn[w]); + return -1; +} static inline int Kit_TruthIsEqual( unsigned * pIn0, unsigned * pIn1, int nVars ) { int w; @@ -433,7 +446,9 @@ extern DdNode * Kit_TruthToBdd( DdManager * dd, unsigned * pTruth, int nV /*=== kitDsd.c ==========================================================*/ extern Kit_DsdNtk_t * Kit_DsdDeriveNtk( unsigned * pTruth, int nVars, int nLutSize ); extern unsigned * Kit_DsdTruthCompute( Kit_DsdMan_t * p, Kit_DsdNtk_t * pNtk ); +extern void Kit_DsdTruth( Kit_DsdNtk_t * pNtk, unsigned * pTruthRes ); extern void Kit_DsdPrint( FILE * pFile, Kit_DsdNtk_t * pNtk ); +extern void Kit_DsdPrintExpanded( Kit_DsdNtk_t * pNtk ); extern Kit_DsdNtk_t * Kit_DsdDecompose( unsigned * pTruth, int nVars ); extern void Kit_DsdNtkFree( Kit_DsdNtk_t * pNtk ); extern int Kit_DsdNonDsdSizeMax( Kit_DsdNtk_t * pNtk ); diff --git a/src/opt/kit/kitDsd.c b/src/opt/kit/kitDsd.c index 8dd1b06f..8b6b6979 100644 --- a/src/opt/kit/kitDsd.c +++ b/src/opt/kit/kitDsd.c @@ -47,7 +47,7 @@ Kit_DsdMan_t * Kit_DsdManAlloc( int nVars ) p->nVars = nVars; p->nWords = Kit_TruthWordNum( p->nVars ); p->vTtElems = Vec_PtrAllocTruthTables( p->nVars ); - p->vTtNodes = Vec_PtrAllocSimInfo( 64, p->nWords ); + p->vTtNodes = Vec_PtrAllocSimInfo( 1024, p->nWords ); return p; } @@ -262,6 +262,25 @@ void Kit_DsdPrint( FILE * pFile, Kit_DsdNtk_t * pNtk ) /**Function************************************************************* + Synopsis [Print the DSD formula.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Kit_DsdPrintExpanded( Kit_DsdNtk_t * pNtk ) +{ + Kit_DsdNtk_t * pTemp; + pTemp = Kit_DsdExpand( pNtk ); + Kit_DsdPrint( stdout, pNtk ); + Kit_DsdNtkFree( pTemp ); +} + +/**Function************************************************************* + Synopsis [Derives the truth table of the DSD node.] Description [] @@ -384,6 +403,26 @@ unsigned * Kit_DsdTruthCompute( Kit_DsdMan_t * p, Kit_DsdNtk_t * pNtk ) return pTruthRes; } +/**Function************************************************************* + + Synopsis [Derives the truth table of the DSD network.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Kit_DsdTruth( Kit_DsdNtk_t * pNtk, unsigned * pTruthRes ) +{ + Kit_DsdMan_t * p; + unsigned * pTruth; + p = Kit_DsdManAlloc( pNtk->nVars ); + pTruth = Kit_DsdTruthCompute( p, pNtk ); + Kit_TruthCopy( pTruthRes, pTruth, pNtk->nVars ); + Kit_DsdManFree( p ); +} /**Function************************************************************* @@ -551,29 +590,25 @@ void Kit_DsdExpandCollectXor_rec( Kit_DsdNtk_t * p, int iLit, int * piLitsNew, i int Kit_DsdExpandNode_rec( Kit_DsdNtk_t * pNew, Kit_DsdNtk_t * p, int iLit ) { unsigned * pTruth, * pTruthNew; - unsigned i, fCompl, iLitFanin, piLitsNew[16], nLitsNew = 0; + unsigned i, iLitFanin, piLitsNew[16], nLitsNew = 0; Kit_DsdObj_t * pObj, * pObjNew; - // remember the complement - fCompl = Kit_DsdLitIsCompl(iLit); - iLit = Kit_DsdLitRegular(iLit); - assert( !Kit_DsdLitIsCompl(iLit) ); - // consider the case of simple gate pObj = Kit_DsdNtkObj( p, Kit_DsdLit2Var(iLit) ); if ( pObj == NULL ) - return Kit_DsdLitNotCond( iLit, fCompl ); + return iLit; if ( pObj->Type == KIT_DSD_AND ) { - Kit_DsdExpandCollectAnd_rec( p, iLit, piLitsNew, &nLitsNew ); + Kit_DsdExpandCollectAnd_rec( p, Kit_DsdLitRegular(iLit), piLitsNew, &nLitsNew ); pObjNew = Kit_DsdObjAlloc( pNew, KIT_DSD_AND, nLitsNew ); for ( i = 0; i < pObjNew->nFans; i++ ) pObjNew->pFans[i] = Kit_DsdExpandNode_rec( pNew, p, piLitsNew[i] ); - return Kit_DsdVar2Lit( pObjNew->Id, fCompl ); + return Kit_DsdVar2Lit( pObjNew->Id, Kit_DsdLitIsCompl(iLit) ); } if ( pObj->Type == KIT_DSD_XOR ) { - Kit_DsdExpandCollectXor_rec( p, iLit, piLitsNew, &nLitsNew ); + int fCompl = Kit_DsdLitIsCompl(iLit); + Kit_DsdExpandCollectXor_rec( p, Kit_DsdLitRegular(iLit), piLitsNew, &nLitsNew ); pObjNew = Kit_DsdObjAlloc( pNew, KIT_DSD_XOR, nLitsNew ); for ( i = 0; i < pObjNew->nFans; i++ ) { @@ -602,7 +637,7 @@ int Kit_DsdExpandNode_rec( Kit_DsdNtk_t * pNew, Kit_DsdNtk_t * p, int iLit ) } } // if the incoming phase is complemented, absorb it into the prime node - if ( fCompl ) + if ( Kit_DsdLitIsCompl(iLit) ) Kit_TruthNot( pTruthNew, pTruthNew, pObj->nFans ); return Kit_DsdVar2Lit( pObjNew->Id, 0 ); } @@ -655,46 +690,48 @@ Kit_DsdNtk_t * Kit_DsdExpand( Kit_DsdNtk_t * p ) SeeAlso [] ***********************************************************************/ -void Kit_DsdCompSort( int pPrios[], unsigned uSupps[], int piLitsNew[], int nVars ) +void Kit_DsdCompSort( int pPrios[], unsigned uSupps[], unsigned char * piLits, int nVars, int piLitsRes[] ) { - int nSuppSizes[16], Priority[16], pOrder[16], Temp[16]; - int i, k, iVarBest, SuppMax, PrioMin; + int nSuppSizes[16], Priority[16], pOrder[16]; + int i, k, iVarBest, SuppMax, PrioMax; // compute support sizes and priorities of the components for ( i = 0; i < nVars; i++ ) { - Temp[i] = piLitsNew[i]; + assert( uSupps[i] ); pOrder[i] = i; - Priority[i] = 16; - nSuppSizes[i] = Kit_WordCountOnes(uSupps[i]); + Priority[i] = KIT_INFINITY; for ( k = 0; k < 16; k++ ) if ( uSupps[i] & (1 << k) ) Priority[i] = KIT_MIN( Priority[i], pPrios[k] ); assert( Priority[i] != 16 ); + nSuppSizes[i] = Kit_WordCountOnes(uSupps[i]); } - // find the component by with largest size and smallest priority + // sort the components by pririty + Extra_BubbleSort( pOrder, Priority, nVars, 0 ); + // find the component by with largest size and lowest priority iVarBest = -1; - SuppMax = 0; - PrioMin = 16; + SuppMax = 0; + PrioMax = 0; for ( i = 0; i < nVars; i++ ) { - if ( SuppMax < nSuppSizes[i] || (SuppMax == nSuppSizes[i] && PrioMin > Priority[i]) ) + if ( SuppMax < nSuppSizes[i] || (SuppMax == nSuppSizes[i] && PrioMax < Priority[i]) ) { - SuppMax = nSuppSizes[i]; - PrioMin = Priority[i]; + SuppMax = nSuppSizes[i]; + PrioMax = Priority[i]; iVarBest = i; } } - // sort the components by pririty - Extra_BubbleSort( pOrder, Priority, nVars, 1 ); + assert( iVarBest != -1 ); // copy the resulting literals k = 0; - piLitsNew[k++] = piLitsNew[iVarBest]; + piLitsRes[k++] = piLits[iVarBest]; for ( i = 0; i < nVars; i++ ) { if ( pOrder[i] == iVarBest ) continue; - piLitsNew[k++] = piLitsNew[pOrder[i]]; + piLitsRes[k++] = piLits[pOrder[i]]; } + assert( k == nVars ); } /**Function************************************************************* @@ -713,76 +750,52 @@ int Kit_DsdShrink_rec( Kit_DsdNtk_t * pNew, Kit_DsdNtk_t * p, int iLit, int pPri Kit_DsdObj_t * pObj, * pObjNew; unsigned * pTruth, * pTruthNew; unsigned i, piLitsNew[16], uSupps[16]; - int fCompl, iLitFanin, iLitNew; - - // remember the complement - fCompl = Kit_DsdLitIsCompl(iLit); - iLit = Kit_DsdLitRegular(iLit); - assert( !Kit_DsdLitIsCompl(iLit) ); + int iLitFanin, iLitNew; // consider the case of simple gate pObj = Kit_DsdNtkObj( p, Kit_DsdLit2Var(iLit) ); if ( pObj == NULL ) - return Kit_DsdLitNotCond( iLit, fCompl ); + return iLit; if ( pObj->Type == KIT_DSD_AND ) { - if ( pObj->nFans == 2 ) + // get the supports + Kit_DsdObjForEachFanin( p, pObj, iLitFanin, i ) + uSupps[i] = Kit_DsdLitSupport( p, iLitFanin ); + // put the largest component last + // sort other components in the decreasing order of priority of their vars + Kit_DsdCompSort( pPrios, uSupps, pObj->pFans, pObj->nFans, piLitsNew ); + // construct the two-input node network + iLitNew = Kit_DsdShrink_rec( pNew, p, piLitsNew[0], pPrios ); + for ( i = 1; i < pObj->nFans; i++ ) { pObjNew = Kit_DsdObjAlloc( pNew, KIT_DSD_AND, 2 ); - pObjNew->pFans[0] = Kit_DsdShrink_rec( pNew, p, pObj->pFans[0], pPrios ); - pObjNew->pFans[1] = Kit_DsdShrink_rec( pNew, p, pObj->pFans[1], pPrios ); - } - else - { - // get the supports - Kit_DsdObjForEachFanin( p, pObj, iLitFanin, i ) - { - piLitsNew[i] = iLitFanin; - uSupps[i] = Kit_DsdLitSupport( p, iLitFanin ); - } - // put the largest component first - // sort other components in the increasing order of the highest variable - Kit_DsdCompSort( pPrios, uSupps, piLitsNew, pObj->nFans ); - iLitNew = Kit_DsdShrink_rec( pNew, p, piLitsNew[0], pPrios ); - for ( i = 1; i < pObj->nFans; i++ ) - { - pObjNew = Kit_DsdObjAlloc( pNew, KIT_DSD_AND, 2 ); - pObjNew->pFans[0] = iLitNew; - pObjNew->pFans[1] = Kit_DsdShrink_rec( pNew, p, piLitsNew[i], pPrios ); - iLitNew = Kit_DsdVar2Lit( pObjNew->Id, 0 ); - } + pObjNew->pFans[0] = Kit_DsdShrink_rec( pNew, p, piLitsNew[i], pPrios ); + pObjNew->pFans[1] = iLitNew; + iLitNew = Kit_DsdVar2Lit( pObjNew->Id, 0 ); } - return Kit_DsdVar2Lit( pObjNew->Id, fCompl ); + return Kit_DsdVar2Lit( pObjNew->Id, Kit_DsdLitIsCompl(iLit) ); } if ( pObj->Type == KIT_DSD_XOR ) { - if ( pObj->nFans == 2 ) + // get the supports + Kit_DsdObjForEachFanin( p, pObj, iLitFanin, i ) { - pObjNew = Kit_DsdObjAlloc( pNew, KIT_DSD_XOR, 2 ); - pObjNew->pFans[0] = Kit_DsdShrink_rec( pNew, p, pObj->pFans[0], pPrios ); - pObjNew->pFans[1] = Kit_DsdShrink_rec( pNew, p, pObj->pFans[1], pPrios ); + assert( !Kit_DsdLitIsCompl(iLitFanin) ); + uSupps[i] = Kit_DsdLitSupport( p, iLitFanin ); } - else + // put the largest component last + // sort other components in the decreasing order of priority of their vars + Kit_DsdCompSort( pPrios, uSupps, pObj->pFans, pObj->nFans, piLitsNew ); + // construct the two-input node network + iLitNew = Kit_DsdShrink_rec( pNew, p, piLitsNew[0], pPrios ); + for ( i = 1; i < pObj->nFans; i++ ) { - // get the supports - Kit_DsdObjForEachFanin( p, pObj, iLitFanin, i ) - { - piLitsNew[i] = iLitFanin; - uSupps[i] = Kit_DsdLitSupport( p, iLitFanin ); - } - // put the largest component first - // sort other components in the increasing order of the highest variable - Kit_DsdCompSort( pPrios, uSupps, piLitsNew, pObj->nFans ); - iLitNew = Kit_DsdShrink_rec( pNew, p, piLitsNew[0], pPrios ); - for ( i = 1; i < pObj->nFans; i++ ) - { - pObjNew = Kit_DsdObjAlloc( pNew, KIT_DSD_XOR, 2 ); - pObjNew->pFans[0] = iLitNew; - pObjNew->pFans[1] = Kit_DsdShrink_rec( pNew, p, piLitsNew[i], pPrios ); - iLitNew = Kit_DsdVar2Lit( pObjNew->Id, 0 ); - } + pObjNew = Kit_DsdObjAlloc( pNew, KIT_DSD_XOR, 2 ); + pObjNew->pFans[0] = Kit_DsdShrink_rec( pNew, p, piLitsNew[i], pPrios ); + pObjNew->pFans[1] = iLitNew; + iLitNew = Kit_DsdVar2Lit( pObjNew->Id, 0 ); } - return Kit_DsdVar2Lit( pObjNew->Id, fCompl ); + return Kit_DsdVar2Lit( pObjNew->Id, Kit_DsdLitIsCompl(iLit) ); } assert( pObj->Type == KIT_DSD_PRIME ); @@ -804,7 +817,7 @@ int Kit_DsdShrink_rec( Kit_DsdNtk_t * pNew, Kit_DsdNtk_t * p, int iLit, int pPri } } // if the incoming phase is complemented, absorb it into the prime node - if ( fCompl ) + if ( Kit_DsdLitIsCompl(iLit) ) Kit_TruthNot( pTruthNew, pTruthNew, pObj->nFans ); return Kit_DsdVar2Lit( pObjNew->Id, 0 ); } @@ -877,22 +890,26 @@ void Kit_DsdRotate( Kit_DsdNtk_t * p, int pFreqs[] ) Weights[k] = 0; for ( v = 0; v < 16; v++ ) if ( uSuppFanin & (1 << v) ) - Weights[k] += pFreqs[v]; + Weights[k] += pFreqs[v] - 1; } // find the most frequent fanin - WeightMax = FaninMax = 0; + WeightMax = 0; + FaninMax = -1; for ( k = 0; k < pObj->nFans; k++ ) if ( WeightMax < Weights[k] ) { WeightMax = Weights[k]; FaninMax = k; } - assert( k < pObj->nFans ); + // no need to reorder if there are no frequent fanins + if ( FaninMax == -1 ) + continue; // move the fanins number k to the first place nSwaps = 0; pIn = Kit_DsdObjTruth(pObj); - pOut = p->pSupps; - for ( v = k-1; v >= 0; v-- ) + pOut = p->pMem; +// for ( v = FaninMax; v < ((int)pObj->nFans)-1; v++ ) + for ( v = FaninMax-1; v >= 0; v-- ) { // swap the fanins Temp = pObj->pFans[v]; @@ -903,8 +920,8 @@ void Kit_DsdRotate( Kit_DsdNtk_t * p, int pFreqs[] ) pTemp = pIn; pIn = pOut; pOut = pTemp; nSwaps++; } - if ( nSwaps & 1) - Kit_TruthCopy( pIn, pOut, pObj->nFans ); + if ( nSwaps & 1 ) + Kit_TruthCopy( pOut, pIn, pObj->nFans ); } } @@ -919,19 +936,53 @@ void Kit_DsdRotate( Kit_DsdNtk_t * p, int pFreqs[] ) SeeAlso [] ***********************************************************************/ -void Kit_DsdGetSupports( Kit_DsdNtk_t * p ) +unsigned Kit_DsdGetSupports_rec( Kit_DsdNtk_t * p, int iLit ) { Kit_DsdObj_t * pObj; unsigned uSupport, k; - int iFaninLit, i; + int iFaninLit; + pObj = Kit_DsdNtkObj( p, Kit_DsdLit2Var(iLit) ); + if ( pObj == NULL ) + return Kit_DsdLitSupport( p, iLit ); + uSupport = 0; + Kit_DsdObjForEachFanin( p, pObj, iFaninLit, k ) + uSupport |= Kit_DsdGetSupports_rec( p, iFaninLit ); + p->pSupps[pObj->Id - p->nVars] = uSupport; + assert( uSupport <= 0xFFFF ); + return uSupport; +} + +/**Function************************************************************* + + Synopsis [Compute the support.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Kit_DsdGetSupports( Kit_DsdNtk_t * p ) +{ + Kit_DsdObj_t * pRoot; + assert( p->pSupps == NULL ); p->pSupps = ALLOC( unsigned, p->nNodes ); - Kit_DsdNtkForEachObj( p, pObj, i ) + // consider simple special cases + pRoot = Kit_DsdNtkRoot(p); + if ( pRoot->Type == KIT_DSD_CONST1 ) { - uSupport = 0; - Kit_DsdObjForEachFanin( p, pObj, iFaninLit, k ) - uSupport |= Kit_DsdLitSupport( p, iFaninLit ); - p->pSupps[pObj->Id - p->nVars] = uSupport; - } + assert( p->nNodes == 1 ); + p->pSupps[0] = 0; + } + if ( pRoot->Type == KIT_DSD_VAR ) + { + assert( p->nNodes == 1 ); + p->pSupps[0] = Kit_DsdLitSupport( p, pRoot->pFans[0] ); + } + else + Kit_DsdGetSupports_rec( p, p->Root ); + assert( p->pSupps[0] <= 0xFFFF ); } /**Function************************************************************* @@ -1772,6 +1823,251 @@ int Kit_DsdCofactoring( unsigned * pTruth, int nVars, int * pCofVars, int nLimit return nStep; } +/**Function************************************************************* + + Synopsis [Canonical decomposition into completely DSD-structure.] + + Description [Returns the number of cofactoring steps. Also returns + the cofactoring variables in pVars.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Kit_DsdPrintCofactors( unsigned * pTruth, int nVars, int nCofLevel, int fVerbose ) +{ + Kit_DsdNtk_t * ppNtks[32] = {0}, * pTemp; + unsigned * ppCofs[5][16]; + int piCofVar[5]; + int nPrimeSizeMax, nPrimeSizeCur, nSuppSizeMax; + int i, k, v1, v2, v3, v4, s, nSteps, nSize, nMemSize; + assert( nCofLevel < 5 ); + + // print the function + ppNtks[0] = Kit_DsdDecompose( pTruth, nVars ); + ppNtks[0] = Kit_DsdExpand( pTemp = ppNtks[0] ); + Kit_DsdNtkFree( pTemp ); + if ( fVerbose ) + Kit_DsdPrint( stdout, ppNtks[0] ); + Kit_DsdNtkFree( ppNtks[0] ); + + // allocate storage for cofactors + nMemSize = Kit_TruthWordNum(nVars); + ppCofs[0][0] = ALLOC( unsigned, 80 * nMemSize ); + nSize = 0; + for ( i = 0; i < 5; i++ ) + for ( k = 0; k < 16; k++ ) + ppCofs[i][k] = ppCofs[0][0] + nMemSize * nSize++; + assert( nSize == 80 ); + + // copy the function + Kit_TruthCopy( ppCofs[0][0], pTruth, nVars ); + + if ( nCofLevel == 1 ) + for ( v1 = 0; v1 < nVars; v1++ ) + { + nSteps = 0; + piCofVar[nSteps++] = v1; + + printf( " Variables { " ); + for ( i = 0; i < nSteps; i++ ) + printf( "%c ", 'a' + piCofVar[i] ); + printf( "}\n" ); + + // single cofactors + for ( s = 1; s <= nSteps; s++ ) + { + for ( k = 0; k < s; k++ ) + { + nSize = (1 << k); + for ( i = 0; i < nSize; i++ ) + { + Kit_TruthCofactor0New( ppCofs[k+1][2*i+0], ppCofs[k][i], nVars, piCofVar[k] ); + Kit_TruthCofactor1New( ppCofs[k+1][2*i+1], ppCofs[k][i], nVars, piCofVar[k] ); + } + } + } + // compute DSD networks + nSize = (1 << nSteps); + nPrimeSizeMax = 0; + nSuppSizeMax = 0; + for ( i = 0; i < nSize; i++ ) + { + ppNtks[i] = Kit_DsdDecompose( ppCofs[nSteps][i], nVars ); + ppNtks[i] = Kit_DsdExpand( pTemp = ppNtks[i] ); + Kit_DsdNtkFree( pTemp ); + if ( fVerbose ) + { + printf( "Cof%d%d: ", nSteps, i ); + Kit_DsdPrint( stdout, ppNtks[i] ); + } + // compute the largest non-decomp block + nPrimeSizeCur = Kit_DsdNonDsdSizeMax(ppNtks[i]); + nPrimeSizeMax = KIT_MAX( nPrimeSizeMax, nPrimeSizeCur ); + Kit_DsdNtkFree( ppNtks[i] ); + nSuppSizeMax += Kit_TruthSupportSize( ppCofs[nSteps][i], nVars ); + } + printf( "Max = %2d. Supps = %2d.\n", nPrimeSizeMax, nSuppSizeMax ); + } + + if ( nCofLevel == 2 ) + for ( v1 = 0; v1 < nVars; v1++ ) + for ( v2 = v1+1; v2 < nVars; v2++ ) + { + nSteps = 0; + piCofVar[nSteps++] = v1; + piCofVar[nSteps++] = v2; + + printf( " Variables { " ); + for ( i = 0; i < nSteps; i++ ) + printf( "%c ", 'a' + piCofVar[i] ); + printf( "}\n" ); + + // single cofactors + for ( s = 1; s <= nSteps; s++ ) + { + for ( k = 0; k < s; k++ ) + { + nSize = (1 << k); + for ( i = 0; i < nSize; i++ ) + { + Kit_TruthCofactor0New( ppCofs[k+1][2*i+0], ppCofs[k][i], nVars, piCofVar[k] ); + Kit_TruthCofactor1New( ppCofs[k+1][2*i+1], ppCofs[k][i], nVars, piCofVar[k] ); + } + } + } + // compute DSD networks + nSize = (1 << nSteps); + nPrimeSizeMax = 0; + nSuppSizeMax = 0; + for ( i = 0; i < nSize; i++ ) + { + ppNtks[i] = Kit_DsdDecompose( ppCofs[nSteps][i], nVars ); + ppNtks[i] = Kit_DsdExpand( pTemp = ppNtks[i] ); + Kit_DsdNtkFree( pTemp ); + if ( fVerbose ) + { + printf( "Cof%d%d: ", nSteps, i ); + Kit_DsdPrint( stdout, ppNtks[i] ); + } + // compute the largest non-decomp block + nPrimeSizeCur = Kit_DsdNonDsdSizeMax(ppNtks[i]); + nPrimeSizeMax = KIT_MAX( nPrimeSizeMax, nPrimeSizeCur ); + Kit_DsdNtkFree( ppNtks[i] ); + nSuppSizeMax += Kit_TruthSupportSize( ppCofs[nSteps][i], nVars ); + } + printf( "Max = %2d. Supps = %2d.\n", nPrimeSizeMax, nSuppSizeMax ); + } + + if ( nCofLevel == 3 ) + for ( v1 = 0; v1 < nVars; v1++ ) + for ( v2 = v1+1; v2 < nVars; v2++ ) + for ( v3 = v2+1; v3 < nVars; v3++ ) + { + nSteps = 0; + piCofVar[nSteps++] = v1; + piCofVar[nSteps++] = v2; + piCofVar[nSteps++] = v3; + + printf( " Variables { " ); + for ( i = 0; i < nSteps; i++ ) + printf( "%c ", 'a' + piCofVar[i] ); + printf( "}\n" ); + + // single cofactors + for ( s = 1; s <= nSteps; s++ ) + { + for ( k = 0; k < s; k++ ) + { + nSize = (1 << k); + for ( i = 0; i < nSize; i++ ) + { + Kit_TruthCofactor0New( ppCofs[k+1][2*i+0], ppCofs[k][i], nVars, piCofVar[k] ); + Kit_TruthCofactor1New( ppCofs[k+1][2*i+1], ppCofs[k][i], nVars, piCofVar[k] ); + } + } + } + // compute DSD networks + nSize = (1 << nSteps); + nPrimeSizeMax = 0; + nSuppSizeMax = 0; + for ( i = 0; i < nSize; i++ ) + { + ppNtks[i] = Kit_DsdDecompose( ppCofs[nSteps][i], nVars ); + ppNtks[i] = Kit_DsdExpand( pTemp = ppNtks[i] ); + Kit_DsdNtkFree( pTemp ); + if ( fVerbose ) + { + printf( "Cof%d%d: ", nSteps, i ); + Kit_DsdPrint( stdout, ppNtks[i] ); + } + // compute the largest non-decomp block + nPrimeSizeCur = Kit_DsdNonDsdSizeMax(ppNtks[i]); + nPrimeSizeMax = KIT_MAX( nPrimeSizeMax, nPrimeSizeCur ); + Kit_DsdNtkFree( ppNtks[i] ); + nSuppSizeMax += Kit_TruthSupportSize( ppCofs[nSteps][i], nVars ); + } + printf( "Max = %2d. Supps = %2d.\n", nPrimeSizeMax, nSuppSizeMax ); + } + + if ( nCofLevel == 4 ) + for ( v1 = 0; v1 < nVars; v1++ ) + for ( v2 = v1+1; v2 < nVars; v2++ ) + for ( v3 = v2+1; v3 < nVars; v3++ ) + for ( v4 = v3+1; v4 < nVars; v4++ ) + { + nSteps = 0; + piCofVar[nSteps++] = v1; + piCofVar[nSteps++] = v2; + piCofVar[nSteps++] = v3; + piCofVar[nSteps++] = v4; + + printf( " Variables { " ); + for ( i = 0; i < nSteps; i++ ) + printf( "%c ", 'a' + piCofVar[i] ); + printf( "}\n" ); + + // single cofactors + for ( s = 1; s <= nSteps; s++ ) + { + for ( k = 0; k < s; k++ ) + { + nSize = (1 << k); + for ( i = 0; i < nSize; i++ ) + { + Kit_TruthCofactor0New( ppCofs[k+1][2*i+0], ppCofs[k][i], nVars, piCofVar[k] ); + Kit_TruthCofactor1New( ppCofs[k+1][2*i+1], ppCofs[k][i], nVars, piCofVar[k] ); + } + } + } + // compute DSD networks + nSize = (1 << nSteps); + nPrimeSizeMax = 0; + nSuppSizeMax = 0; + for ( i = 0; i < nSize; i++ ) + { + ppNtks[i] = Kit_DsdDecompose( ppCofs[nSteps][i], nVars ); + ppNtks[i] = Kit_DsdExpand( pTemp = ppNtks[i] ); + Kit_DsdNtkFree( pTemp ); + if ( fVerbose ) + { + printf( "Cof%d%d: ", nSteps, i ); + Kit_DsdPrint( stdout, ppNtks[i] ); + } + // compute the largest non-decomp block + nPrimeSizeCur = Kit_DsdNonDsdSizeMax(ppNtks[i]); + nPrimeSizeMax = KIT_MAX( nPrimeSizeMax, nPrimeSizeCur ); + Kit_DsdNtkFree( ppNtks[i] ); + nSuppSizeMax += Kit_TruthSupportSize( ppCofs[nSteps][i], nVars ); + } + printf( "Max = %2d. Supps = %2d.\n", nPrimeSizeMax, nSuppSizeMax ); + } + + + free( ppCofs[0][0] ); +} + //////////////////////////////////////////////////////////////////////// /// END OF FILE /// //////////////////////////////////////////////////////////////////////// diff --git a/src/opt/lpk/lpk.h b/src/opt/lpk/lpk.h new file mode 100644 index 00000000..092b43e1 --- /dev/null +++ b/src/opt/lpk/lpk.h @@ -0,0 +1,82 @@ +/**CFile**************************************************************** + + FileName [lpk.h] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [Fast Boolean matching for LUT structures.] + + Synopsis [External declarations.] + + Author [Alan Mishchenko] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - April 28, 2007.] + + Revision [$Id: lpk.h,v 1.00 2007/04/28 00:00:00 alanmi Exp $] + +***********************************************************************/ + +#ifndef __LPK_H__ +#define __LPK_H__ + +#ifdef __cplusplus +extern "C" { +#endif + +//////////////////////////////////////////////////////////////////////// +/// INCLUDES /// +//////////////////////////////////////////////////////////////////////// + +//////////////////////////////////////////////////////////////////////// +/// PARAMETERS /// +//////////////////////////////////////////////////////////////////////// + +//////////////////////////////////////////////////////////////////////// +/// BASIC TYPES /// +//////////////////////////////////////////////////////////////////////// + +typedef struct Lpk_Par_t_ Lpk_Par_t; +struct Lpk_Par_t_ +{ + // user-controlled parameters + int nLutsMax; // (N) the maximum number of LUTs in the structure + int nLutsOver; // (Q) the maximum number of LUTs not in the MFFC + int nVarsShared; // (S) the maximum number of shared variables (crossbars) + int nGrowthLevel; // (L) the maximum increase in the node level after resynthesis + int fSatur; // iterate till saturation + int fZeroCost; // accept zero-cost replacements + int fVerbose; // the verbosiness flag + int fVeryVerbose; // additional verbose info printout + // internal parameters + int nLutSize; // (K) the LUT size (determined by the input network) + int nVarsMax; // (V) the largest number of variables: V = N * (K-1) + 1 +}; + +//////////////////////////////////////////////////////////////////////// +/// MACRO DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + +//////////////////////////////////////////////////////////////////////// +/// ITERATORS /// +//////////////////////////////////////////////////////////////////////// + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +/*=== lpkCore.c ========================================================*/ +extern int Lpk_Resynthesize( Abc_Ntk_t * pNtk, Lpk_Par_t * pPars ); + + +#ifdef __cplusplus +} +#endif + +#endif + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + diff --git a/src/opt/lpk/lpkCore.c b/src/opt/lpk/lpkCore.c new file mode 100644 index 00000000..cbd971e3 --- /dev/null +++ b/src/opt/lpk/lpkCore.c @@ -0,0 +1,280 @@ +/**CFile**************************************************************** + + FileName [lpkCore.c] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [Fast Boolean matching for LUT structures.] + + Synopsis [] + + Author [Alan Mishchenko] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - April 28, 2007.] + + Revision [$Id: lpkCore.c,v 1.00 2007/04/28 00:00:00 alanmi Exp $] + +***********************************************************************/ + +#include "lpkInt.h" + +//////////////////////////////////////////////////////////////////////// +/// DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + +/**Function************************************************************* + + Synopsis [Returns 1 if at least one entry has changed.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Lpk_NodeHasChanged( Lpk_Man_t * p, int iNode ) +{ + Vec_Ptr_t * vNodes; + Abc_Obj_t * pTemp; + int i; + vNodes = Vec_VecEntry( p->vVisited, iNode ); + if ( Vec_PtrSize(vNodes) == 0 ) + return 1; + Vec_PtrForEachEntry( vNodes, pTemp, i ) + { + // check if the node has changed + pTemp = Abc_NtkObj( p->pNtk, (int)pTemp ); + if ( pTemp == NULL ) + return 1; + // check if the number of fanouts has changed +// if ( Abc_ObjFanoutNum(pTemp) != (int)Vec_PtrEntry(vNodes, i+1) ) +// return 1; + i++; + } + return 0; +} + +/**Function************************************************************* + + Synopsis [Performs resynthesis for one node.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Lpk_ResynthesizeNode( Lpk_Man_t * p ) +{ + Kit_DsdNtk_t * pDsdNtk; + Lpk_Cut_t * pCut; + unsigned * pTruth; + void * pDsd = NULL; + int i, RetValue, clk; + + Lpk_Cut_t * pCutMax; + + // compute the cuts +clk = clock(); + if ( !Lpk_NodeCuts( p ) ) + { +p->timeCuts += clock() - clk; + return 0; + } +p->timeCuts += clock() - clk; + + // find the max volume cut + pCutMax = NULL; + for ( i = 0; i < p->nEvals; i++ ) + { + pCut = p->pCuts + p->pEvals[i]; + if ( pCutMax == NULL || pCutMax->nNodes < pCut->nNodes ) + pCutMax = pCut; + } + assert( pCutMax != NULL ); + + + if ( p->pPars->fVeryVerbose ) + printf( "Node %5d : Mffc size = %5d. Cuts = %5d.\n", p->pObj->Id, p->nMffc, p->nEvals ); + // try the good cuts + p->nCutsTotal += p->nCuts; + p->nCutsUseful += p->nEvals; + for ( i = 0; i < p->nEvals; i++ ) + { + // get the cut + pCut = p->pCuts + p->pEvals[i]; + + if ( pCut != pCutMax ) + continue; + + // compute the truth table +clk = clock(); + pTruth = Lpk_CutTruth( p, pCut ); +p->timeTruth += clock() - clk; + +clk = clock(); + pDsdNtk = Kit_DsdDeriveNtk( pTruth, pCut->nLeaves, p->pPars->nLutSize ); +p->timeEval += clock() - clk; + + if ( Kit_DsdNtkRoot(pDsdNtk)->nFans == 16 ) // skip 16-input non-DSD because ISOP will not work + { + Kit_DsdNtkFree( pDsdNtk ); + continue; + } + + if ( p->pPars->fVeryVerbose ) + { + printf( " C%02d: L= %2d/%2d V= %2d/%d N= %d W= %4.2f ", + i, pCut->nLeaves, Extra_TruthSupportSize(pTruth, pCut->nLeaves), pCut->nNodes, pCut->nNodesDup, pCut->nLuts, pCut->Weight ); + Kit_DsdPrint( stdout, pDsdNtk ); + } + + // update the network +clk = clock(); + RetValue = Lpk_CutExplore( p, pCut, pDsdNtk ); + Kit_DsdNtkFree( pDsdNtk ); +p->timeMap += clock() - clk; + if ( RetValue ) + break; + } + return 1; +} + +/**Function************************************************************* + + Synopsis [Performs resynthesis for one network.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Lpk_Resynthesize( Abc_Ntk_t * pNtk, Lpk_Par_t * pPars ) +{ + ProgressBar * pProgress; + Lpk_Man_t * p; + Abc_Obj_t * pObj; + double Delta; + int i, Iter, nNodes, nNodesPrev, clk = clock(); + assert( Abc_NtkIsLogic(pNtk) ); + + // get the number of inputs + pPars->nLutSize = Abc_NtkGetFaninMax( pNtk ); + // adjust the number of crossbars based on LUT size + if ( pPars->nVarsShared > pPars->nLutSize - 2 ) + pPars->nVarsShared = pPars->nLutSize - 2; + // get the max number of LUTs tried + pPars->nVarsMax = pPars->nLutsMax * (pPars->nLutSize - 1) + 1; // V = N * (K-1) + 1 + while ( pPars->nVarsMax > 16 ) + { + pPars->nLutsMax--; + pPars->nVarsMax = pPars->nLutsMax * (pPars->nLutSize - 1) + 1; + + } + if ( pPars->fVerbose ) + { + printf( "Resynthesis for %d %d-LUTs with %d non-MFFC LUTs, %d crossbars, and %d-input cuts.\n", + pPars->nLutsMax, pPars->nLutSize, pPars->nLutsOver, pPars->nVarsShared, pPars->nVarsMax ); + } + + // convert logic to AIGs + Abc_NtkToAig( pNtk ); + + // start the manager + p = Lpk_ManStart( pPars ); + p->pNtk = pNtk; + p->nNodesTotal = Abc_NtkNodeNum(pNtk); + p->vLevels = Vec_VecStart( 3 * Abc_NtkLevel(pNtk) ); // computes levels of all nodes + if ( p->pPars->fSatur ) + p->vVisited = Vec_VecStart( 0 ); + + // iterate over the network + nNodesPrev = p->nNodesTotal; + for ( Iter = 1; ; Iter++ ) + { + // expand storage for changed nodes + if ( p->pPars->fSatur ) + Vec_VecExpand( p->vVisited, Abc_NtkObjNumMax(pNtk) + 1 ); + + // consider all nodes + nNodes = Abc_NtkObjNumMax(pNtk); + if ( !pPars->fVeryVerbose ) + pProgress = Extra_ProgressBarStart( stdout, nNodes ); + Abc_NtkForEachNode( pNtk, pObj, i ) + { + // skip all except the final node +// if ( !Abc_ObjIsCo(Abc_ObjFanout0(pObj)) ) +// continue; + + if ( i >= nNodes ) + break; + if ( !pPars->fVeryVerbose ) + Extra_ProgressBarUpdate( pProgress, i, NULL ); + // skip the nodes that did not change + if ( p->pPars->fSatur && !Lpk_NodeHasChanged(p, pObj->Id) ) + continue; + // resynthesize + p->pObj = pObj; + Lpk_ResynthesizeNode( p ); + + if ( p->nChanges == 3 ) + break; + } + if ( !pPars->fVeryVerbose ) + Extra_ProgressBarStop( pProgress ); + + // check the increase + Delta = 100.00 * (nNodesPrev - Abc_NtkNodeNum(pNtk)) / p->nNodesTotal; + if ( Delta < 0.05 ) + break; + nNodesPrev = Abc_NtkNodeNum(pNtk); + if ( !p->pPars->fSatur ) + break; + + break; + } + + if ( pPars->fVerbose ) + { + printf( "N = %5d (%3d) Cut = %5d (%4d) Change = %5d Gain = %5d (%5.2f %%) Iter = %2d\n", + p->nNodesTotal, p->nNodesOver, p->nCutsTotal, p->nCutsUseful, p->nChanges, p->nGainTotal, 100.0 * p->nGainTotal / p->nNodesTotal, Iter ); + printf( "Non_DSD blocks: " ); + for ( i = 3; i <= pPars->nVarsMax; i++ ) + if ( p->nBlocks[i] ) + printf( "%d=%d ", i, p->nBlocks[i] ); + printf( "\n" ); + p->timeTotal = clock() - clk; + p->timeOther = p->timeTotal - p->timeCuts - p->timeTruth - p->timeEval - p->timeMap; + PRTP( "Cuts ", p->timeCuts, p->timeTotal ); + PRTP( "Truth ", p->timeTruth, p->timeTotal ); + PRTP( "Eval ", p->timeEval, p->timeTotal ); + PRTP( "Map ", p->timeMap, p->timeTotal ); + PRTP( "Other ", p->timeOther, p->timeTotal ); + PRTP( "TOTAL ", p->timeTotal, p->timeTotal ); + } + + Lpk_ManStop( p ); + // check the resulting network + if ( !Abc_NtkCheck( pNtk ) ) + { + printf( "Lpk_Resynthesize: The network check has failed.\n" ); + return 0; + } + return 1; +} + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + + diff --git a/src/opt/lpk/lpkCut.c b/src/opt/lpk/lpkCut.c new file mode 100644 index 00000000..251ec829 --- /dev/null +++ b/src/opt/lpk/lpkCut.c @@ -0,0 +1,584 @@ +/**CFile**************************************************************** + + FileName [lpkCut.c] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [Fast Boolean matching for LUT structures.] + + Synopsis [] + + Author [Alan Mishchenko] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - April 28, 2007.] + + Revision [$Id: lpkCut.c,v 1.00 2007/04/28 00:00:00 alanmi Exp $] + +***********************************************************************/ + +#include "lpkInt.h" + +//////////////////////////////////////////////////////////////////////// +/// DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + +/**Function************************************************************* + + Synopsis [Computes the truth able of one cut.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +unsigned * Lpk_CutTruth_rec( Hop_Man_t * pMan, Hop_Obj_t * pObj, int nVars, Vec_Ptr_t * vTtNodes, int * iCount ) +{ + unsigned * pTruth, * pTruth0, * pTruth1; + assert( !Hop_IsComplement(pObj) ); + if ( pObj->pData ) + { + assert( ((unsigned)pObj->pData) & 0xffff0000 ); + return pObj->pData; + } + // get the plan for a new truth table + pTruth = Vec_PtrEntry( vTtNodes, (*iCount)++ ); + if ( Hop_ObjIsConst1(pObj) ) + Extra_TruthFill( pTruth, nVars ); + else + { + assert( Hop_ObjIsAnd(pObj) ); + // compute the truth tables of the fanins + pTruth0 = Lpk_CutTruth_rec( pMan, Hop_ObjFanin0(pObj), nVars, vTtNodes, iCount ); + pTruth1 = Lpk_CutTruth_rec( pMan, Hop_ObjFanin1(pObj), nVars, vTtNodes, iCount ); + // creat the truth table of the node + Extra_TruthAndPhase( pTruth, pTruth0, pTruth1, nVars, Hop_ObjFaninC0(pObj), Hop_ObjFaninC1(pObj) ); + } + pObj->pData = pTruth; + return pTruth; +} + +/**Function************************************************************* + + Synopsis [Computes the truth able of one cut.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +unsigned * Lpk_CutTruth( Lpk_Man_t * p, Lpk_Cut_t * pCut ) +{ + Hop_Man_t * pManHop = p->pNtk->pManFunc; + Hop_Obj_t * pObjHop; + Abc_Obj_t * pObj, * pFanin; + unsigned * pTruth; + int i, k, iCount = 0; +// Lpk_NodePrintCut( p, pCut ); + + // initialize the leaves + Lpk_CutForEachLeaf( p->pNtk, pCut, pObj, i ) + pObj->pCopy = Vec_PtrEntry( p->vTtElems, i ); + + // construct truth table in the topological order + Lpk_CutForEachNodeReverse( p->pNtk, pCut, pObj, i ) + { + // get the local AIG + pObjHop = Hop_Regular(pObj->pData); + // clean the data field of the nodes in the AIG subgraph + Hop_ObjCleanData_rec( pObjHop ); + // set the initial truth tables at the fanins + Abc_ObjForEachFanin( pObj, pFanin, k ) + { + assert( ((unsigned)pFanin->pCopy) & 0xffff0000 ); + Hop_ManPi( pManHop, k )->pData = pFanin->pCopy; + } + // compute the truth table of internal nodes + pTruth = Lpk_CutTruth_rec( pManHop, pObjHop, pCut->nLeaves, p->vTtNodes, &iCount ); + if ( Hop_IsComplement(pObj->pData) ) + Extra_TruthNot( pTruth, pTruth, pCut->nLeaves ); + // set the truth table at the node + pObj->pCopy = (Abc_Obj_t *)pTruth; + } + + return pTruth; +} + +/**Function************************************************************* + + Synopsis [Returns 1 if at least one entry has changed.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Lpk_NodeRecordImpact( Lpk_Man_t * p ) +{ + Lpk_Cut_t * pCut; + Vec_Ptr_t * vNodes = Vec_VecEntry( p->vVisited, p->pObj->Id ); + Abc_Obj_t * pNode; + int i, k; + // collect the nodes that impact the given node + Vec_PtrClear( vNodes ); + for ( i = 0; i < p->nCuts; i++ ) + { + pCut = p->pCuts + i; + for ( k = 0; k < (int)pCut->nLeaves; k++ ) + { + pNode = Abc_NtkObj( p->pNtk, pCut->pLeaves[k] ); + if ( pNode->fMarkC ) + continue; + pNode->fMarkC = 1; + Vec_PtrPush( vNodes, (void *)pNode->Id ); + Vec_PtrPush( vNodes, (void *)Abc_ObjFanoutNum(pNode) ); + } + } + // clear the marks + Vec_PtrForEachEntry( vNodes, pNode, i ) + { + pNode = Abc_NtkObj( p->pNtk, (int)pNode ); + pNode->fMarkC = 0; + i++; + } +//printf( "%d ", Vec_PtrSize(vNodes) ); +} + +/**Function************************************************************* + + Synopsis [Returns 1 if the cut has structural DSD.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Lpk_NodeCutsCheckDsd( Lpk_Man_t * p, Lpk_Cut_t * pCut ) +{ + Abc_Obj_t * pObj, * pFanin; + int i, k, nCands, fLeavesOnly, RetValue; + assert( pCut->nLeaves > 0 ); + // clear ref counters + memset( p->pRefs, 0, sizeof(int) * pCut->nLeaves ); + // mark cut leaves + Lpk_CutForEachLeaf( p->pNtk, pCut, pObj, i ) + { + assert( pObj->fMarkA == 0 ); + pObj->fMarkA = 1; + pObj->pCopy = (void *)i; + } + // ref leaves pointed from the internal nodes + nCands = 0; + Lpk_CutForEachNode( p->pNtk, pCut, pObj, i ) + { + fLeavesOnly = 1; + Abc_ObjForEachFanin( pObj, pFanin, k ) + if ( pFanin->fMarkA ) + p->pRefs[(int)pFanin->pCopy]++; + else + fLeavesOnly = 0; + if ( fLeavesOnly ) + p->pCands[nCands++] = pObj->Id; + } + // look at the nodes that only point to the leaves + RetValue = 0; + for ( i = 0; i < nCands; i++ ) + { + pObj = Abc_NtkObj( p->pNtk, p->pCands[i] ); + Abc_ObjForEachFanin( pObj, pFanin, k ) + { + assert( pFanin->fMarkA == 1 ); + if ( p->pRefs[(int)pFanin->pCopy] > 1 ) + break; + } + if ( k == Abc_ObjFaninNum(pObj) ) + { + RetValue = 1; + break; + } + } + // unmark cut leaves + Lpk_CutForEachLeaf( p->pNtk, pCut, pObj, i ) + pObj->fMarkA = 0; + return RetValue; +} + +/**Function************************************************************* + + Synopsis [Returns 1 if pDom is contained in pCut.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +static inline int Lpk_NodeCutsOneDominance( Lpk_Cut_t * pDom, Lpk_Cut_t * pCut ) +{ + int i, k; + for ( i = 0; i < (int)pDom->nLeaves; i++ ) + { + for ( k = 0; k < (int)pCut->nLeaves; k++ ) + if ( pDom->pLeaves[i] == pCut->pLeaves[k] ) + break; + if ( k == (int)pCut->nLeaves ) // node i in pDom is not contained in pCut + return 0; + } + // every node in pDom is contained in pCut + return 1; +} + +/**Function************************************************************* + + Synopsis [Check if the cut exists.] + + Description [Returns 1 if the cut exists.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Lpk_NodeCutsOneFilter( Lpk_Cut_t * pCuts, int nCuts, Lpk_Cut_t * pCutNew ) +{ + Lpk_Cut_t * pCut; + int i, k; + assert( pCutNew->uSign[0] || pCutNew->uSign[1] ); + // try to find the cut + for ( i = 0; i < nCuts; i++ ) + { + pCut = pCuts + i; + if ( pCut->nLeaves == 0 ) + continue; + if ( pCut->nLeaves == pCutNew->nLeaves ) + { + if ( pCut->uSign[0] == pCutNew->uSign[0] && pCut->uSign[1] == pCutNew->uSign[1] ) + { + for ( k = 0; k < (int)pCutNew->nLeaves; k++ ) + if ( pCut->pLeaves[k] != pCutNew->pLeaves[k] ) + break; + if ( k == (int)pCutNew->nLeaves ) + return 1; + } + continue; + } + if ( pCut->nLeaves < pCutNew->nLeaves ) + { + // skip the non-contained cuts + if ( (pCut->uSign[0] & pCutNew->uSign[0]) != pCut->uSign[0] ) + continue; + if ( (pCut->uSign[1] & pCutNew->uSign[1]) != pCut->uSign[1] ) + continue; + // check containment seriously + if ( Lpk_NodeCutsOneDominance( pCut, pCutNew ) ) + return 1; + continue; + } + // check potential containment of other cut + + // skip the non-contained cuts + if ( (pCut->uSign[0] & pCutNew->uSign[0]) != pCutNew->uSign[0] ) + continue; + if ( (pCut->uSign[1] & pCutNew->uSign[1]) != pCutNew->uSign[1] ) + continue; + // check containment seriously + if ( Lpk_NodeCutsOneDominance( pCutNew, pCut ) ) + pCut->nLeaves = 0; // removed + } + return 0; +} + +/**Function************************************************************* + + Synopsis [Prints the given cut.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Lpk_NodePrintCut( Lpk_Man_t * p, Lpk_Cut_t * pCut, int fLeavesOnly ) +{ + Abc_Obj_t * pObj; + int i; + if ( !fLeavesOnly ) + printf( "LEAVES:\n" ); + Lpk_CutForEachLeaf( p->pNtk, pCut, pObj, i ) + printf( "%d,", pObj->Id ); + if ( !fLeavesOnly ) + { + printf( "\nNODES:\n" ); + Lpk_CutForEachNode( p->pNtk, pCut, pObj, i ) + { + printf( "%d,", pObj->Id ); + assert( Abc_ObjIsNode(pObj) ); + } + printf( "\n" ); + } +} + +/**Function************************************************************* + + Synopsis [Set the cut signature.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Lpk_NodeCutSignature( Lpk_Cut_t * pCut ) +{ + unsigned i; + pCut->uSign[0] = pCut->uSign[1] = 0; + for ( i = 0; i < pCut->nLeaves; i++ ) + { + pCut->uSign[(pCut->pLeaves[i] & 32) > 0] |= (1 << (pCut->pLeaves[i] & 31)); + if ( i != pCut->nLeaves - 1 ) + assert( pCut->pLeaves[i] < pCut->pLeaves[i+1] ); + } +} + + +/**Function************************************************************* + + Synopsis [Computes the set of all cuts.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Lpk_NodeCutsOne( Lpk_Man_t * p, Lpk_Cut_t * pCut, int Node ) +{ + Lpk_Cut_t * pCutNew; + Abc_Obj_t * pObj, * pFanin; + int i, k, j, nLeavesNew; +/* + printf( "Exploring cut " ); + Lpk_NodePrintCut( p, pCut, 1 ); + printf( "with node %d\n", Node ); +*/ + // check if the cut can stand adding one more internal node + if ( pCut->nNodes == LPK_SIZE_MAX ) + return; + + // if the node is a PI, quit + pObj = Abc_NtkObj( p->pNtk, Node ); + if ( Abc_ObjIsCi(pObj) ) + return; + assert( Abc_ObjIsNode(pObj) ); + assert( Abc_ObjFaninNum(pObj) <= p->pPars->nLutSize ); + + // if the node is not in the MFFC, check the limit + if ( !Abc_NodeIsTravIdCurrent(pObj) ) + { + if ( (int)pCut->nNodesDup == p->pPars->nLutsOver ) + return; + assert( (int)pCut->nNodesDup < p->pPars->nLutsOver ); + } + + // check the possibility of adding this node using the signature + nLeavesNew = pCut->nLeaves - 1; + Abc_ObjForEachFanin( pObj, pFanin, i ) + { + if ( (pCut->uSign[(pFanin->Id & 32) > 0] & (1 << (pFanin->Id & 31))) ) + continue; + if ( ++nLeavesNew > p->pPars->nVarsMax ) + return; + } + + // initialize the set of leaves to the nodes in the cut + assert( p->nCuts < LPK_CUTS_MAX ); + pCutNew = p->pCuts + p->nCuts; +/* +if ( p->pObj->Id == 31 && Node == 38 && pCut->pNodes[0] == 31 && pCut->pNodes[1] == 34 && pCut->pNodes[2] == 35 )//p->nCuts == 48 ) +{ + int x = 0; + printf( "Start:\n" ); + Lpk_NodePrintCut( p, pCut ); +} +*/ + pCutNew->nLeaves = 0; + for ( i = 0; i < (int)pCut->nLeaves; i++ ) + if ( pCut->pLeaves[i] != Node ) + pCutNew->pLeaves[pCutNew->nLeaves++] = pCut->pLeaves[i]; + + // add new nodes + Abc_ObjForEachFanin( pObj, pFanin, i ) + { + // find the place where this node belongs + for ( k = 0; k < (int)pCutNew->nLeaves; k++ ) + if ( pCutNew->pLeaves[k] >= pFanin->Id ) + break; + if ( k < (int)pCutNew->nLeaves && pCutNew->pLeaves[k] == pFanin->Id ) + continue; + // check if there is room + if ( (int)pCutNew->nLeaves == p->pPars->nVarsMax ) + return; + // move all the nodes + for ( j = pCutNew->nLeaves; j > k; j-- ) + pCutNew->pLeaves[j] = pCutNew->pLeaves[j-1]; + pCutNew->pLeaves[k] = pFanin->Id; + pCutNew->nLeaves++; + assert( pCutNew->nLeaves <= LPK_SIZE_MAX ); + + } +/* + printf( " Trying cut: " ); + Lpk_NodePrintCut( p, pCutNew, 1 ); + printf( "\n" ); +*/ + // skip the contained cuts + Lpk_NodeCutSignature( pCutNew ); + if ( Lpk_NodeCutsOneFilter( p->pCuts, p->nCuts, pCutNew ) ) + return; + + + // update the set of internal nodes + assert( pCut->nNodes < LPK_SIZE_MAX ); + memcpy( pCutNew->pNodes, pCut->pNodes, pCut->nNodes * sizeof(int) ); + pCutNew->nNodes = pCut->nNodes; + pCutNew->pNodes[ pCutNew->nNodes++ ] = Node; + + // add the marked node + pCutNew->nNodesDup = pCut->nNodesDup + !Abc_NodeIsTravIdCurrent(pObj); +/* +if ( p->pObj->Id == 31 && Node == 38 )//p->nCuts == 48 ) +{ + int x = 0; + printf( "Finish:\n" ); + Lpk_NodePrintCut( p, pCutNew ); +} +*/ + // add the cut to storage + assert( p->nCuts < LPK_CUTS_MAX ); + p->nCuts++; + + assert( pCut->nNodes <= p->nMffc + pCutNew->nNodesDup ); +/* + printf( " Creating cut: " ); + Lpk_NodePrintCut( p, pCutNew, 1 ); + printf( "\n" ); +*/ +} + +/**Function************************************************************* + + Synopsis [Computes the set of all cuts.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Lpk_NodeCuts( Lpk_Man_t * p ) +{ + Lpk_Cut_t * pCut, * pCut2; + int i, k, Temp, nMffc, fChanges; + + // mark the MFFC of the node with the current trav ID + nMffc = p->nMffc = Abc_NodeMffcLabel( p->pObj ); + assert( nMffc > 0 ); + if ( nMffc == 1 ) + return 0; + + // initialize the first cut + pCut = p->pCuts; p->nCuts = 1; + pCut->nNodes = 0; + pCut->nNodesDup = 0; + pCut->nLeaves = 1; + pCut->pLeaves[0] = p->pObj->Id; + // assign the signature + Lpk_NodeCutSignature( pCut ); + + // perform the cut computation + for ( i = 0; i < p->nCuts; i++ ) + { + pCut = p->pCuts + i; + if ( pCut->nLeaves == 0 ) + continue; + // try to expand the fanins of this cut + for ( k = 0; k < (int)pCut->nLeaves; k++ ) + { + // create a new cut + Lpk_NodeCutsOne( p, pCut, pCut->pLeaves[k] ); + // quit if the number of cuts has exceeded the limit + if ( p->nCuts == LPK_CUTS_MAX ) + break; + } + if ( p->nCuts == LPK_CUTS_MAX ) + break; + } + if ( p->nCuts == LPK_CUTS_MAX ) + p->nNodesOver++; + + // record the impact of this node + if ( p->pPars->fSatur ) + Lpk_NodeRecordImpact( p ); + + // compress the cuts by removing empty ones, those with negative Weight, and decomposable ones + p->nEvals = 0; + for ( i = 0; i < p->nCuts; i++ ) + { + pCut = p->pCuts + i; + if ( pCut->nLeaves < 2 ) + continue; + // compute the number of LUTs neede to implement this cut + // V = N * (K-1) + 1 ~~~~~ N = Ceiling[(V-1)/(K-1)] = (V-1)/(K-1) + [(V-1)%(K-1) > 0] + pCut->nLuts = (pCut->nLeaves-1)/(p->pPars->nLutSize-1) + ( (pCut->nLeaves-1)%(p->pPars->nLutSize-1) > 0 ); + pCut->Weight = (float)1.0 * (pCut->nNodes - pCut->nNodesDup) / pCut->nLuts; //p->pPars->nLutsMax; + if ( pCut->Weight <= 1.0 ) + continue; + pCut->fHasDsd = Lpk_NodeCutsCheckDsd( p, pCut ); + if ( pCut->fHasDsd ) + continue; + p->pEvals[p->nEvals++] = i; + } + if ( p->nEvals == 0 ) + return 0; + + // sort the cuts by Weight + do { + fChanges = 0; + for ( i = 0; i < p->nEvals - 1; i++ ) + { + pCut = p->pCuts + p->pEvals[i]; + pCut2 = p->pCuts + p->pEvals[i+1]; + if ( pCut->Weight >= pCut2->Weight ) + continue; + Temp = p->pEvals[i]; + p->pEvals[i] = p->pEvals[i+1]; + p->pEvals[i+1] = Temp; + fChanges = 1; + } + } while ( fChanges ); + return 1; +} + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + + diff --git a/src/opt/lpk/lpkInt.h b/src/opt/lpk/lpkInt.h new file mode 100644 index 00000000..fe442302 --- /dev/null +++ b/src/opt/lpk/lpkInt.h @@ -0,0 +1,161 @@ +/**CFile**************************************************************** + + FileName [lpkInt.h] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [Fast Boolean matching for LUT structures.] + + Synopsis [Internal declarations.] + + Author [Alan Mishchenko] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - April 28, 2007.] + + Revision [$Id: lpkInt.h,v 1.00 2007/04/28 00:00:00 alanmi Exp $] + +***********************************************************************/ + +#ifndef __LPK_INT_H__ +#define __LPK_INT_H__ + +#ifdef __cplusplus +extern "C" { +#endif + +//////////////////////////////////////////////////////////////////////// +/// INCLUDES /// +//////////////////////////////////////////////////////////////////////// + +#include "abc.h" +#include "kit.h" +#include "if.h" +#include "lpk.h" + +//////////////////////////////////////////////////////////////////////// +/// PARAMETERS /// +//////////////////////////////////////////////////////////////////////// + +//////////////////////////////////////////////////////////////////////// +/// BASIC TYPES /// +//////////////////////////////////////////////////////////////////////// + +#define LPK_SIZE_MAX 24 // the largest size of the function +#define LPK_CUTS_MAX 512 // the largest number of cuts considered + +typedef struct Lpk_Man_t_ Lpk_Man_t; +typedef struct Lpk_Cut_t_ Lpk_Cut_t; + +struct Lpk_Cut_t_ +{ + unsigned nLeaves : 6; // (L) the number of leaves + unsigned nNodes : 6; // (M) the number of nodes + unsigned nNodesDup : 6; // (Q) nodes outside of MFFC + unsigned nLuts : 6; // (N) the number of LUTs to try + unsigned unused : 6; // unused + unsigned fHasDsd : 1; // set to 1 if the cut has structural DSD (and so cannot be used) + unsigned fMark : 1; // multipurpose mark + unsigned uSign[2]; // the signature + float Weight; // the weight of the cut: (M - Q)/N(V) (the larger the better) + int Gain; // the gain achieved using this cut + int pLeaves[LPK_SIZE_MAX]; // the leaves of the cut + int pNodes[LPK_SIZE_MAX]; // the nodes of the cut +}; + +struct Lpk_Man_t_ +{ + // parameters + Lpk_Par_t * pPars; // the set of parameters + // current representation + Abc_Ntk_t * pNtk; // the network + Abc_Obj_t * pObj; // the node to resynthesize + // cut representation + int nMffc; // the size of MFFC of the node + int nCuts; // the total number of cuts + int nCutsMax; // the largest possible number of cuts + int nEvals; // the number of good cuts + Lpk_Cut_t pCuts[LPK_CUTS_MAX]; // the storage for cuts + int pEvals[LPK_CUTS_MAX]; // the good cuts + // visited nodes + Vec_Vec_t * vVisited; + // mapping manager + If_Man_t * pIfMan; + Vec_Int_t * vCover; + Vec_Vec_t * vLevels; + // temporary variables + int fCofactoring; // working in the cofactoring mode + int fCalledOnce; // limits the depth of MUX cofactoring + int pRefs[LPK_SIZE_MAX]; // fanin reference counters + int pCands[LPK_SIZE_MAX]; // internal nodes pointing only to the leaves + // truth table representation + Vec_Ptr_t * vTtElems; // elementary truth tables + Vec_Ptr_t * vTtNodes; // storage for temporary truth tables of the nodes + // variable sets + Vec_Int_t * vSets[8]; + // statistics + int nNodesTotal; // total number of nodes + int nNodesOver; // nodes with cuts over the limit + int nCutsTotal; // total number of cuts + int nCutsUseful; // useful cuts + int nGainTotal; // the gain in LUTs + int nChanges; // the number of changed nodes + // counter of non-DSD blocks + int nBlocks[17]; + // rutime + int timeCuts; + int timeTruth; + int timeEval; + int timeMap; + int timeOther; + int timeTotal; +}; + +//////////////////////////////////////////////////////////////////////// +/// MACRO DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + +//////////////////////////////////////////////////////////////////////// +/// ITERATORS /// +//////////////////////////////////////////////////////////////////////// + +#define Lpk_CutForEachLeaf( pNtk, pCut, pObj, i ) \ + for ( i = 0; (i < (int)(pCut)->nLeaves) && (((pObj) = Abc_NtkObj(pNtk, (pCut)->pLeaves[i])), 1); i++ ) +#define Lpk_CutForEachNode( pNtk, pCut, pObj, i ) \ + for ( i = 0; (i < (int)(pCut)->nNodes) && (((pObj) = Abc_NtkObj(pNtk, (pCut)->pNodes[i])), 1); i++ ) +#define Lpk_CutForEachNodeReverse( pNtk, pCut, pObj, i ) \ + for ( i = (int)(pCut)->nNodes - 1; (i >= 0) && (((pObj) = Abc_NtkObj(pNtk, (pCut)->pNodes[i])), 1); i-- ) + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +/*=== lpkCut.c =========================================================*/ +extern unsigned * Lpk_CutTruth( Lpk_Man_t * p, Lpk_Cut_t * pCut ); +extern int Lpk_NodeCuts( Lpk_Man_t * p ); +/*=== lpkMap.c =========================================================*/ +extern Lpk_Man_t * Lpk_ManStart( Lpk_Par_t * pPars ); +extern void Lpk_ManStop( Lpk_Man_t * p ); +/*=== lpkMap.c =========================================================*/ +extern int Lpk_CutExplore( Lpk_Man_t * p, Lpk_Cut_t * pCut, Kit_DsdNtk_t * pNtk ); +extern If_Obj_t * Lpk_MapPrime( Lpk_Man_t * p, unsigned * pTruth, int nVars, If_Obj_t ** ppLeaves ); +extern If_Obj_t * Lpk_MapTree_rec( Lpk_Man_t * p, Kit_DsdNtk_t * pNtk, If_Obj_t ** ppLeaves, int iLit, If_Obj_t * pResult ); +/*=== lpkMulti.c =======================================================*/ +extern If_Obj_t * Lpk_MapTreeMulti( Lpk_Man_t * p, unsigned * pTruth, int nLeaves, If_Obj_t ** ppLeaves ); +/*=== lpkMux.c =========================================================*/ +extern If_Obj_t * Lpk_MapTreeMux_rec( Lpk_Man_t * p, unsigned * pTruth, int nVars, If_Obj_t ** ppLeaves ); +extern If_Obj_t * Lpk_MapSuppRedDec_rec( Lpk_Man_t * p, unsigned * pTruth, int nVars, If_Obj_t ** ppLeaves ); +/*=== lpkSets.c =========================================================*/ +extern unsigned Lpk_MapSuppRedDecSelect( Lpk_Man_t * p, unsigned * pTruth, int nVars, int * piVar, int * piVarReused ); + +#ifdef __cplusplus +} +#endif + +#endif + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + diff --git a/src/opt/lpk/lpkMan.c b/src/opt/lpk/lpkMan.c new file mode 100644 index 00000000..da8b0e3a --- /dev/null +++ b/src/opt/lpk/lpkMan.c @@ -0,0 +1,96 @@ +/**CFile**************************************************************** + + FileName [lpkMan.c] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [Fast Boolean matching for LUT structures.] + + Synopsis [] + + Author [Alan Mishchenko] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - April 28, 2007.] + + Revision [$Id: lpkMan.c,v 1.00 2007/04/28 00:00:00 alanmi Exp $] + +***********************************************************************/ + +#include "lpkInt.h" + +//////////////////////////////////////////////////////////////////////// +/// DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Lpk_Man_t * Lpk_ManStart( Lpk_Par_t * pPars ) +{ + Lpk_Man_t * p; + int i; + assert( pPars->nLutsMax <= 16 ); + assert( pPars->nVarsMax > 0 ); + p = ALLOC( Lpk_Man_t, 1 ); + memset( p, 0, sizeof(Lpk_Man_t) ); + p->pPars = pPars; + p->nCutsMax = LPK_CUTS_MAX; + p->vTtElems = Vec_PtrAllocTruthTables( pPars->nVarsMax ); + p->vTtNodes = Vec_PtrAllocSimInfo( 256, Abc_TruthWordNum(pPars->nVarsMax) ); + p->vCover = Vec_IntAlloc( 1 << 12 ); + for ( i = 0; i < 8; i++ ) + p->vSets[i] = Vec_IntAlloc(100); + return p; +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Lpk_ManStop( Lpk_Man_t * p ) +{ + int i; + for ( i = 0; i < 8; i++ ) + Vec_IntFree(p->vSets[i]); + if ( p->pIfMan ) + { + void * pPars = p->pIfMan->pPars; + If_ManStop( p->pIfMan ); + free( pPars ); + } + if ( p->vLevels ) + Vec_VecFree( p->vLevels ); + if ( p->vVisited ) + Vec_VecFree( p->vVisited ); + Vec_IntFree( p->vCover ); + Vec_PtrFree( p->vTtElems ); + Vec_PtrFree( p->vTtNodes ); + free( p ); +} + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + + diff --git a/src/opt/lpk/lpkMap.c b/src/opt/lpk/lpkMap.c new file mode 100644 index 00000000..c647fdf7 --- /dev/null +++ b/src/opt/lpk/lpkMap.c @@ -0,0 +1,349 @@ +/**CFile**************************************************************** + + FileName [lpkMap.c] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [Fast Boolean matching for LUT structures.] + + Synopsis [] + + Author [Alan Mishchenko] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - April 28, 2007.] + + Revision [$Id: lpkMap.c,v 1.00 2007/04/28 00:00:00 alanmi Exp $] + +***********************************************************************/ + +#include "lpkInt.h" + +//////////////////////////////////////////////////////////////////////// +/// DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +extern void Res_UpdateNetworkLevel( Abc_Obj_t * pObjNew, Vec_Vec_t * vLevels ); + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + +/**Function************************************************************* + + Synopsis [Prepares the mapping manager.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Lpk_IfManStart( Lpk_Man_t * p ) +{ + If_Par_t * pPars; + assert( p->pIfMan == NULL ); + // set defaults + pPars = ALLOC( If_Par_t, 1 ); + memset( pPars, 0, sizeof(If_Par_t) ); + // user-controlable paramters + pPars->nLutSize = p->pPars->nLutSize; + pPars->nCutsMax = 16; + pPars->nFlowIters = 0; // 1 + pPars->nAreaIters = 0; // 1 + pPars->DelayTarget = -1; + pPars->fPreprocess = 0; + pPars->fArea = 1; + pPars->fFancy = 0; + pPars->fExpRed = 0; // + pPars->fLatchPaths = 0; + pPars->fSeqMap = 0; + pPars->fVerbose = 0; + // internal parameters + pPars->fTruth = 0; + pPars->fUsePerm = 0; + pPars->nLatches = 0; + pPars->pLutLib = NULL; // Abc_FrameReadLibLut(); + pPars->pTimesArr = NULL; + pPars->pTimesArr = NULL; + pPars->fUseBdds = 0; + pPars->fUseSops = 0; + pPars->fUseCnfs = 0; + pPars->fUseMv = 0; + // start the mapping manager and set its parameters + p->pIfMan = If_ManStart( pPars ); + If_ManSetupSetAll( p->pIfMan, 1000 ); + p->pIfMan->pPars->pTimesArr = ALLOC( float, 32 ); +} + +/**Function************************************************************* + + Synopsis [Transforms the decomposition graph into the AIG.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +If_Obj_t * Lpk_MapPrimeInternal( If_Man_t * pIfMan, Kit_Graph_t * pGraph ) +{ + Kit_Node_t * pNode; + If_Obj_t * pAnd0, * pAnd1; + int i; + // check for constant function + if ( Kit_GraphIsConst(pGraph) ) + return If_ManConst1(pIfMan); + // check for a literal + if ( Kit_GraphIsVar(pGraph) ) + return Kit_GraphVar(pGraph)->pFunc; + // build the AIG nodes corresponding to the AND gates of the graph + Kit_GraphForEachNode( pGraph, pNode, i ) + { + pAnd0 = Kit_GraphNode(pGraph, pNode->eEdge0.Node)->pFunc; + pAnd1 = Kit_GraphNode(pGraph, pNode->eEdge1.Node)->pFunc; + pNode->pFunc = If_ManCreateAnd( pIfMan, + If_NotCond( If_Regular(pAnd0), If_IsComplement(pAnd0) ^ pNode->eEdge0.fCompl ), + If_NotCond( If_Regular(pAnd1), If_IsComplement(pAnd1) ^ pNode->eEdge1.fCompl ) ); + } + return pNode->pFunc; +} + +/**Function************************************************************* + + Synopsis [Strashes one logic node using its SOP.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +If_Obj_t * Lpk_MapPrime( Lpk_Man_t * p, unsigned * pTruth, int nVars, If_Obj_t ** ppLeaves ) +{ + Kit_Graph_t * pGraph; + Kit_Node_t * pNode; + If_Obj_t * pRes; + int i; + // derive the factored form + pGraph = Kit_TruthToGraph( pTruth, nVars, p->vCover ); + if ( pGraph == NULL ) + return NULL; + // collect the fanins + Kit_GraphForEachLeaf( pGraph, pNode, i ) + pNode->pFunc = ppLeaves[i]; + // perform strashing + pRes = Lpk_MapPrimeInternal( p->pIfMan, pGraph ); + pRes = If_NotCond( pRes, Kit_GraphIsComplement(pGraph) ); + Kit_GraphFree( pGraph ); + return pRes; +} + +/**Function************************************************************* + + Synopsis [Prepares the mapping manager.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Lpk_CutExplore( Lpk_Man_t * p, Lpk_Cut_t * pCut, Kit_DsdNtk_t * pNtk ) +{ + extern Abc_Obj_t * Abc_NodeFromIf_rec( Abc_Ntk_t * pNtkNew, If_Man_t * pIfMan, If_Obj_t * pIfObj, Vec_Int_t * vCover ); + Kit_DsdObj_t * pRoot; + If_Obj_t * pDriver, * ppLeaves[16]; + Abc_Obj_t * pLeaf, * pObjNew; + int nGain, i; +// int nOldShared; + + // check special cases + pRoot = Kit_DsdNtkRoot( pNtk ); + if ( pRoot->Type == KIT_DSD_CONST1 ) + { + if ( Kit_DsdLitIsCompl(pNtk->Root) ) + pObjNew = Abc_NtkCreateNodeConst0( p->pNtk ); + else + pObjNew = Abc_NtkCreateNodeConst1( p->pNtk ); + + // perform replacement + pObjNew->Level = p->pObj->Level; + Abc_ObjReplace( p->pObj, pObjNew ); + Res_UpdateNetworkLevel( pObjNew, p->vLevels ); + p->nGainTotal += pCut->nNodes - pCut->nNodesDup; + return 1; + } + if ( pRoot->Type == KIT_DSD_VAR ) + { + pObjNew = Abc_NtkObj( p->pNtk, pCut->pLeaves[ Kit_DsdLit2Var(pRoot->pFans[0]) ] ); + if ( Kit_DsdLitIsCompl(pNtk->Root) ^ Kit_DsdLitIsCompl(pRoot->pFans[0]) ) + pObjNew = Abc_NtkCreateNodeInv( p->pNtk, pObjNew ); + + // perform replacement + pObjNew->Level = p->pObj->Level; + Abc_ObjReplace( p->pObj, pObjNew ); + Res_UpdateNetworkLevel( pObjNew, p->vLevels ); + p->nGainTotal += pCut->nNodes - pCut->nNodesDup; + return 1; + } + assert( pRoot->Type == KIT_DSD_AND || pRoot->Type == KIT_DSD_XOR || pRoot->Type == KIT_DSD_PRIME ); + + // start the mapping manager + if ( p->pIfMan == NULL ) + Lpk_IfManStart( p ); + + // prepare the mapping manager + If_ManRestart( p->pIfMan ); + // create the PI variables + for ( i = 0; i < p->pPars->nVarsMax; i++ ) + ppLeaves[i] = If_ManCreateCi( p->pIfMan ); + // set the arrival times + Lpk_CutForEachLeaf( p->pNtk, pCut, pLeaf, i ) + p->pIfMan->pPars->pTimesArr[i] = (float)pLeaf->Level; + // prepare the PI cuts + If_ManSetupCiCutSets( p->pIfMan ); + // create the internal nodes + p->fCalledOnce = 0; + pDriver = Lpk_MapTree_rec( p, pNtk, ppLeaves, pNtk->Root, NULL ); + if ( pDriver == NULL ) + return 0; + // create the PO node + If_ManCreateCo( p->pIfMan, If_Regular(pDriver) ); + + // perform mapping + p->pIfMan->pPars->fAreaOnly = 1; + If_ManPerformMappingComb( p->pIfMan ); + + // compute the gain in area + nGain = pCut->nNodes - pCut->nNodesDup - (int)p->pIfMan->AreaGlo; + if ( p->pPars->fVeryVerbose ) + printf( " Mffc = %2d. Mapped = %2d. Gain = %3d. Depth increase = %d.\n", + pCut->nNodes - pCut->nNodesDup, (int)p->pIfMan->AreaGlo, nGain, (int)p->pIfMan->RequiredGlo - (int)p->pObj->Level ); + + // quit if there is no gain + if ( !(nGain > 0 || (p->pPars->fZeroCost && nGain == 0)) ) + return 0; + + // quit if depth increases too much + if ( (int)p->pIfMan->RequiredGlo - (int)p->pObj->Level > p->pPars->nGrowthLevel ) + return 0; + + // perform replacement + p->nGainTotal += nGain; + p->nChanges++; + + // prepare the mapping manager + If_ManCleanNodeCopy( p->pIfMan ); + If_ManCleanCutData( p->pIfMan ); + // set the PIs of the cut + Lpk_CutForEachLeaf( p->pNtk, pCut, pLeaf, i ) + If_ObjSetCopy( If_ManCi(p->pIfMan, i), pLeaf ); + // get the area of mapping + pObjNew = Abc_NodeFromIf_rec( p->pNtk, p->pIfMan, If_Regular(pDriver), p->vCover ); + pObjNew->pData = Hop_NotCond( pObjNew->pData, If_IsComplement(pDriver) ); + + // perform replacement + pObjNew->Level = p->pObj->Level; + Abc_ObjReplace( p->pObj, pObjNew ); + Res_UpdateNetworkLevel( pObjNew, p->vLevels ); + return 1; +} + +/**Function************************************************************* + + Synopsis [Prepares the mapping manager.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +If_Obj_t * Lpk_MapTree_rec( Lpk_Man_t * p, Kit_DsdNtk_t * pNtk, If_Obj_t ** ppLeaves, int iLit, If_Obj_t * pResult ) +{ + Kit_DsdObj_t * pObj; + If_Obj_t * pObjNew, * pFansNew[16]; + unsigned i, iLitFanin; + + assert( iLit >= 0 ); + + // consider the case of a gate + pObj = Kit_DsdNtkObj( pNtk, Kit_DsdLit2Var(iLit) ); + if ( pObj == NULL ) + { + pObjNew = ppLeaves[Kit_DsdLit2Var(iLit)]; + return If_NotCond( pObjNew, Kit_DsdLitIsCompl(iLit) ); + } + if ( pObj->Type == KIT_DSD_CONST1 ) + { + return If_NotCond( If_ManConst1(p->pIfMan), Kit_DsdLitIsCompl(iLit) ); + } + if ( pObj->Type == KIT_DSD_VAR ) + { + pObjNew = ppLeaves[Kit_DsdLit2Var(pObj->pFans[0])]; + return If_NotCond( pObjNew, Kit_DsdLitIsCompl(iLit) ^ Kit_DsdLitIsCompl(pObj->pFans[0]) ); + } + if ( pObj->Type == KIT_DSD_AND ) + { + assert( pObj->nFans == 2 ); + pFansNew[0] = Lpk_MapTree_rec( p, pNtk, ppLeaves, pObj->pFans[0], NULL ); + pFansNew[1] = pResult? pResult : Lpk_MapTree_rec( p, pNtk, ppLeaves, pObj->pFans[1], NULL ); + if ( pFansNew[0] == NULL || pFansNew[1] == NULL ) + return NULL; + pObjNew = If_ManCreateAnd( p->pIfMan, pFansNew[0], pFansNew[1] ); + return If_NotCond( pObjNew, Kit_DsdLitIsCompl(iLit) ); + } + if ( pObj->Type == KIT_DSD_XOR ) + { + int fCompl = Kit_DsdLitIsCompl(iLit); + assert( pObj->nFans == 2 ); + pFansNew[0] = Lpk_MapTree_rec( p, pNtk, ppLeaves, pObj->pFans[0], NULL ); + pFansNew[1] = pResult? pResult : Lpk_MapTree_rec( p, pNtk, ppLeaves, pObj->pFans[1], NULL ); + if ( pFansNew[0] == NULL || pFansNew[1] == NULL ) + return NULL; + fCompl ^= If_IsComplement(pFansNew[0]) ^ If_IsComplement(pFansNew[1]); + pObjNew = If_ManCreateXor( p->pIfMan, If_Regular(pFansNew[0]), If_Regular(pFansNew[1]) ); + return If_NotCond( pObjNew, fCompl ); + } + assert( pObj->Type == KIT_DSD_PRIME ); + p->nBlocks[pObj->nFans]++; + + // solve for the inputs + Kit_DsdObjForEachFanin( pNtk, pObj, iLitFanin, i ) + { + if ( i == 0 ) + pFansNew[i] = pResult? pResult : Lpk_MapTree_rec( p, pNtk, ppLeaves, iLitFanin, NULL ); + else + pFansNew[i] = Lpk_MapTree_rec( p, pNtk, ppLeaves, iLitFanin, NULL ); + if ( pFansNew[i] == NULL ) + return NULL; + } +/* + if ( !p->fCofactoring && p->pPars->nVarsShared > 0 && (int)pObj->nFans > p->pPars->nLutSize ) + { + pObjNew = Lpk_MapTreeMulti( p, Kit_DsdObjTruth(pObj), pObj->nFans, pFansNew ); + return If_NotCond( pObjNew, Kit_DsdLitIsCompl(iLit) ); + } +*/ + + // find best cofactoring variable + if ( pObj->nFans > 3 && !p->fCalledOnce ) +// pObjNew = Lpk_MapTreeMux_rec( p, Kit_DsdObjTruth(pObj), pObj->nFans, pFansNew ); + pObjNew = Lpk_MapSuppRedDec_rec( p, Kit_DsdObjTruth(pObj), pObj->nFans, pFansNew ); + else + pObjNew = Lpk_MapPrime( p, Kit_DsdObjTruth(pObj), pObj->nFans, pFansNew ); + return If_NotCond( pObjNew, Kit_DsdLitIsCompl(iLit) ); +} + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + + diff --git a/src/opt/lpk/lpkMulti.c b/src/opt/lpk/lpkMulti.c new file mode 100644 index 00000000..82cf3578 --- /dev/null +++ b/src/opt/lpk/lpkMulti.c @@ -0,0 +1,495 @@ +/**CFile**************************************************************** + + FileName [lpkMulti.c] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [Fast Boolean matching for LUT structures.] + + Synopsis [] + + Author [Alan Mishchenko] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - April 28, 2007.] + + Revision [$Id: lpkMulti.c,v 1.00 2007/04/28 00:00:00 alanmi Exp $] + +***********************************************************************/ + +#include "lpkInt.h" + +//////////////////////////////////////////////////////////////////////// +/// DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + +/**Function************************************************************* + + Synopsis [Records variable order.] + + Description [Increaments Order[x][y] by 1 if x should be above y in the DSD.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Lpk_CreateVarOrder( Kit_DsdNtk_t * pNtk, char pTable[][16] ) +{ + Kit_DsdObj_t * pObj; + unsigned uSuppFanins, k; + int Above[16], Below[16]; + int nAbove, nBelow, iFaninLit, i, x, y; + // iterate through the nodes + Kit_DsdNtkForEachObj( pNtk, pObj, i ) + { + // collect fanin support of this node + nAbove = 0; + uSuppFanins = 0; + Kit_DsdObjForEachFanin( pNtk, pObj, iFaninLit, k ) + { + if ( Kit_DsdLitIsLeaf( pNtk, iFaninLit ) ) + Above[nAbove++] = Kit_DsdLit2Var(iFaninLit); + else + uSuppFanins |= Kit_DsdLitSupport( pNtk, iFaninLit ); + } + // find the below variables + nBelow = 0; + for ( y = 0; y < 16; y++ ) + if ( uSuppFanins & (1 << y) ) + Below[nBelow++] = y; + // create all pairs + for ( x = 0; x < nAbove; x++ ) + for ( y = 0; y < nBelow; y++ ) + pTable[Above[x]][Below[y]]++; + } +} + +/**Function************************************************************* + + Synopsis [Creates commmon variable order.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Lpk_CreateCommonOrder( char pTable[][16], int piCofVar[], int nCBars, int pPrios[], int nVars, int fVerbose ) +{ + int Score[16] = {0}, pPres[16]; + int i, y, x, iVarBest, ScoreMax, PrioCount; + + // mark the present variables + for ( i = 0; i < nVars; i++ ) + pPres[i] = 1; + // remove cofactored variables + for ( i = 0; i < nCBars; i++ ) + pPres[piCofVar[i]] = 0; + + // compute scores for each leaf + for ( i = 0; i < nVars; i++ ) + { + if ( pPres[i] == 0 ) + continue; + for ( y = 0; y < nVars; y++ ) + Score[i] += pTable[i][y]; + for ( x = 0; x < nVars; x++ ) + Score[i] -= pTable[x][i]; + } + + // print the scores + if ( fVerbose ) + { + printf( "Scores: " ); + for ( i = 0; i < nVars; i++ ) + printf( "%c=%d ", 'a'+i, Score[i] ); + printf( " " ); + printf( "Prios: " ); + } + + // derive variable priority + // variables with equal score receive the same priority + for ( i = 0; i < nVars; i++ ) + pPrios[i] = 16; + + // iterate until variables remain + for ( PrioCount = 1; ; PrioCount++ ) + { + // find the present variable with the highest score + iVarBest = -1; + ScoreMax = -100000; + for ( i = 0; i < nVars; i++ ) + { + if ( pPres[i] == 0 ) + continue; + if ( ScoreMax < Score[i] ) + { + ScoreMax = Score[i]; + iVarBest = i; + } + } + if ( iVarBest == -1 ) + break; + // give the next priority to all vars having this score + if ( fVerbose ) + printf( "%d=", PrioCount ); + for ( i = 0; i < nVars; i++ ) + { + if ( pPres[i] == 0 ) + continue; + if ( Score[i] == ScoreMax ) + { + pPrios[i] = PrioCount; + pPres[i] = 0; + if ( fVerbose ) + printf( "%c", 'a'+i ); + } + } + if ( fVerbose ) + printf( " " ); + } + if ( fVerbose ) + printf( "\n" ); +} + +/**Function************************************************************* + + Synopsis [Finds components with the highest priority.] + + Description [Returns the number of components selected.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Lpk_FindHighest( Kit_DsdNtk_t ** ppNtks, int * piLits, int nSize, int * pPrio, int * pDecision ) +{ + Kit_DsdObj_t * pObj; + unsigned uSupps[8], uSuppFanin, uSuppTotal, uSuppLarge; + int i, pTriv[8], PrioMin, iVarMax, nComps, fOneNonTriv; + + // find individual support and total support + uSuppTotal = 0; + for ( i = 0; i < nSize; i++ ) + { + pTriv[i] = 1; + if ( piLits[i] < 0 ) + uSupps[i] = 0; + else if ( Kit_DsdLitIsLeaf(ppNtks[i], piLits[i]) ) + uSupps[i] = Kit_DsdLitSupport( ppNtks[i], piLits[i] ); + else + { + pObj = Kit_DsdNtkObj( ppNtks[i], Kit_DsdLit2Var(piLits[i]) ); + if ( pObj->Type == KIT_DSD_PRIME ) + { + pTriv[i] = 0; + uSuppFanin = Kit_DsdLitSupport( ppNtks[i], pObj->pFans[0] ); + } + else + { + assert( pObj->nFans == 2 ); + if ( !Kit_DsdLitIsLeaf(ppNtks[i], pObj->pFans[0]) ) + pTriv[i] = 0; + uSuppFanin = Kit_DsdLitSupport( ppNtks[i], pObj->pFans[1] ); + } + uSupps[i] = Kit_DsdLitSupport( ppNtks[i], piLits[i] ) & ~uSuppFanin; + } + assert( uSupps[i] <= 0xFFFF ); + uSuppTotal |= uSupps[i]; + } + if ( uSuppTotal == 0 ) + return 0; + + // find one support variable with the highest priority + PrioMin = ABC_INFINITY; + iVarMax = -1; + for ( i = 0; i < 16; i++ ) + if ( uSuppTotal & (1 << i) ) + if ( PrioMin > pPrio[i] ) + { + PrioMin = pPrio[i]; + iVarMax = i; + } + assert( iVarMax != -1 ); + + // select components, which have this variable + nComps = 0; + fOneNonTriv = 0; + uSuppLarge = 0; + for ( i = 0; i < nSize; i++ ) + if ( uSupps[i] & (1<<iVarMax) ) + { + if ( pTriv[i] || !fOneNonTriv ) + { + if ( !pTriv[i] ) + { + uSuppLarge = uSupps[i]; + fOneNonTriv = 1; + } + pDecision[i] = 1; + nComps++; + } + else + pDecision[i] = 0; + } + else + pDecision[i] = 0; + + // add other non-trivial not-taken components whose support is contained in the current large component support + if ( fOneNonTriv ) + for ( i = 0; i < nSize; i++ ) + if ( !pTriv[i] && pDecision[i] == 0 && (uSupps[i] & ~uSuppLarge) == 0 ) + { + pDecision[i] = 1; + nComps++; + } + + return nComps; +} + +/**Function************************************************************* + + Synopsis [Prepares the mapping manager.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +If_Obj_t * Lpk_MapTreeMulti_rec( Lpk_Man_t * p, Kit_DsdNtk_t ** ppNtks, int * piLits, int * piCofVar, int nCBars, If_Obj_t ** ppLeaves, int nLeaves, int * pPrio ) +{ + Kit_DsdObj_t * pObj; + If_Obj_t * pObjsNew[4][8], * pResPrev; + int piLitsNew[8], pDecision[8]; + int i, k, nComps, nSize; + + // find which of the variables is highest in the order + nSize = (1 << nCBars); + nComps = Lpk_FindHighest( ppNtks, piLits, nSize, pPrio, pDecision ); + if ( nComps == 0 ) + return If_Not( If_ManConst1(p->pIfMan) ); + + // iterate over the nodes + if ( p->pPars->fVeryVerbose ) + printf( "Decision: " ); + for ( i = 0; i < nSize; i++ ) + { + if ( pDecision[i] ) + { + if ( p->pPars->fVeryVerbose ) + printf( "%d ", i ); + assert( piLits[i] >= 0 ); + pObj = Kit_DsdNtkObj( ppNtks[i], Kit_DsdLit2Var(piLits[i]) ); + if ( pObj == NULL ) + piLitsNew[i] = -2; + else if ( pObj->Type == KIT_DSD_PRIME ) + piLitsNew[i] = pObj->pFans[0]; + else + piLitsNew[i] = pObj->pFans[1]; + } + else + piLitsNew[i] = piLits[i]; + } + if ( p->pPars->fVeryVerbose ) + printf( "\n" ); + + // call again + pResPrev = Lpk_MapTreeMulti_rec( p, ppNtks, piLitsNew, piCofVar, nCBars, ppLeaves, nLeaves, pPrio ); + + // create new set of nodes + for ( i = 0; i < nSize; i++ ) + { + if ( pDecision[i] ) + pObjsNew[nCBars][i] = Lpk_MapTree_rec( p, ppNtks[i], ppLeaves, piLits[i], pResPrev ); + else if ( piLits[i] == -1 ) + pObjsNew[nCBars][i] = If_ManConst1(p->pIfMan); + else if ( piLits[i] == -2 ) + pObjsNew[nCBars][i] = If_Not( If_ManConst1(p->pIfMan) ); + else + pObjsNew[nCBars][i] = pResPrev; + } + + // create MUX using these outputs + for ( k = nCBars; k > 0; k-- ) + { + nSize /= 2; + for ( i = 0; i < nSize; i++ ) + pObjsNew[k-1][i] = If_ManCreateMux( p->pIfMan, pObjsNew[k][2*i+0], pObjsNew[k][2*i+1], ppLeaves[piCofVar[k-1]] ); + } + assert( nSize == 1 ); + return pObjsNew[0][0]; +} + +/**Function************************************************************* + + Synopsis [Prepares the mapping manager.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +If_Obj_t * Lpk_MapTreeMulti( Lpk_Man_t * p, unsigned * pTruth, int nVars, If_Obj_t ** ppLeaves ) +{ + static Counter = 0; + If_Obj_t * pResult; + Kit_DsdNtk_t * ppNtks[8] = {0}, * pTemp; + Kit_DsdObj_t * pRoot; + int piCofVar[4], pPrios[16], pFreqs[16] = {0}, piLits[16]; + int i, k, nCBars, nSize, nMemSize; + unsigned * ppCofs[4][8], uSupport; + char pTable[16][16] = {0}; + int fVerbose = p->pPars->fVeryVerbose; + + Counter++; +// printf( "Run %d.\n", Counter ); + + // allocate storage for cofactors + nMemSize = Kit_TruthWordNum(nVars); + ppCofs[0][0] = ALLOC( unsigned, 32 * nMemSize ); + nSize = 0; + for ( i = 0; i < 4; i++ ) + for ( k = 0; k < 8; k++ ) + ppCofs[i][k] = ppCofs[0][0] + nMemSize * nSize++; + assert( nSize == 32 ); + + // find the best cofactoring variables + nCBars = Kit_DsdCofactoring( pTruth, nVars, piCofVar, p->pPars->nVarsShared, 0 ); +// nCBars = 2; +// piCofVar[0] = 0; +// piCofVar[1] = 1; + + + // copy the function + Kit_TruthCopy( ppCofs[0][0], pTruth, nVars ); + + // decompose w.r.t. these variables + for ( k = 0; k < nCBars; k++ ) + { + nSize = (1 << k); + for ( i = 0; i < nSize; i++ ) + { + Kit_TruthCofactor0New( ppCofs[k+1][2*i+0], ppCofs[k][i], nVars, piCofVar[k] ); + Kit_TruthCofactor1New( ppCofs[k+1][2*i+1], ppCofs[k][i], nVars, piCofVar[k] ); + } + } + nSize = (1 << nCBars); + // compute DSD networks + for ( i = 0; i < nSize; i++ ) + { + ppNtks[i] = Kit_DsdDecompose( ppCofs[nCBars][i], nVars ); + ppNtks[i] = Kit_DsdExpand( pTemp = ppNtks[i] ); + Kit_DsdNtkFree( pTemp ); + if ( fVerbose ) + { + printf( "Cof%d%d: ", nCBars, i ); + Kit_DsdPrint( stdout, ppNtks[i] ); + } + } + + // compute variable frequences + for ( i = 0; i < nSize; i++ ) + { + uSupport = Kit_TruthSupport( ppCofs[nCBars][i], nVars ); + for ( k = 0; k < nVars; k++ ) + if ( uSupport & (1<<k) ) + pFreqs[k]++; + } + + // find common variable order + for ( i = 0; i < nSize; i++ ) + { + Kit_DsdGetSupports( ppNtks[i] ); + Lpk_CreateVarOrder( ppNtks[i], pTable ); + } + Lpk_CreateCommonOrder( pTable, piCofVar, nCBars, pPrios, nVars, fVerbose ); + // update priorities with frequences + for ( i = 0; i < nVars; i++ ) + pPrios[i] = pPrios[i] * 256 + (16 - pFreqs[i]) * 16 + i; + + if ( fVerbose ) + printf( "After restructuring with priority:\n" ); + + if ( Counter == 1 ) + { + int x = 0; + } + // transform all networks according to the variable order + for ( i = 0; i < nSize; i++ ) + { + ppNtks[i] = Kit_DsdShrink( pTemp = ppNtks[i], pPrios ); + Kit_DsdNtkFree( pTemp ); + Kit_DsdGetSupports( ppNtks[i] ); + assert( ppNtks[i]->pSupps[0] <= 0xFFFF ); + // undec nodes should be rotated in such a way that the first input has as many shared inputs as possible + Kit_DsdRotate( ppNtks[i], pFreqs ); + // print the resulting networks + if ( fVerbose ) + { + printf( "Cof%d%d: ", nCBars, i ); + Kit_DsdPrint( stdout, ppNtks[i] ); + } + } + + for ( i = 0; i < nSize; i++ ) + { + // collect the roots + pRoot = Kit_DsdNtkRoot(ppNtks[i]); + if ( pRoot->Type == KIT_DSD_CONST1 ) + piLits[i] = Kit_DsdLitIsCompl(ppNtks[i]->Root)? -2: -1; + else if ( pRoot->Type == KIT_DSD_VAR ) + piLits[i] = Kit_DsdLitNotCond( pRoot->pFans[0], Kit_DsdLitIsCompl(ppNtks[i]->Root) ); + else + piLits[i] = ppNtks[i]->Root; + } + + + // recursively construct AIG for mapping + p->fCofactoring = 1; + pResult = Lpk_MapTreeMulti_rec( p, ppNtks, piLits, piCofVar, nCBars, ppLeaves, nVars, pPrios ); + p->fCofactoring = 0; + + if ( fVerbose ) + printf( "\n" ); + + // verify the transformations + nSize = (1 << nCBars); + for ( i = 0; i < nSize; i++ ) + Kit_DsdTruth( ppNtks[i], ppCofs[nCBars][i] ); + // mux the truth tables + for ( k = nCBars-1; k >= 0; k-- ) + { + nSize = (1 << k); + for ( i = 0; i < nSize; i++ ) + Kit_TruthMuxVar( ppCofs[k][i], ppCofs[k+1][2*i+0], ppCofs[k+1][2*i+1], nVars, piCofVar[k] ); + } + if ( !Extra_TruthIsEqual( pTruth, ppCofs[0][0], nVars ) ) + printf( "Verification failed.\n" ); + + + // free the networks + for ( i = 0; i < 8; i++ ) + if ( ppNtks[i] ) + Kit_DsdNtkFree( ppNtks[i] ); + free( ppCofs[0][0] ); + + return pResult; +} + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + + diff --git a/src/opt/lpk/lpkMux.c b/src/opt/lpk/lpkMux.c new file mode 100644 index 00000000..d9e013f0 --- /dev/null +++ b/src/opt/lpk/lpkMux.c @@ -0,0 +1,257 @@ +/**CFile**************************************************************** + + FileName [lpkMux.c] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [Fast Boolean matching for LUT structures.] + + Synopsis [] + + Author [Alan Mishchenko] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - April 28, 2007.] + + Revision [$Id: lpkMux.c,v 1.00 2007/04/28 00:00:00 alanmi Exp $] + +***********************************************************************/ + +#include "lpkInt.h" + +//////////////////////////////////////////////////////////////////////// +/// DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + +/**Function************************************************************* + + Synopsis [Find the best cofactoring variable.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Lpk_MapTreeBestVar( Lpk_Man_t * p, unsigned * pTruth, int nVars ) +{ +// Kit_DsdNtk_t * ppNtks[2], * pTemp; + unsigned * pCof0 = Vec_PtrEntry( p->vTtNodes, 0 ); + unsigned * pCof1 = Vec_PtrEntry( p->vTtNodes, 1 ); + int i, iBestVar, nSuppSizeCur0, nSuppSizeCur1, nSuppSizeCur, nSuppSizeMin; +// int nPrimeSizeCur0, nPrimeSizeCur1, nPrimeSizeCur, nPrimeSizeMin; + + // iterate through variables + iBestVar = -1; + nSuppSizeMin = ABC_INFINITY; +// nPrimeSizeMin = ABC_INFINITY; + for ( i = 0; i < nVars; i++ ) + { + // cofactor the functiona and get support sizes + Kit_TruthCofactor0New( pCof0, pTruth, nVars, i ); + Kit_TruthCofactor1New( pCof1, pTruth, nVars, i ); + nSuppSizeCur0 = Kit_TruthSupportSize( pCof0, nVars ); + nSuppSizeCur1 = Kit_TruthSupportSize( pCof1, nVars ); + nSuppSizeCur = nSuppSizeCur0 + nSuppSizeCur1; +/* + // check the size of the largest prime components + ppNtks[0] = Kit_DsdDecompose( pCof0, nVars ); + ppNtks[1] = Kit_DsdDecompose( pCof1, nVars ); + // compute the largest non-decomp block + nPrimeSizeCur0 = Kit_DsdNonDsdSizeMax(ppNtks[0]); + nPrimeSizeCur1 = Kit_DsdNonDsdSizeMax(ppNtks[1]); + nPrimeSizeCur = KIT_MAX( nPrimeSizeCur0, nPrimeSizeCur1 ); + + printf( "Evaluating variable %c:\n", 'a'+i ); +// Kit_DsdPrintExpanded( ppNtks[0] ); +// Kit_DsdPrintExpanded( ppNtks[1] ); + + ppNtks[0] = Kit_DsdExpand( pTemp = ppNtks[0] ); + Kit_DsdNtkFree( pTemp ); + + ppNtks[1] = Kit_DsdExpand( pTemp = ppNtks[1] ); + Kit_DsdNtkFree( pTemp ); + + Kit_DsdPrint( stdout, ppNtks[0] ); + Kit_DsdPrint( stdout, ppNtks[1] ); + +// Lpk_DsdEvalSets( p, ppNtks[0], ppNtks[1] ); + + // free the networks + Kit_DsdNtkFree( ppNtks[0] ); + Kit_DsdNtkFree( ppNtks[1] ); +*/ + // compare this variable with other variables + if ( nSuppSizeMin > nSuppSizeCur ) //|| (nSuppSizeMin == nSuppSizeCur && nPrimeSizeMin > nPrimeSizeCur ) ) + { + nSuppSizeMin = nSuppSizeCur; +// nPrimeSizeMin = nPrimeSizeCur; + iBestVar = i; + } + } + printf( "\n" ); + assert( iBestVar != -1 ); + return iBestVar; +} + +/**Function************************************************************* + + Synopsis [Maps the function by the best cofactoring.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +If_Obj_t * Lpk_MapTreeMux_rec( Lpk_Man_t * p, unsigned * pTruth, int nVars, If_Obj_t ** ppLeaves ) +{ + If_Obj_t * pObj0, * pObj1; + Kit_DsdNtk_t * ppNtks[2]; + unsigned * pCof0 = Vec_PtrEntry( p->vTtNodes, 0 ); + unsigned * pCof1 = Vec_PtrEntry( p->vTtNodes, 1 ); + int iBestVar; + assert( nVars > 3 ); + p->fCalledOnce = 1; + + // cofactor w.r.t. the best variable + iBestVar = Lpk_MapTreeBestVar( p, pTruth, nVars ); + Kit_TruthCofactor0New( pCof0, pTruth, nVars, iBestVar ); + Kit_TruthCofactor1New( pCof1, pTruth, nVars, iBestVar ); + // decompose the functions + ppNtks[0] = Kit_DsdDecompose( pCof0, nVars ); + ppNtks[1] = Kit_DsdDecompose( pCof1, nVars ); + if ( p->pPars->fVeryVerbose ) + { + printf( "Cofactoring w.r.t. var %c (%d -> %d+%d supp vars):\n", + 'a'+iBestVar, nVars, Kit_TruthSupportSize(pCof0, nVars), Kit_TruthSupportSize(pCof1, nVars) ); + Kit_DsdPrintExpanded( ppNtks[0] ); + Kit_DsdPrintExpanded( ppNtks[1] ); + } + // map the DSD structures + pObj0 = Lpk_MapTree_rec( p, ppNtks[0], ppLeaves, ppNtks[0]->Root, NULL ); + pObj1 = Lpk_MapTree_rec( p, ppNtks[1], ppLeaves, ppNtks[1]->Root, NULL ); + Kit_DsdNtkFree( ppNtks[0] ); + Kit_DsdNtkFree( ppNtks[1] ); + return If_ManCreateMux( p->pIfMan, pObj0, pObj1, ppLeaves[iBestVar] ); +} + + + +/**Function************************************************************* + + Synopsis [Implements support-reducing decomposition.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +If_Obj_t * Lpk_MapSuppRedDec_rec( Lpk_Man_t * p, unsigned * pTruth, int nVars, If_Obj_t ** ppLeaves ) +{ + Kit_DsdNtk_t * pNtkDec, * pNtkComp; + If_Obj_t * pObjNew; + unsigned * pCof0 = Vec_PtrEntry( p->vTtNodes, 0 ); + unsigned * pCof1 = Vec_PtrEntry( p->vTtNodes, 1 ); + unsigned * pDec0 = Vec_PtrEntry( p->vTtNodes, 2 ); + unsigned * pDec1 = Vec_PtrEntry( p->vTtNodes, 3 ); + unsigned * pDec = Vec_PtrEntry( p->vTtNodes, 4 ); + unsigned * pCo00 = Vec_PtrEntry( p->vTtNodes, 5 ); + unsigned * pCo01 = Vec_PtrEntry( p->vTtNodes, 6 ); + unsigned * pCo10 = Vec_PtrEntry( p->vTtNodes, 7 ); + unsigned * pCo11 = Vec_PtrEntry( p->vTtNodes, 8 ); + unsigned * pCo0 = Vec_PtrEntry( p->vTtNodes, 9 ); + unsigned * pCo1 = Vec_PtrEntry( p->vTtNodes, 10 ); + unsigned * pCo = Vec_PtrEntry( p->vTtNodes, 11 ); + int TrueMint0, TrueMint1; + int uSubsets, uSubset0, uSubset1, iVar, iVarReused, i; + + // determine if supp-red decomposition exists + uSubsets = Lpk_MapSuppRedDecSelect( p, pTruth, nVars, &iVar, &iVarReused ); + if ( uSubsets == 0 ) + return NULL; + + // get the bound sets + uSubset0 = uSubsets & 0xFFFF; + uSubset1 = uSubsets >> 16; + // get the cofactors + Kit_TruthCofactor0New( pCof0, pTruth, nVars, iVar ); + Kit_TruthCofactor1New( pCof1, pTruth, nVars, iVar ); + // find any true assignments of the cofactors + TrueMint0 = Kit_TruthFindFirstBit( pCof0, nVars ); + TrueMint1 = Kit_TruthFindFirstBit( pCof1, nVars ); + assert( TrueMint0 >= 0 && TrueMint1 >= 0 ); + // cofactor the cofactors according to these minterms + Kit_TruthCopy( pDec0, pCof0, nVars ); + Kit_TruthCopy( pDec1, pCof1, nVars ); + for ( i = 0; i < nVars; i++ ) + if ( !(uSubset0 & (1 << i)) ) + { + if ( TrueMint0 & (1 << i) ) + Kit_TruthCofactor1( pDec0, nVars, i ); + else + Kit_TruthCofactor0( pDec0, nVars, i ); + } + for ( i = 0; i < nVars; i++ ) + if ( !(uSubset1 & (1 << i)) ) + { + if ( TrueMint1 & (1 << i) ) + Kit_TruthCofactor1( pDec1, nVars, i ); + else + Kit_TruthCofactor0( pDec1, nVars, i ); + } + // get the decomposed function + Kit_TruthMuxVar( pDec, pDec0, pDec1, nVars, iVar ); + + // derive the remainders + Kit_TruthAndPhase( pCo00, pCof0, pDec0, nVars, 0, 1 ); + Kit_TruthAndPhase( pCo01, pCof0, pDec0, nVars, 0, 0 ); + Kit_TruthAndPhase( pCo10, pCof1, pDec1, nVars, 0, 1 ); + Kit_TruthAndPhase( pCo11, pCof1, pDec1, nVars, 0, 0 ); + // quantify bound set variables + for ( i = 0; i < nVars; i++ ) + if ( uSubset0 & (1 << i) ) + { + Kit_TruthExist( pCo00, nVars, i ); + Kit_TruthExist( pCo01, nVars, i ); + } + for ( i = 0; i < nVars; i++ ) + if ( uSubset1 & (1 << i) ) + { + Kit_TruthExist( pCo10, nVars, i ); + Kit_TruthExist( pCo11, nVars, i ); + } + // derive the functions by composing them with the new variable (iVarReused) + Kit_TruthMuxVar( pCo0, pCo00, pCo01, nVars, iVarReused ); + Kit_TruthMuxVar( pCo1, pCo10, pCo11, nVars, iVarReused ); + // derive the composition function + Kit_TruthMuxVar( pCo , pCo0 , pCo1 , nVars, iVar ); + + // process the decomposed function + pNtkDec = Kit_DsdDecompose( pDec, nVars ); + Kit_DsdPrint( stdout, pNtkDec ); + ppLeaves[iVarReused] = Lpk_MapTree_rec( p, pNtkDec, ppLeaves, pNtkDec->Root, NULL ); + Kit_DsdNtkFree( pNtkDec ); + + // process the composition function + pNtkComp = Kit_DsdDecompose( pCo, nVars ); + Kit_DsdPrint( stdout, pNtkComp ); + pObjNew = Lpk_MapTree_rec( p, pNtkComp, ppLeaves, pNtkComp->Root, NULL ); + Kit_DsdNtkFree( pNtkComp ); + return pObjNew; +} + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + + diff --git a/src/opt/lpk/lpkSets.c b/src/opt/lpk/lpkSets.c new file mode 100644 index 00000000..721705cb --- /dev/null +++ b/src/opt/lpk/lpkSets.c @@ -0,0 +1,399 @@ +/**CFile**************************************************************** + + FileName [lpkSets.c] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [Fast Boolean matching for LUT structures.] + + Synopsis [] + + Author [Alan Mishchenko] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - April 28, 2007.] + + Revision [$Id: lpkSets.c,v 1.00 2007/04/28 00:00:00 alanmi Exp $] + +***********************************************************************/ + +#include "lpkInt.h" + +//////////////////////////////////////////////////////////////////////// +/// DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +typedef struct Lpk_Set_t_ Lpk_Set_t; +struct Lpk_Set_t_ +{ + char iVar; // the cofactoring variable + char Over; // the overlap in supports + char SRed; // the support reduction + char Size; // the size of the boundset + unsigned uSubset0; // the first subset (with removed) + unsigned uSubset1; // the second subset (with removed) +}; + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + +/**Function************************************************************* + + Synopsis [Recursively computes decomposable subsets.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +unsigned Lpk_ComputeSets_rec( Kit_DsdNtk_t * p, int iLit, Vec_Int_t * vSets ) +{ + unsigned i, iLitFanin, uSupport, uSuppCur; + Kit_DsdObj_t * pObj; + // consider the case of simple gate + pObj = Kit_DsdNtkObj( p, Kit_DsdLit2Var(iLit) ); + if ( pObj == NULL ) + return (1 << Kit_DsdLit2Var(iLit)); + if ( pObj->Type == KIT_DSD_AND || pObj->Type == KIT_DSD_XOR ) + { + unsigned uSupps[16], Limit, s; + uSupport = 0; + Kit_DsdObjForEachFanin( p, pObj, iLitFanin, i ) + { + uSupps[i] = Lpk_ComputeSets_rec( p, iLitFanin, vSets ); + uSupport |= uSupps[i]; + } + // create all subsets, except empty and full + Limit = (1 << pObj->nFans) - 1; + for ( s = 1; s < Limit; s++ ) + { + uSuppCur = 0; + for ( i = 0; i < pObj->nFans; i++ ) + if ( s & (1 << i) ) + uSuppCur |= uSupps[i]; + Vec_IntPush( vSets, uSuppCur ); + } + return uSupport; + } + assert( pObj->Type == KIT_DSD_PRIME ); + // get the cumulative support of all fanins + uSupport = 0; + Kit_DsdObjForEachFanin( p, pObj, iLitFanin, i ) + { + uSuppCur = Lpk_ComputeSets_rec( p, iLitFanin, vSets ); + uSupport |= uSuppCur; + Vec_IntPush( vSets, uSuppCur ); + } + return uSupport; +} + +/**Function************************************************************* + + Synopsis [Computes the set of subsets of decomposable variables.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +unsigned Lpk_ComputeSets( Kit_DsdNtk_t * p, Vec_Int_t * vSets ) +{ + unsigned uSupport, Entry, i; + assert( p->nVars <= 16 ); + Vec_IntClear( vSets ); + Vec_IntPush( vSets, 0 ); + if ( Kit_DsdNtkRoot(p)->Type == KIT_DSD_CONST1 ) + return 0; + if ( Kit_DsdNtkRoot(p)->Type == KIT_DSD_VAR ) + { + uSupport = ( 1 << Kit_DsdLit2Var(Kit_DsdNtkRoot(p)->pFans[0]) ); + Vec_IntPush( vSets, uSupport ); + return uSupport; + } + uSupport = Lpk_ComputeSets_rec( p, p->Root, vSets ); + assert( (uSupport & 0xFFFF0000) == 0 ); + Vec_IntPush( vSets, uSupport ); + // set the remaining variables + Vec_IntForEachEntry( vSets, Entry, i ) + Vec_IntWriteEntry( vSets, i, Entry | ((uSupport & ~Entry) << 16) ); + return uSupport; +} + +/**Function************************************************************* + + Synopsis [Prints the sets of subsets.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Lpk_PrintSetOne( int uSupport ) +{ + unsigned k; + for ( k = 0; k < 16; k++ ) + if ( uSupport & (1<<k) ) + printf( "%c", 'a'+k ); + printf( " " ); +} +/**Function************************************************************* + + Synopsis [Prints the sets of subsets.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Lpk_PrintSets( Vec_Int_t * vSets ) +{ + unsigned uSupport, i; + printf( "Subsets(%d): ", Vec_IntSize(vSets) ); + Vec_IntForEachEntry( vSets, uSupport, i ) + Lpk_PrintSetOne( uSupport ); + printf( "\n" ); +} + +/**Function************************************************************* + + Synopsis [Computes maximal support reducing bound-sets.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Lpk_ComposeSets( Vec_Int_t * vSets0, Vec_Int_t * vSets1, int nVars, int iCofVar, + Lpk_Set_t * pStore, int * pSize, int nSizeLimit ) +{ + static int nTravId = 0; // the number of the times this is visited + static int TravId[1<<16] = {0}; // last visited + static char SRed[1<<16]; // best support reduction + static char Over[1<<16]; // best overlaps + static unsigned Parents[1<<16]; // best set of parents + static unsigned short Used[1<<16]; // storage for used subsets + int nSuppSize, nSuppOver, nSuppRed, nUsed, nMinOver, i, k, s; + unsigned Entry, Entry0, Entry1; + unsigned uSupp, uSupp0, uSupp1, uSuppTotal; + Lpk_Set_t * pEntry; + + if ( nTravId == (1 << 30) ) + memset( TravId, 0, sizeof(int) * (1 << 16) ); + + // collect support reducing subsets + nUsed = 0; + nTravId++; + uSuppTotal = Kit_BitMask(nVars) & ~(1<<iCofVar); + Vec_IntForEachEntry( vSets0, Entry0, i ) + Vec_IntForEachEntry( vSets1, Entry1, k ) + { + uSupp0 = (Entry0 & 0xFFFF); + uSupp1 = (Entry1 & 0xFFFF); + // skip trivial + if ( uSupp0 == 0 || uSupp1 == 0 || (uSupp0 | uSupp1) == uSuppTotal ) + continue; + if ( Kit_WordHasOneBit(uSupp0) && Kit_WordHasOneBit(uSupp1) ) + continue; + // get the entry + Entry = Entry0 | Entry1; + uSupp = Entry & 0xFFFF; + // set the bound set size + nSuppSize = Kit_WordCountOnes( uSupp ); + // get the number of overlapping vars + nSuppOver = Kit_WordCountOnes( Entry & (Entry >> 16) ); + // get the support reduction + nSuppRed = nSuppSize - 1 - nSuppOver; + // only consider support-reducing subsets + if ( nSuppRed <= 0 ) + continue; + // check if this support is already used + if ( TravId[uSupp] < nTravId ) + { + Used[nUsed++] = uSupp; + + TravId[uSupp] = nTravId; + SRed[uSupp] = nSuppRed; + Over[uSupp] = nSuppOver; + Parents[uSupp] = (k << 16) | i; + } + else if ( TravId[uSupp] == nTravId && SRed[uSupp] < nSuppRed ) + { + TravId[uSupp] = nTravId; + SRed[uSupp] = nSuppRed; + Over[uSupp] = nSuppOver; + Parents[uSupp] = (k << 16) | i; + } + } + + // check if there are non-overlapping + nMinOver = 1000; + for ( s = 0; s < nUsed; s++ ) + if ( nMinOver > Over[Used[s]] ) + nMinOver = Over[Used[s]]; + + + // collect the accumulated ones + for ( s = 0; s < nUsed; s++ ) + if ( Over[Used[s]] == nMinOver ) + { + // save the entry + if ( *pSize == nSizeLimit ) + return; + pEntry = pStore + (*pSize)++; + + i = Parents[Used[s]] & 0xFFFF; + k = Parents[Used[s]] >> 16; + + pEntry->uSubset0 = Vec_IntEntry(vSets0, i); + pEntry->uSubset1 = Vec_IntEntry(vSets1, k); + Entry = pEntry->uSubset0 | pEntry->uSubset1; + + // record the cofactoring variable + pEntry->iVar = iCofVar; + // set the bound set size + pEntry->Size = Kit_WordCountOnes( Entry & 0xFFFF ); + // get the number of overlapping vars + pEntry->Over = Kit_WordCountOnes( Entry & (Entry >> 16) ); + // get the support reduction + pEntry->SRed = pEntry->Size - 1 - pEntry->Over; + assert( pEntry->SRed > 0 ); + } +} + +/**Function************************************************************* + + Synopsis [Prints one set.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Lpk_MapSuppPrintSet( Lpk_Set_t * pSet, int i ) +{ + unsigned Entry; + Entry = pSet->uSubset0 | pSet->uSubset1; + printf( "%2d : ", i ); + printf( "Var = %c ", 'a' + pSet->iVar ); + printf( "Size = %2d ", pSet->Size ); + printf( "Over = %2d ", pSet->Over ); + printf( "SRed = %2d ", pSet->SRed ); + Lpk_PrintSetOne( Entry ); + printf( " " ); + Lpk_PrintSetOne( Entry >> 16 ); + printf( "\n" ); +} + +/**Function************************************************************* + + Synopsis [Evaluates the cofactors.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +unsigned Lpk_MapSuppRedDecSelect( Lpk_Man_t * p, unsigned * pTruth, int nVars, int * piVar, int * piVarReused ) +{ + static int nStoreSize = 256; + static Lpk_Set_t pStore[256], * pSet, * pSetBest; + Kit_DsdNtk_t * ppNtks[2], * pTemp; + Vec_Int_t * vSets0 = p->vSets[0]; + Vec_Int_t * vSets1 = p->vSets[1]; + unsigned * pCof0 = Vec_PtrEntry( p->vTtNodes, 0 ); + unsigned * pCof1 = Vec_PtrEntry( p->vTtNodes, 1 ); + int nSets, i, SizeMax; + unsigned Entry; + + // collect decomposable subsets for each pair of cofactors + nSets = 0; + for ( i = 0; i < nVars; i++ ) + { + printf( "Evaluating variable %c:\n", 'a'+i ); + // evaluate the cofactor pair + Kit_TruthCofactor0New( pCof0, pTruth, nVars, i ); + Kit_TruthCofactor1New( pCof1, pTruth, nVars, i ); + // decompose and expand + ppNtks[0] = Kit_DsdDecompose( pCof0, nVars ); + ppNtks[1] = Kit_DsdDecompose( pCof1, nVars ); + ppNtks[0] = Kit_DsdExpand( pTemp = ppNtks[0] ); Kit_DsdNtkFree( pTemp ); + ppNtks[1] = Kit_DsdExpand( pTemp = ppNtks[1] ); Kit_DsdNtkFree( pTemp ); + Kit_DsdPrint( stdout, ppNtks[0] ); + Kit_DsdPrint( stdout, ppNtks[1] ); + // compute subsets + Lpk_ComputeSets( ppNtks[0], vSets0 ); + Lpk_ComputeSets( ppNtks[1], vSets1 ); + // print subsets + Lpk_PrintSets( vSets0 ); + Lpk_PrintSets( vSets1 ); + // free the networks + Kit_DsdNtkFree( ppNtks[0] ); + Kit_DsdNtkFree( ppNtks[1] ); + // evaluate the pair + Lpk_ComposeSets( vSets0, vSets1, nVars, i, pStore, &nSets, nStoreSize ); + } + + // print the results + printf( "\n" ); + for ( i = 0; i < nSets; i++ ) + Lpk_MapSuppPrintSet( pStore + i, i ); + + // choose the best subset + SizeMax = 0; + pSetBest = NULL; + for ( i = 0; i < nSets; i++ ) + { + pSet = pStore + i; + if ( pSet->Size > p->pPars->nLutSize - 1 ) + continue; + if ( SizeMax < pSet->Size ) + { + pSetBest = pSet; + SizeMax = pSet->Size; + } + } + if ( pSetBest == NULL ) + { + printf( "Could not select a subset.\n" ); + return 0; + } + else + { + printf( "Selected the following subset:\n" ); + Lpk_MapSuppPrintSet( pSetBest, pSetBest - pStore ); + } + + // prepare the return result + // get the remaining variables + Entry = ((pSetBest->uSubset0 >> 16) | (pSetBest->uSubset1 >> 16)); + // get the variables to be removed + Entry = Kit_BitMask(nVars) & ~(1<<pSetBest->iVar) & ~Entry; + // make sure there are some - otherwise it is not supp-red + assert( Entry ); + // remember the first such variable + *piVarReused = Kit_WordFindFirstBit( Entry ); + *piVar = pSetBest->iVar; + return (pSetBest->uSubset1 << 16) | (pSetBest->uSubset0 & 0xFFFF); +} + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + + diff --git a/src/opt/lpk/lpk_.c b/src/opt/lpk/lpk_.c new file mode 100644 index 00000000..d8555e08 --- /dev/null +++ b/src/opt/lpk/lpk_.c @@ -0,0 +1,48 @@ +/**CFile**************************************************************** + + FileName [lpk_.c] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [Fast Boolean matching for LUT structures.] + + Synopsis [] + + Author [Alan Mishchenko] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - April 28, 2007.] + + Revision [$Id: lpk_.c,v 1.00 2007/04/28 00:00:00 alanmi Exp $] + +***********************************************************************/ + +#include "lpkInt.h" + +//////////////////////////////////////////////////////////////////////// +/// DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ + + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + + diff --git a/src/opt/lpk/module.make b/src/opt/lpk/module.make new file mode 100644 index 00000000..9e7bbc7c --- /dev/null +++ b/src/opt/lpk/module.make @@ -0,0 +1,7 @@ +SRC += src/aig/lpk/lpkCore.c \ + src/aig/lpk/lpkCut.c \ + src/aig/lpk/lpkMan.c \ + src/aig/lpk/lpkMap.c \ + src/aig/lpk/lpkMulti.c \ + src/aig/lpk/lpkMux.c \ + src/aig/lpk/lpkSets.c |