diff options
| author | Alan Mishchenko <alanmi@berkeley.edu> | 2008-04-02 08:01:00 -0700 |
|---|---|---|
| committer | Alan Mishchenko <alanmi@berkeley.edu> | 2008-04-02 08:01:00 -0700 |
| commit | 0080244a89eaaccd64c64af8f394486ab5d3e5b5 (patch) | |
| tree | 0a0badb1e94215e0689edf36faeed7d7e9f2b88a | |
| parent | 2c7f6e39b84d29db096388459db7583c01b79b01 (diff) | |
| download | abc-0080244a89eaaccd64c64af8f394486ab5d3e5b5.tar.gz abc-0080244a89eaaccd64c64af8f394486ab5d3e5b5.tar.bz2 abc-0080244a89eaaccd64c64af8f394486ab5d3e5b5.zip | |
Version abc80402
44 files changed, 798 insertions, 295 deletions
@@ -42,7 +42,7 @@ RSC=rc.exe # PROP Ignore_Export_Lib 0 # PROP Target_Dir "" # ADD BASE CPP /nologo /W3 /GX /O2 /D "WIN32" /D "NDEBUG" /D "_CONSOLE" /D "_MBCS" /YX /FD /c -# ADD CPP /nologo /W3 /GX /O2 /I "src/base/abc" /I "src/base/abci" /I "src/base/cmd" /I "src/base/io" /I "src/base/main" /I "src/base/ver" /I "src/bdd/cudd" /I "src/bdd/dsd" /I "src/bdd/epd" /I "src/bdd/mtr" /I "src/bdd/parse" /I "src/bdd/reo" /I "src/bdd/cas" /I "src/map/fpga" /I "src/map/mapper" /I "src/map/mio" /I "src/map/super" /I "src/map/if" /I "src/map/pcm" /I "src/map/ply" /I "src/misc/extra" /I "src/misc/mvc" /I "src/misc/st" /I "src/misc/util" /I "src/misc/espresso" /I "src/misc/nm" /I "src/misc/vec" /I "src/misc/hash" /I "src/opt/cut" /I "src/opt/dec" /I "src/opt/fxu" /I "src/opt/rwr" /I "src/opt/sim" /I "src/opt/ret" /I "src/opt/res" /I "src/opt/lpk" /I "src/sat/bsat" /I "src/sat/csat" /I "src/sat/msat" /I "src/sat/fraig" /I "src/aig/ivy" /I "src/aig/hop" /I "src/aig/rwt" /I "src/aig/deco" /I "src/aig/mem" /I "src/aig/dar" /I "src/aig/fra" /I "src/aig/cnf" /I "src/aig/csw" /I "src/aig/ioa" /I "src/aig/aig" /I "src/aig/kit" /I "src/aig/bdc" /I "src/aig/bar" /I "src/aig/ntl" /I "src/aig/nwk" /I "src/aig/tim" /I "src/opt/mfs" /D "WIN32" /D "NDEBUG" /D "_CONSOLE" /D "_MBCS" /D "__STDC__" /FR /YX /FD /c +# ADD CPP /nologo /W3 /GX /O2 /I "src/base/abc" /I "src/base/abci" /I "src/base/cmd" /I "src/base/io" /I "src/base/main" /I "src/base/ver" /I "src/bdd/cudd" /I "src/bdd/dsd" /I "src/bdd/epd" /I "src/bdd/mtr" /I "src/bdd/parse" /I "src/bdd/reo" /I "src/bdd/cas" /I "src/map/fpga" /I "src/map/mapper" /I "src/map/mio" /I "src/map/super" /I "src/map/if" /I "src/map/pcm" /I "src/map/ply" /I "src/misc/extra" /I "src/misc/mvc" /I "src/misc/st" /I "src/misc/util" /I "src/misc/espresso" /I "src/misc/nm" /I "src/misc/vec" /I "src/misc/hash" /I "src/opt/cut" /I "src/opt/dec" /I "src/opt/fxu" /I "src/opt/rwr" /I "src/opt/sim" /I "src/opt/ret" /I "src/opt/res" /I "src/opt/lpk" /I "src/sat/bsat" /I "src/sat/csat" /I "src/sat/msat" /I "src/sat/fraig" /I "src/aig/ivy" /I "src/aig/hop" /I "src/aig/rwt" /I "src/aig/deco" /I "src/aig/mem" /I "src/aig/dar" /I "src/aig/fra" /I "src/aig/cnf" /I "src/aig/csw" /I "src/aig/ioa" /I "src/aig/aig" /I "src/aig/kit" /I "src/aig/bdc" /I "src/aig/bar" /I "src/aig/ntl" /I "src/aig/nwk" /I "src/aig/tim" /I "src/opt/mfs" /I "src/aig/mfx" /D "WIN32" /D "NDEBUG" /D "_CONSOLE" /D "_MBCS" /D "__STDC__" /FR /YX /FD /c # ADD BASE RSC /l 0x409 /d "NDEBUG" # ADD RSC /l 0x409 /d "NDEBUG" BSC32=bscmake.exe @@ -66,7 +66,7 @@ LINK32=link.exe # PROP Ignore_Export_Lib 0 # PROP Target_Dir "" # ADD BASE CPP /nologo /W3 /Gm /GX /ZI /Od /D "WIN32" /D "_DEBUG" /D "_CONSOLE" /D "_MBCS" /YX /FD /GZ /c -# ADD CPP /nologo /W3 /Gm /GX /ZI /Od /I "src/base/abc" /I "src/base/abci" /I "src/base/cmd" /I "src/base/io" /I "src/base/main" /I "src/base/ver" /I "src/bdd/cudd" /I "src/bdd/dsd" /I "src/bdd/epd" /I "src/bdd/mtr" /I "src/bdd/parse" /I "src/bdd/reo" /I "src/bdd/cas" /I "src/map/fpga" /I "src/map/mapper" /I "src/map/mio" /I "src/map/super" /I "src/map/if" /I "src/map/pcm" /I "src/map/ply" /I "src/misc/extra" /I "src/misc/mvc" /I "src/misc/st" /I "src/misc/util" /I "src/misc/espresso" /I "src/misc/nm" /I "src/misc/vec" /I "src/misc/hash" /I "src/opt/cut" /I "src/opt/dec" /I "src/opt/fxu" /I "src/opt/rwr" /I "src/opt/sim" /I "src/opt/ret" /I "src/opt/res" /I "src/opt/lpk" /I "src/sat/bsat" /I "src/sat/csat" /I "src/sat/msat" /I "src/sat/fraig" /I "src/aig/ivy" /I "src/aig/hop" /I "src/aig/rwt" /I "src/aig/deco" /I "src/aig/mem" /I "src/aig/dar" /I "src/aig/fra" /I "src/aig/cnf" /I "src/aig/csw" /I "src/aig/ioa" /I "src/aig/aig" /I "src/aig/kit" /I "src/aig/bdc" /I "src/aig/bar" /I "src/aig/ntl" /I "src/aig/nwk" /I "src/aig/tim" /I "src/opt/mfs" /D "WIN32" /D "_DEBUG" /D "_CONSOLE" /D "_MBCS" /D "__STDC__" /FR /YX /FD /GZ /c +# ADD CPP /nologo /W3 /Gm /GX /ZI /Od /I "src/base/abc" /I "src/base/abci" /I "src/base/cmd" /I "src/base/io" /I "src/base/main" /I "src/base/ver" /I "src/bdd/cudd" /I "src/bdd/dsd" /I "src/bdd/epd" /I "src/bdd/mtr" /I "src/bdd/parse" /I "src/bdd/reo" /I "src/bdd/cas" /I "src/map/fpga" /I "src/map/mapper" /I "src/map/mio" /I "src/map/super" /I "src/map/if" /I "src/map/pcm" /I "src/map/ply" /I "src/misc/extra" /I "src/misc/mvc" /I "src/misc/st" /I "src/misc/util" /I "src/misc/espresso" /I "src/misc/nm" /I "src/misc/vec" /I "src/misc/hash" /I "src/opt/cut" /I "src/opt/dec" /I "src/opt/fxu" /I "src/opt/rwr" /I "src/opt/sim" /I "src/opt/ret" /I "src/opt/res" /I "src/opt/lpk" /I "src/sat/bsat" /I "src/sat/csat" /I "src/sat/msat" /I "src/sat/fraig" /I "src/aig/ivy" /I "src/aig/hop" /I "src/aig/rwt" /I "src/aig/deco" /I "src/aig/mem" /I "src/aig/dar" /I "src/aig/fra" /I "src/aig/cnf" /I "src/aig/csw" /I "src/aig/ioa" /I "src/aig/aig" /I "src/aig/kit" /I "src/aig/bdc" /I "src/aig/bar" /I "src/aig/ntl" /I "src/aig/nwk" /I "src/aig/tim" /I "src/opt/mfs" /I "src/aig/mfx" /D "WIN32" /D "_DEBUG" /D "_CONSOLE" /D "_MBCS" /D "__STDC__" /FR /YX /FD /GZ /c # SUBTRACT CPP /X # ADD BASE RSC /l 0x409 /d "_DEBUG" # ADD RSC /l 0x409 /d "_DEBUG" diff --git a/src/aig/aig/aig.h b/src/aig/aig/aig.h index 0b3abce7..38fd5190 100644 --- a/src/aig/aig/aig.h +++ b/src/aig/aig/aig.h @@ -444,6 +444,7 @@ extern void Aig_ManCheckPhase( Aig_Man_t * p ); extern Aig_ManCut_t * Aig_ComputeCuts( Aig_Man_t * pAig, int nCutsMax, int nLeafMax, int fTruth, int fVerbose ); extern void Aig_ManCutStop( Aig_ManCut_t * p ); /*=== aigDfs.c ==========================================================*/ +extern int Aig_ManVerifyTopoOrder( Aig_Man_t * p ); extern Vec_Ptr_t * Aig_ManDfs( Aig_Man_t * p ); extern Vec_Vec_t * Aig_ManLevelize( Aig_Man_t * p ); extern Vec_Ptr_t * Aig_ManDfsPio( Aig_Man_t * p ); diff --git a/src/aig/aig/aigDfs.c b/src/aig/aig/aigDfs.c index aebe6c95..95ed1c3a 100644 --- a/src/aig/aig/aigDfs.c +++ b/src/aig/aig/aigDfs.c @@ -19,6 +19,7 @@ ***********************************************************************/ #include "aig.h" +#include "tim.h" //////////////////////////////////////////////////////////////////////// /// DECLARATIONS /// @@ -30,6 +31,79 @@ /**Function************************************************************* + Synopsis [Verifies that the objects are in a topo order.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Aig_ManVerifyTopoOrder( Aig_Man_t * p ) +{ + Aig_Obj_t * pObj, * pNext; + int i, iBox, iTerm1, nTerms; + Aig_ManSetPioNumbers( p ); + Aig_ManIncrementTravId( p ); + Aig_ManForEachObj( p, pObj, i ) + { + if ( Aig_ObjIsNode(pObj) ) + { + pNext = Aig_ObjFanin0(pObj); + if ( !Aig_ObjIsTravIdCurrent(p,pNext) ) + { + printf( "Node %d has fanin %d that is not in a topological order.\n", pObj->Id, pNext->Id ); + return 0; + } + pNext = Aig_ObjFanin1(pObj); + if ( !Aig_ObjIsTravIdCurrent(p,pNext) ) + { + printf( "Node %d has fanin %d that is not in a topological order.\n", pObj->Id, pNext->Id ); + return 0; + } + } + else if ( Aig_ObjIsPo(pObj) ) + { + pNext = Aig_ObjFanin0(pObj); + if ( !Aig_ObjIsTravIdCurrent(p,pNext) ) + { + printf( "Node %d has fanin %d that is not in a topological order.\n", pObj->Id, pNext->Id ); + return 0; + } + } + else if ( Aig_ObjIsPi(pObj) ) + { + if ( p->pManTime ) + { + iBox = Tim_ManBoxForCi( p->pManTime, Aig_ObjPioNum(pObj) ); + if ( iBox >= 0 ) // this is not a true PI + { + iTerm1 = Tim_ManBoxInputFirst( p->pManTime, iBox ); + nTerms = Tim_ManBoxInputNum( p->pManTime, iBox ); + for ( i = 0; i < nTerms; i++ ) + { + pNext = Aig_ManPo( p, iTerm1 + i ); + assert( Tim_ManBoxForCo( p->pManTime, Aig_ObjPioNum(pNext) ) == iBox ); + if ( !Aig_ObjIsTravIdCurrent(p,pNext) ) + { + printf( "Box %d has input %d that is not in a topological order.\n", iBox, pNext->Id ); + return 0; + } + } + } + } + } + else + assert( 0 ); + Aig_ObjSetTravIdCurrent( p, pObj ); + } + Aig_ManCleanPioNumbers( p ); + return 1; +} + +/**Function************************************************************* + Synopsis [Collects internal nodes in the DFS order.] Description [] diff --git a/src/aig/aig/aigFrames.c b/src/aig/aig/aigFrames.c index 4a3b0c7c..f8bc4bda 100644 --- a/src/aig/aig/aigFrames.c +++ b/src/aig/aig/aigFrames.c @@ -59,6 +59,7 @@ Aig_Man_t * Aig_ManFrames( Aig_Man_t * pAig, int nFs, int fInit, int fOuts, int // start the fraig package pFrames = Aig_ManStart( Aig_ManObjNumMax(pAig) * nFs ); pFrames->pName = Aig_UtilStrsav( pAig->pName ); + pFrames->pSpec = Aig_UtilStrsav( pAig->pSpec ); // map constant nodes for ( f = 0; f < nFs; f++ ) Aig_ObjSetFrames( pObjMap, nFs, Aig_ManConst1(pAig), f, Aig_ManConst1(pFrames) ); diff --git a/src/aig/aig/aigHaig.c b/src/aig/aig/aigHaig.c index eaf9fd05..dc083465 100644 --- a/src/aig/aig/aigHaig.c +++ b/src/aig/aig/aigHaig.c @@ -101,6 +101,7 @@ Aig_Man_t * Aig_ManHaigFrames( Aig_Man_t * pHaig, int nFrames ) // start the frames pFrames = Aig_ManStart( Aig_ManObjNumMax(pHaig) * nFrames ); pFrames->pName = Aig_UtilStrsav( pHaig->pName ); + pFrames->pSpec = Aig_UtilStrsav( pHaig->pSpec ); pFrames->nRegs = pHaig->nRegs; // create PI nodes for the frames diff --git a/src/aig/aig/aigMan.c b/src/aig/aig/aigMan.c index 741ecc8d..3dddc687 100644 --- a/src/aig/aig/aigMan.c +++ b/src/aig/aig/aigMan.c @@ -90,6 +90,7 @@ Aig_Man_t * Aig_ManStartFrom( Aig_Man_t * p ) // create the new manager pNew = Aig_ManStart( Aig_ManObjNumMax(p) ); pNew->pName = Aig_UtilStrsav( p->pName ); + pNew->pSpec = Aig_UtilStrsav( p->pSpec ); // create the PIs Aig_ManConst1(p)->pData = Aig_ManConst1(pNew); Aig_ManForEachPi( p, pObj, i ) @@ -122,6 +123,7 @@ Aig_Man_t * Aig_ManDupExor( Aig_Man_t * p ) pNew = Aig_ManStart( Aig_ManObjNumMax(p) ); pNew->fCatchExor = 1; pNew->pName = Aig_UtilStrsav( p->pName ); + pNew->pSpec = Aig_UtilStrsav( p->pSpec ); pNew->nRegs = p->nRegs; pNew->nAsserts = p->nAsserts; if ( p->vFlopNums ) @@ -213,6 +215,7 @@ Aig_Man_t * Aig_ManDup( Aig_Man_t * p, int fOrdered ) // create the new manager pNew = Aig_ManStart( Aig_ManObjNumMax(p) ); pNew->pName = Aig_UtilStrsav( p->pName ); + pNew->pSpec = Aig_UtilStrsav( p->pSpec ); pNew->nRegs = p->nRegs; pNew->nAsserts = p->nAsserts; if ( p->vFlopNums ) @@ -254,7 +257,6 @@ Aig_Man_t * Aig_ManDup( Aig_Man_t * p, int fOrdered ) else { /* - Aig_ManConst1(p)->pData = Aig_ManConst1(pNew); Aig_ManConst1(pNew)->pHaig = Aig_ManConst1(p)->pHaig; Aig_ManForEachObj( p, pObj, i ) @@ -276,6 +278,7 @@ Aig_Man_t * Aig_ManDup( Aig_Man_t * p, int fOrdered ) } } */ + Vec_Vec_t * vLevels; int k; @@ -399,6 +402,7 @@ Aig_Man_t * Aig_ManDup( Aig_Man_t * p, int fOrdered ) // create the new manager pNew = Aig_ManStart( Aig_ManObjNumMax(p) ); pNew->pName = Aig_UtilStrsav( p->pName ); + pNew->pSpec = Aig_UtilStrsav( p->pSpec ); pNew->nRegs = p->nRegs; pNew->nAsserts = p->nAsserts; if ( p->vFlopNums ) @@ -481,6 +485,7 @@ Aig_Man_t * Aig_ManDupWithoutPos( Aig_Man_t * p ) // create the new manager pNew = Aig_ManStart( Aig_ManObjNumMax(p) ); pNew->pName = Aig_UtilStrsav( p->pName ); + pNew->pSpec = Aig_UtilStrsav( p->pSpec ); // create the PIs Aig_ManCleanData( p ); Aig_ManConst1(p)->pData = Aig_ManConst1(pNew); @@ -515,6 +520,7 @@ Aig_Man_t * Aig_ManExtractMiter( Aig_Man_t * p, Aig_Obj_t * pNode1, Aig_Obj_t * // create the new manager pNew = Aig_ManStart( Aig_ManObjNumMax(p) ); pNew->pName = Aig_UtilStrsav( p->pName ); + pNew->pSpec = Aig_UtilStrsav( p->pSpec ); // create the PIs Aig_ManCleanData( p ); Aig_ManConst1(p)->pData = Aig_ManConst1(pNew); diff --git a/src/aig/aig/aigMem.c b/src/aig/aig/aigMem.c index dab90777..80a5ceb5 100644 --- a/src/aig/aig/aigMem.c +++ b/src/aig/aig/aigMem.c @@ -64,10 +64,14 @@ struct Aig_MmFlex_t_ struct Aig_MmStep_t_ { - int nMems; // the number of fixed memory managers employed + int nMems; // the number of fixed memory managers employed Aig_MmFixed_t ** pMems; // memory managers: 2^1 words, 2^2 words, etc - int nMapSize; // the size of the memory array + int nMapSize; // the size of the memory array Aig_MmFixed_t ** pMap; // maps the number of bytes into its memory manager + // additional memory chunks + int nChunksAlloc; // the maximum number of memory chunks + int nChunks; // the current number of memory chunks + char ** pChunks; // the allocated memory }; #define ALLOC(type, num) ((type *) malloc(sizeof(type) * (num))) @@ -486,6 +490,9 @@ Aig_MmStep_t * Aig_MmStepStart( int nSteps ) p->pMap[k] = p->pMems[i]; //for ( i = 1; i < 100; i ++ ) //printf( "%10d: size = %10d\n", i, p->pMap[i]->nEntrySize ); + p->nChunksAlloc = 64; + p->nChunks = 0; + p->pChunks = ALLOC( char *, p->nChunksAlloc ); return p; } @@ -505,12 +512,12 @@ void Aig_MmStepStop( Aig_MmStep_t * p, int fVerbose ) int i; for ( i = 0; i < p->nMems; i++ ) Aig_MmFixedStop( p->pMems[i], fVerbose ); -// if ( p->pLargeChunks ) -// { -// for ( i = 0; i < p->nLargeChunks; i++ ) -// free( p->pLargeChunks[i] ); -// free( p->pLargeChunks ); -// } + if ( p->nChunksAlloc ) + { + for ( i = 0; i < p->nChunks; i++ ) + free( p->pChunks[i] ); + free( p->pChunks ); + } free( p->pMems ); free( p->pMap ); free( p ); @@ -533,19 +540,13 @@ char * Aig_MmStepEntryFetch( Aig_MmStep_t * p, int nBytes ) return NULL; if ( nBytes > p->nMapSize ) { -// printf( "Allocating %d bytes.\n", nBytes ); -/* - if ( p->nLargeChunks == p->nLargeChunksAlloc ) + if ( p->nChunks == p->nChunksAlloc ) { - if ( p->nLargeChunksAlloc == 0 ) - p->nLargeChunksAlloc = 5; - p->nLargeChunksAlloc *= 2; - p->pLargeChunks = REALLOC( char *, p->pLargeChunks, p->nLargeChunksAlloc ); + p->nChunksAlloc *= 2; + p->pChunks = REALLOC( char *, p->pChunks, p->nChunksAlloc ); } - p->pLargeChunks[ p->nLargeChunks++ ] = ALLOC( char, nBytes ); - return p->pLargeChunks[ p->nLargeChunks - 1 ]; -*/ - return ALLOC( char, nBytes ); + p->pChunks[ p->nChunks++ ] = ALLOC( char, nBytes ); + return p->pChunks[p->nChunks-1]; } return Aig_MmFixedEntryFetch( p->pMap[nBytes] ); } @@ -568,7 +569,7 @@ void Aig_MmStepEntryRecycle( Aig_MmStep_t * p, char * pEntry, int nBytes ) return; if ( nBytes > p->nMapSize ) { - free( pEntry ); +// free( pEntry ); return; } Aig_MmFixedEntryRecycle( p->pMap[nBytes], pEntry ); diff --git a/src/aig/aig/aigObj.c b/src/aig/aig/aigObj.c index 2f92f720..d02e3228 100644 --- a/src/aig/aig/aigObj.c +++ b/src/aig/aig/aigObj.c @@ -142,6 +142,7 @@ void Aig_ObjConnect( Aig_Man_t * p, Aig_Obj_t * pObj, Aig_Obj_t * pFan0, Aig_Obj // add the node to the dynamically updated topological order // if ( p->pOrderData && Aig_ObjIsNode(pObj) ) // Aig_ObjOrderInsert( p, pObj->Id ); + assert( !Aig_ObjIsNode(pObj) || pObj->Level > 0 ); } /**Function************************************************************* diff --git a/src/aig/aig/aigPart.c b/src/aig/aig/aigPart.c index 2a9800cf..4ce36245 100644 --- a/src/aig/aig/aigPart.c +++ b/src/aig/aig/aigPart.c @@ -1494,7 +1494,7 @@ void Aig_ManChoiceLevel_rec( Aig_Man_t * pNew, Aig_Obj_t * pObj ) LevelMax++; // get the level of the nodes in the choice node - if ( pNew->pEquivs && (pNext = pNew->pEquivs[pObj->iData]) ) + if ( pNew->pEquivs && (pNext = pNew->pEquivs[pObj->Id]) ) { Aig_ManChoiceLevel_rec( pNew, pNext ); if ( LevelMax < Aig_ObjLevel(pNext) ) @@ -1504,6 +1504,7 @@ void Aig_ManChoiceLevel_rec( Aig_Man_t * pNew, Aig_Obj_t * pObj ) else assert( 0 ); Aig_ObjSetLevel( pObj, LevelMax ); + assert( !Aig_ObjIsNode(pObj) || LevelMax > 0 ); } /**Function************************************************************* @@ -1546,6 +1547,46 @@ int Aig_ManChoiceLevel( Aig_Man_t * pNew ) SeeAlso [] ***********************************************************************/ +void Aig_ManChoiceEval( Aig_Man_t * p ) +{ + Vec_Ptr_t * vSupp; + Aig_Obj_t * pNode, * pTemp; + int i, Counter; + + vSupp = Vec_PtrAlloc( 100 ); + Aig_ManForEachNode( p, pNode, i ) + { + if ( !Aig_ObjIsChoice(p, pNode) ) + continue; + if ( pNode->Id == 4225 ) + { + int x = 0; + } + Counter = 0; + for ( pTemp = pNode; pTemp; pTemp = p->pEquivs[pTemp->Id] ) + Counter++; + printf( "Choice node = %5d. Level = %2d. Choices = %d. { ", pNode->Id, pNode->Level, Counter ); + for ( pTemp = pNode; pTemp; pTemp = p->pEquivs[pTemp->Id] ) + { + Counter = Aig_NodeMffsSupp( p, pTemp, 0, vSupp ); + printf( "S=%d N=%d L=%d ", Vec_PtrSize(vSupp), Counter, pTemp->Level ); + } + printf( "}\n" ); + } + Vec_PtrFree( vSupp ); +} + +/**Function************************************************************* + + Synopsis [Constructively accumulates choices.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ Aig_Man_t * Aig_ManChoiceConstructive( Vec_Ptr_t * vAigs, int fVerbose ) { Aig_Man_t * pNew, * pThis, * pPrev; @@ -1573,6 +1614,7 @@ Aig_Man_t * Aig_ManChoiceConstructive( Vec_Ptr_t * vAigs, int fVerbose ) //Aig_ManPrintStats( pNew ); // reset levels Aig_ManChoiceLevel( pNew ); +// Aig_ManChoiceEval( pNew ); return pNew; } diff --git a/src/aig/aig/aigRepr.c b/src/aig/aig/aigRepr.c index eb4325f4..eff31fff 100644 --- a/src/aig/aig/aigRepr.c +++ b/src/aig/aig/aigRepr.c @@ -269,6 +269,7 @@ Aig_Man_t * Aig_ManDupRepr( Aig_Man_t * p, int fOrdered ) // start the HOP package pNew = Aig_ManStart( Aig_ManObjNumMax(p) ); pNew->pName = Aig_UtilStrsav( p->pName ); + pNew->pSpec = Aig_UtilStrsav( p->pSpec ); pNew->nRegs = p->nRegs; if ( p->vFlopNums ) pNew->vFlopNums = Vec_IntDup( p->vFlopNums ); diff --git a/src/aig/aig/aigRet.c b/src/aig/aig/aigRet.c index d1784b1b..e20b1d4f 100644 --- a/src/aig/aig/aigRet.c +++ b/src/aig/aig/aigRet.c @@ -950,6 +950,7 @@ clk = clock(); // get the new manager pNew = Rtm_ManToAig( pRtm ); pNew->pName = Aig_UtilStrsav( p->pName ); + pNew->pSpec = Aig_UtilStrsav( p->pSpec ); Rtm_ManFree( pRtm ); // group the registers clk = clock(); diff --git a/src/aig/aig/aigScl.c b/src/aig/aig/aigScl.c index d8ffda9a..92bfcd28 100644 --- a/src/aig/aig/aigScl.c +++ b/src/aig/aig/aigScl.c @@ -48,6 +48,7 @@ Aig_Man_t * Aig_ManRemap( Aig_Man_t * p, Vec_Ptr_t * vMap ) // create the new manager pNew = Aig_ManStart( Aig_ManObjNumMax(p) ); pNew->pName = Aig_UtilStrsav( p->pName ); + pNew->pSpec = Aig_UtilStrsav( p->pSpec ); pNew->nRegs = p->nRegs; pNew->nAsserts = p->nAsserts; if ( p->vFlopNums ) diff --git a/src/aig/dar/dar.h b/src/aig/dar/dar.h index 1cc239b1..99c0276d 100644 --- a/src/aig/dar/dar.h +++ b/src/aig/dar/dar.h @@ -80,6 +80,7 @@ extern void Dar_LibStart(); extern void Dar_LibStop(); /*=== darBalance.c ========================================================*/ extern Aig_Man_t * Dar_ManBalance( Aig_Man_t * p, int fUpdateLevel ); +extern Aig_Man_t * Dar_ManBalanceXor( Aig_Man_t * pAig, int fExor, int fUpdateLevel, int fVerbose ); extern void Dar_BalancePrintStats( Aig_Man_t * p ); /*=== darCore.c ========================================================*/ extern void Dar_ManDefaultRwrParams( Dar_RwrPar_t * pPars ); @@ -94,7 +95,6 @@ extern Aig_Man_t * Dar_ManRwsat( Aig_Man_t * pAig, int fBalance, int fVerbos extern Aig_Man_t * Dar_ManCompress( Aig_Man_t * pAig, int fBalance, int fUpdateLevel, int fVerbose ); extern Aig_Man_t * Dar_ManCompress2( Aig_Man_t * pAig, int fBalance, int fUpdateLevel, int fFanout, int fVerbose ); extern Aig_Man_t * Dar_ManChoice( Aig_Man_t * pAig, int fBalance, int fUpdateLevel, int fConstruct, int nConfMax, int nLevelMax, int fVerbose ); -extern Aig_Man_t * Dar_ManBalanceXor( Aig_Man_t * pAig, int fExor, int fUpdateLevel, int fVerbose ); #ifdef __cplusplus } diff --git a/src/aig/dar/darBalance.c b/src/aig/dar/darBalance.c index 63f6f232..6e78041a 100644 --- a/src/aig/dar/darBalance.c +++ b/src/aig/dar/darBalance.c @@ -333,7 +333,7 @@ Aig_Obj_t * Dar_Balance_rec( Aig_Man_t * pNew, Aig_Obj_t * pObjOld, Vec_Vec_t * if ( vSuper->nSize == 0 ) return pObjOld->pData = Aig_ManConst0(pNew); if ( Vec_PtrSize(vSuper) < 2 ) - printf( "BUG!\n" ); + printf( "Dar_Balance_rec: Internal error!\n" ); // for each old node, derive the new well-balanced node for ( i = 0; i < Vec_PtrSize(vSuper); i++ ) { @@ -366,9 +366,11 @@ Aig_Man_t * Dar_ManBalance( Aig_Man_t * p, int fUpdateLevel ) Aig_Obj_t * pObj, * pDriver, * pObjNew; Vec_Vec_t * vStore; int i; + assert( Aig_ManVerifyTopoOrder(p) ); // create the new manager pNew = Aig_ManStart( Aig_ManObjNumMax(p) ); pNew->pName = Aig_UtilStrsav( p->pName ); + pNew->pSpec = Aig_UtilStrsav( p->pSpec ); pNew->nRegs = p->nRegs; pNew->nAsserts = p->nAsserts; if ( p->vFlopNums ) @@ -439,6 +441,35 @@ Aig_Man_t * Dar_ManBalance( Aig_Man_t * p, int fUpdateLevel ) /**Function************************************************************* + Synopsis [Reproduces script "compress2".] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Aig_Man_t * Dar_ManBalanceXor( Aig_Man_t * pAig, int fExor, int fUpdateLevel, int fVerbose ) +{ + Aig_Man_t * pAigXor, * pRes; + if ( fExor ) + { + pAigXor = Aig_ManDupExor( pAig ); + if ( fVerbose ) + Dar_BalancePrintStats( pAigXor ); + pRes = Dar_ManBalance( pAigXor, fUpdateLevel ); + Aig_ManStop( pAigXor ); + } + else + { + pRes = Dar_ManBalance( pAig, fUpdateLevel ); + } + return pRes; +} + +/**Function************************************************************* + Synopsis [Inserts a new node in the order by levels.] Description [] diff --git a/src/aig/dar/darScript.c b/src/aig/dar/darScript.c index 2a0aa7d5..7d78bf40 100644 --- a/src/aig/dar/darScript.c +++ b/src/aig/dar/darScript.c @@ -341,11 +341,19 @@ Vec_Ptr_t * Dar_ManChoiceSynthesis( Aig_Man_t * pAig, int fBalance, int fUpdateL //Aig_ManPrintStats( pAig ); Aig_ManForEachObj( pAig, pObj, i ) + { + pObj->pNext = pObj->pHaig; pObj->pHaig = pObj; + } pAig = Dar_ManCompress2(pAig, fBalance, fUpdateLevel, 1, fVerbose); Vec_PtrPush( vAigs, pAig ); //Aig_ManPrintStats( pAig ); + + pAig = Vec_PtrEntry( vAigs, 1 ); + Aig_ManForEachObj( pAig, pObj, i ) + pObj->pHaig = pObj->pNext; + return vAigs; } @@ -399,35 +407,6 @@ PRT( "Choicing time ", clock() - clk ); // return NULL; } -/**Function************************************************************* - - Synopsis [Reproduces script "compress2".] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -Aig_Man_t * Dar_ManBalanceXor( Aig_Man_t * pAig, int fExor, int fUpdateLevel, int fVerbose ) -{ - Aig_Man_t * pAigXor, * pRes; - if ( fExor ) - { - pAigXor = Aig_ManDupExor( pAig ); - if ( fVerbose ) - Dar_BalancePrintStats( pAigXor ); - pRes = Dar_ManBalance( pAigXor, fUpdateLevel ); - Aig_ManStop( pAigXor ); - } - else - { - pRes = Dar_ManBalance( pAig, fUpdateLevel ); - } - return pRes; -} - //////////////////////////////////////////////////////////////////////// /// END OF FILE /// //////////////////////////////////////////////////////////////////////// diff --git a/src/aig/fra/fraBmc.c b/src/aig/fra/fraBmc.c index cf026fac..9b975b82 100644 --- a/src/aig/fra/fraBmc.c +++ b/src/aig/fra/fraBmc.c @@ -241,6 +241,7 @@ Aig_Man_t * Fra_BmcFrames( Fra_Bmc_t * p, int fKeepPos ) // start the fraig package pAigFrames = Aig_ManStart( Aig_ManObjNumMax(p->pAig) * p->nFramesAll ); pAigFrames->pName = Aig_UtilStrsav( p->pAig->pName ); + pAigFrames->pSpec = Aig_UtilStrsav( p->pAig->pSpec ); // create PI nodes for the frames for ( f = 0; f < p->nFramesAll; f++ ) Bmc_ObjSetFrames( Aig_ManConst1(p->pAig), f, Aig_ManConst1(pAigFrames) ); diff --git a/src/aig/fra/fraClass.c b/src/aig/fra/fraClass.c index baae7c3f..498ea758 100644 --- a/src/aig/fra/fraClass.c +++ b/src/aig/fra/fraClass.c @@ -801,6 +801,7 @@ Aig_Man_t * Fra_ClassesDeriveAig( Fra_Cla_t * p, int nFramesK ) // start the fraig package pManFraig = Aig_ManStart( Aig_ManObjNumMax(p->pAig) * nFramesAll ); pManFraig->pName = Aig_UtilStrsav( p->pAig->pName ); + pManFraig->pSpec = Aig_UtilStrsav( p->pAig->pSpec ); // allocate place for the node mapping ppEquivs = ALLOC( Aig_Obj_t *, Aig_ManObjNumMax(p->pAig) ); Fra_ObjSetEqu( ppEquivs, Aig_ManConst1(p->pAig), Aig_ManConst1(pManFraig) ); diff --git a/src/aig/fra/fraInd.c b/src/aig/fra/fraInd.c index 1ac2adab..8b9e863e 100644 --- a/src/aig/fra/fraInd.c +++ b/src/aig/fra/fraInd.c @@ -134,6 +134,7 @@ Aig_Man_t * Fra_FramesWithClasses( Fra_Man_t * p ) // start the fraig package pManFraig = Aig_ManStart( Aig_ManObjNumMax(p->pManAig) * p->nFramesAll ); pManFraig->pName = Aig_UtilStrsav( p->pManAig->pName ); + pManFraig->pSpec = Aig_UtilStrsav( p->pManAig->pSpec ); pManFraig->nRegs = p->pManAig->nRegs; // create PI nodes for the frames for ( f = 0; f < p->nFramesAll; f++ ) diff --git a/src/aig/fra/fraMan.c b/src/aig/fra/fraMan.c index b06f98d4..720260a5 100644 --- a/src/aig/fra/fraMan.c +++ b/src/aig/fra/fraMan.c @@ -178,6 +178,7 @@ Aig_Man_t * Fra_ManPrepareComb( Fra_Man_t * p ) // start the fraig package pManFraig = Aig_ManStart( Aig_ManObjNumMax(p->pManAig) ); pManFraig->pName = Aig_UtilStrsav( p->pManAig->pName ); + pManFraig->pSpec = Aig_UtilStrsav( p->pManAig->pSpec ); pManFraig->nRegs = p->pManAig->nRegs; pManFraig->nAsserts = p->pManAig->nAsserts; // set the pointers to the available fraig nodes diff --git a/src/aig/kit/kitDsd.c b/src/aig/kit/kitDsd.c index e24a9964..a397d452 100644 --- a/src/aig/kit/kitDsd.c +++ b/src/aig/kit/kitDsd.c @@ -2111,8 +2111,8 @@ void Kit_DsdTest( unsigned * pTruth, int nVars ) // if ( Kit_DsdNtkRoot(pNtk)->nFans == (unsigned)nVars && nVars == 6 ) - printf( "\n" ); - Kit_DsdPrint( stdout, pNtk ); +// printf( "\n" ); +// Kit_DsdPrint( stdout, pNtk ); pNtk = Kit_DsdExpand( pTemp = pNtk ); Kit_DsdNtkFree( pTemp ); diff --git a/src/aig/mem/mem.c b/src/aig/mem/mem.c index f5bfbfd8..911ceffb 100644 --- a/src/aig/mem/mem.c +++ b/src/aig/mem/mem.c @@ -574,7 +574,7 @@ void Mem_StepEntryRecycle( Mem_Step_t * p, char * pEntry, int nBytes ) return; if ( nBytes > p->nMapSize ) { - free( pEntry ); +// free( pEntry ); return; } Mem_FixedEntryRecycle( p->pMap[nBytes], pEntry ); diff --git a/src/aig/mfx/mfxCore.c b/src/aig/mfx/mfxCore.c index 4c8988cc..6e47c986 100644 --- a/src/aig/mfx/mfxCore.c +++ b/src/aig/mfx/mfxCore.c @@ -19,6 +19,7 @@ ***********************************************************************/ #include "mfxInt.h" +#include "bar.h" //////////////////////////////////////////////////////////////////////// /// DECLARATIONS /// @@ -83,8 +84,8 @@ p->timeWin += clock() - clk; return 1; // compute the divisors of the window clk = clock(); -// p->vDivs = Mfx_ComputeDivisors( p, pNode, Nwk_ObjRequired(pNode) - If_LutLibSlowestPinDelay(pNode->pMan->pLutLib) ); - p->vDivs = Mfx_ComputeDivisors( p, pNode, AIG_INFINITY ); + p->vDivs = Mfx_ComputeDivisors( p, pNode, Nwk_ObjRequired(pNode) - If_LutLibSlowestPinDelay(pNode->pMan->pLutLib) ); +// p->vDivs = Mfx_ComputeDivisors( p, pNode, AIG_INFINITY ); p->nTotalDivs += Vec_PtrSize(p->vDivs); p->timeDiv += clock() - clk; // construct AIG for the window @@ -192,10 +193,10 @@ p->timeSat += clock() - clk; SeeAlso [] ***********************************************************************/ -int Mfx_Perform( Nwk_Man_t * pNtk, Mfx_Par_t * pPars ) +int Mfx_Perform( Nwk_Man_t * pNtk, Mfx_Par_t * pPars, If_Lib_t * pLutLib ) { Bdc_Par_t Pars = {0}, * pDecPars = &Pars; -// ProgressBar * pProgress; + Bar_Progress_t * pProgress; Mfx_Man_t * p; Tim_Man_t * pManTimeOld = NULL; Nwk_Obj_t * pObj; @@ -223,23 +224,19 @@ int Mfx_Perform( Nwk_Man_t * pNtk, Mfx_Par_t * pPars ) nFaninMax = MFX_FANIN_MAX; } } - -/* - // prepare timing information - if ( pNtk->pManTime ) + if ( pLutLib && pLutLib->LutMax < nFaninMax ) { - // compute levels - Nwk_ManLevel( pNtk ); - // compute delay trace with white-boxes - Nwk_ManDelayTraceLut( pNtk, pNtk->pLutLib ); - // save the general timing manager - pManTimeOld = pNtk->pManTime; - // derive an approximate timing manager without white-boxes - pNtk->pManTime = Tim_ManDupApprox( pNtk->pManTime ); + printf( "The selected LUT library with max LUT size (%d) cannot be used to compute timing for network with %d-input nodes. Using unit-delay model.\n", pLutLib->LutMax, nFaninMax ); + pLutLib = NULL; } - // compute delay trace with the given timing manager - Nwk_ManDelayTraceLut( pNtk, pNtk->pLutLib ); -*/ + pNtk->pLutLib = pLutLib; + + // compute levels + Nwk_ManLevel( pNtk ); + assert( Nwk_ManVerifyLevel( pNtk ) ); + // compute delay trace with white-boxes + Nwk_ManDelayTraceLut( pNtk ); + assert( Nwk_ManVerifyTiming( pNtk ) ); // start the manager p = Mfx_ManAlloc( pPars ); @@ -259,27 +256,27 @@ int Mfx_Perform( Nwk_Man_t * pNtk, Mfx_Par_t * pPars ) p->nTotalEdgesBeg = nTotalEdgesBeg; if ( pPars->fResub ) { -// pProgress = Extra_ProgressBarStart( stdout, Nwk_ObjNumMax(pNtk) ); + pProgress = Bar_ProgressStart( stdout, Nwk_ManObjNumMax(pNtk) ); Nwk_ManForEachNode( pNtk, pObj, i ) { if ( p->pPars->nDepthMax && pObj->Level > p->pPars->nDepthMax ) continue; if ( Nwk_ObjFaninNum(pObj) < 2 || Nwk_ObjFaninNum(pObj) > nFaninMax ) continue; -// if ( !p->pPars->fVeryVerbose ) -// Extra_ProgressBarUpdate( pProgress, i, NULL ); + if ( !p->pPars->fVeryVerbose ) + Bar_ProgressUpdate( pProgress, i, NULL ); Mfx_Resub( p, pObj ); } -// Extra_ProgressBarStop( pProgress ); + Bar_ProgressStop( pProgress ); } else { -// pProgress = Extra_ProgressBarStart( stdout, Nwk_NodeNum(pNtk) ); + pProgress = Bar_ProgressStart( stdout, Nwk_ManNodeNum(pNtk) ); vLevels = Nwk_ManLevelize( pNtk ); Vec_VecForEachLevelStart( vLevels, vNodes, k, 1 ) { -// if ( !p->pPars->fVeryVerbose ) -// Extra_ProgressBarUpdate( pProgress, nNodes, NULL ); + if ( !p->pPars->fVeryVerbose ) + Bar_ProgressUpdate( pProgress, nNodes, NULL ); p->nNodesGainedLevel = 0; p->nTotConfLevel = 0; p->nTimeOutsLevel = 0; @@ -303,20 +300,15 @@ int Mfx_Perform( Nwk_Man_t * pNtk, Mfx_Par_t * pPars ) PRT( "Time", clock() - clk2 ); } } -// Extra_ProgressBarStop( pProgress ); + Bar_ProgressStop( pProgress ); Vec_VecFree( vLevels ); } p->nTotalNodesEnd = Nwk_ManNodeNum(pNtk); p->nTotalEdgesEnd = Nwk_ManGetTotalFanins(pNtk); -/* - // reset the timing manager - if ( pNtk->pManTime ) - { - Tim_ManStop( pNtk->pManTime ); - pNtk->pManTime = pManTimeOld; - } - Nwk_ManVerifyLevel( pNtk ); -*/ + + assert( Nwk_ManVerifyLevel( pNtk ) ); + assert( Nwk_ManVerifyTiming( pNtk ) ); + // free the manager p->timeTotal = clock() - clk; Mfx_ManStop( p ); diff --git a/src/aig/mfx/mfxDiv.c b/src/aig/mfx/mfxDiv.c index b7b76031..33f55ecb 100644 --- a/src/aig/mfx/mfxDiv.c +++ b/src/aig/mfx/mfxDiv.c @@ -88,17 +88,17 @@ Vec_Ptr_t * Abc_MfxWinMarkTfi( Nwk_Obj_t * pNode ) SeeAlso [] ***********************************************************************/ -void Abc_MfxWinSweepLeafTfo_rec( Nwk_Obj_t * pObj, int nLevelLimit ) +void Abc_MfxWinSweepLeafTfo_rec( Nwk_Obj_t * pObj, float tArrivalMax ) { Nwk_Obj_t * pFanout; int i; - if ( Nwk_ObjIsCo(pObj) || (int)pObj->Level > nLevelLimit ) + if ( Nwk_ObjIsCo(pObj) || Nwk_ObjArrival(pObj) > tArrivalMax ) return; if ( Nwk_ObjIsTravIdCurrent(pObj) ) return; Nwk_ObjSetTravIdCurrent( pObj ); Nwk_ObjForEachFanout( pObj, pFanout, i ) - Abc_MfxWinSweepLeafTfo_rec( pFanout, nLevelLimit ); + Abc_MfxWinSweepLeafTfo_rec( pFanout, tArrivalMax ); } /**Function************************************************************* @@ -187,7 +187,7 @@ int Abc_MfxWinVisitMffc( Nwk_Obj_t * pNode ) SeeAlso [] ***********************************************************************/ -Vec_Ptr_t * Mfx_ComputeDivisors( Mfx_Man_t * p, Nwk_Obj_t * pNode, int nLevDivMax ) +Vec_Ptr_t * Mfx_ComputeDivisors( Mfx_Man_t * p, Nwk_Obj_t * pNode, float tArrivalMax ) { Vec_Ptr_t * vCone, * vDivs; Nwk_Obj_t * pObj, * pFanout, * pFanin; @@ -210,7 +210,7 @@ Vec_Ptr_t * Mfx_ComputeDivisors( Mfx_Man_t * p, Nwk_Obj_t * pNode, int nLevDivMa // (2) the MFFC of the node // (3) the node's fanins (these are treated as a special case) Nwk_ManIncrementTravId( pNode->pMan ); - Abc_MfxWinSweepLeafTfo_rec( pNode, nLevDivMax ); + Abc_MfxWinSweepLeafTfo_rec( pNode, tArrivalMax ); Abc_MfxWinVisitMffc( pNode ); Nwk_ObjForEachFanin( pNode, pObj, k ) Nwk_ObjSetTravIdCurrent( pObj ); @@ -225,7 +225,7 @@ Vec_Ptr_t * Mfx_ComputeDivisors( Mfx_Man_t * p, Nwk_Obj_t * pNode, int nLevDivMa { if ( !Nwk_ObjIsTravIdPrevious(pObj) ) continue; - if ( (int)pObj->Level > nLevDivMax ) + if ( Nwk_ObjArrival(pObj) > tArrivalMax ) continue; Vec_PtrPush( vDivs, pObj ); if ( Vec_PtrSize(vDivs) >= p->pPars->nDivMax ) @@ -253,7 +253,7 @@ Vec_Ptr_t * Mfx_ComputeDivisors( Mfx_Man_t * p, Nwk_Obj_t * pNode, int nLevDivMa if ( !Nwk_ObjIsNode(pFanout) ) continue; // skip nodes with large level - if ( (int)pFanout->Level > nLevDivMax ) + if ( Nwk_ObjArrival(pFanout) > tArrivalMax ) continue; // skip nodes whose fanins are not divisors Nwk_ObjForEachFanin( pFanout, pFanin, m ) diff --git a/src/aig/mfx/mfxInt.h b/src/aig/mfx/mfxInt.h index 88792bf2..0693200d 100644 --- a/src/aig/mfx/mfxInt.h +++ b/src/aig/mfx/mfxInt.h @@ -125,7 +125,7 @@ struct Mfx_Man_t_ //////////////////////////////////////////////////////////////////////// /*=== mfxDiv.c ==========================================================*/ -extern Vec_Ptr_t * Mfx_ComputeDivisors( Mfx_Man_t * p, Nwk_Obj_t * pNode, int nLevDivMax ); +extern Vec_Ptr_t * Mfx_ComputeDivisors( Mfx_Man_t * p, Nwk_Obj_t * pNode, float tArrivalMax ); /*=== mfxInter.c ==========================================================*/ extern sat_solver * Mfx_CreateSolverResub( Mfx_Man_t * p, int * pCands, int nCands, int fInvert ); extern Hop_Obj_t * Mfx_Interplate( Mfx_Man_t * p, int * pCands, int nCands ); diff --git a/src/aig/mfx/mfxMan.c b/src/aig/mfx/mfxMan.c index 1b536f8c..63531770 100644 --- a/src/aig/mfx/mfxMan.c +++ b/src/aig/mfx/mfxMan.c @@ -120,8 +120,8 @@ void Mfx_ManPrint( Mfx_Man_t * p ) if ( p->pPars->fSwapEdge ) printf( "Swappable edges = %d. Total edges = %d. Ratio = %5.2f.\n", p->nNodesResub, Nwk_ManGetTotalFanins(p->pNtk), 1.00 * p->nNodesResub / Nwk_ManGetTotalFanins(p->pNtk) ); - else - Mfx_PrintResubStats( p ); +// else +// Mfx_PrintResubStats( p ); // printf( "Average ratio of DCs in the resubed nodes = %.2f.\n", 1.0*p->nDcMints/(64 * p->nNodesResub) ); } else diff --git a/src/aig/mfx/mfxResub.c b/src/aig/mfx/mfxResub.c index 2eafc559..7179173b 100644 --- a/src/aig/mfx/mfxResub.c +++ b/src/aig/mfx/mfxResub.c @@ -45,17 +45,10 @@ void Mfx_UpdateNetwork( Mfx_Man_t * p, Nwk_Obj_t * pObj, Vec_Ptr_t * vFanins, Ho int k; // create the new node pObjNew = Nwk_ManCreateNode( pObj->pMan, Vec_PtrSize(vFanins), Nwk_ObjFanoutNum(pObj) ); -if ( pObjNew->Id == 19969 ) -{ - int x = 0; -} pObjNew->pFunc = pFunc; Vec_PtrForEachEntry( vFanins, pFanin, k ) Nwk_ObjAddFanin( pObjNew, pFanin ); // replace the old node by the new node -//printf( "Replacing node " ); Nwk_ObjPrint( stdout, pObj ); -//printf( "Inserting node " ); Nwk_ObjPrint( stdout, pObjNew ); - // update the level of the node Nwk_ManUpdate( pObj, pObjNew, p->vLevels ); } diff --git a/src/aig/nwk/nwk.h b/src/aig/nwk/nwk.h index 295b3a9e..191ca3e5 100644 --- a/src/aig/nwk/nwk.h +++ b/src/aig/nwk/nwk.h @@ -131,6 +131,7 @@ static inline Nwk_Obj_t * Nwk_ObjFanout0( Nwk_Obj_t * p ) { return p->pF static inline Nwk_Obj_t * Nwk_ObjFanin( Nwk_Obj_t * p, int i ) { return p->pFanio[i]; } static inline Nwk_Obj_t * Nwk_ObjFanout( Nwk_Obj_t * p, int i ) { return p->pFanio[p->nFanins+1]; } +static inline int Nwk_ObjIsNone( Nwk_Obj_t * p ) { return p->Type == NWK_OBJ_NONE; } static inline int Nwk_ObjIsCi( Nwk_Obj_t * p ) { return p->Type == NWK_OBJ_CI; } static inline int Nwk_ObjIsCo( Nwk_Obj_t * p ) { return p->Type == NWK_OBJ_CO; } static inline int Nwk_ObjIsNode( Nwk_Obj_t * p ) { return p->Type == NWK_OBJ_NODE; } @@ -154,6 +155,10 @@ static inline void Nwk_ObjSetTravIdPrevious( Nwk_Obj_t * pObj ) { p static inline int Nwk_ObjIsTravIdCurrent( Nwk_Obj_t * pObj ) { return pObj->TravId == pObj->pMan->nTravIds; } static inline int Nwk_ObjIsTravIdPrevious( Nwk_Obj_t * pObj ) { return pObj->TravId == pObj->pMan->nTravIds - 1; } +static inline int Nwk_ManTimeEqual( float f1, float f2, float Eps ) { return (f1 < f2 + Eps) && (f2 < f1 + Eps); } +static inline int Nwk_ManTimeLess( float f1, float f2, float Eps ) { return (f1 < f2 + Eps); } +static inline int Nwk_ManTimeMore( float f1, float f2, float Eps ) { return (f1 + Eps > f2); } + //////////////////////////////////////////////////////////////////////// /// ITERATORS /// //////////////////////////////////////////////////////////////////////// @@ -191,8 +196,10 @@ static inline int Nwk_ObjIsTravIdPrevious( Nwk_Obj_t * pObj ) { r extern void Nwk_ManBidecResyn( Nwk_Man_t * pNtk, int fVerbose ); extern Hop_Obj_t * Nwk_NodeIfNodeResyn( Bdc_Man_t * p, Hop_Man_t * pHop, Hop_Obj_t * pRoot, int nVars, Vec_Int_t * vTruth, unsigned * puCare ); /*=== nwkDfs.c ==========================================================*/ +extern int Nwk_ManVerifyTopoOrder( Nwk_Man_t * pNtk ); +extern int Nwk_ManLevelBackup( Nwk_Man_t * pNtk ); extern int Nwk_ManLevel( Nwk_Man_t * pNtk ); -extern int Nwk_ManLevel2( Nwk_Man_t * pNtk ); +extern int Nwk_ManLevelMax( Nwk_Man_t * pNtk ); extern Vec_Vec_t * Nwk_ManLevelize( Nwk_Man_t * pNtk ); extern Vec_Ptr_t * Nwk_ManDfs( Nwk_Man_t * pNtk ); extern Vec_Ptr_t * Nwk_ManDfsNodes( Nwk_Man_t * pNtk, Nwk_Obj_t ** ppNodes, int nNodes ); @@ -203,9 +210,12 @@ extern int Nwk_ObjMffcLabel( Nwk_Obj_t * pNode ); /*=== nwkFanio.c ==========================================================*/ extern void Nwk_ObjCollectFanins( Nwk_Obj_t * pNode, Vec_Ptr_t * vNodes ); extern void Nwk_ObjCollectFanouts( Nwk_Obj_t * pNode, Vec_Ptr_t * vNodes ); +extern int Nwk_ObjFindFanin( Nwk_Obj_t * pObj, Nwk_Obj_t * pFanin ); +extern int Nwk_ObjFindFanout( Nwk_Obj_t * pObj, Nwk_Obj_t * pFanout ); extern void Nwk_ObjAddFanin( Nwk_Obj_t * pObj, Nwk_Obj_t * pFanin ); extern void Nwk_ObjDeleteFanin( Nwk_Obj_t * pObj, Nwk_Obj_t * pFanin ); extern void Nwk_ObjPatchFanin( Nwk_Obj_t * pObj, Nwk_Obj_t * pFaninOld, Nwk_Obj_t * pFaninNew ); +extern void Nwk_ObjTransferFanout( Nwk_Obj_t * pNodeFrom, Nwk_Obj_t * pNodeTo ); extern void Nwk_ObjReplace( Nwk_Obj_t * pNodeOld, Nwk_Obj_t * pNodeNew ); /*=== nwkMan.c ============================================================*/ extern Nwk_Man_t * Nwk_ManAlloc(); @@ -222,10 +232,11 @@ extern Nwk_Obj_t * Nwk_ManCreateLatch( Nwk_Man_t * pMan ); extern void Nwk_ManDeleteNode( Nwk_Obj_t * pObj ); extern void Nwk_ManDeleteNode_rec( Nwk_Obj_t * pObj ); /*=== nwkTiming.c ============================================================*/ -extern float Nwk_ManDelayTraceLut( Nwk_Man_t * pNtk, If_Lib_t * pLutLib ); -extern void Nwk_ManDelayTracePrint( Nwk_Man_t * pNtk, If_Lib_t * pLutLib ); +extern int Nwk_ManVerifyTiming( Nwk_Man_t * pNtk ); +extern float Nwk_ManDelayTraceLut( Nwk_Man_t * pNtk ); +extern void Nwk_ManDelayTracePrint( Nwk_Man_t * pNtk ); extern void Nwk_ManUpdate( Nwk_Obj_t * pObj, Nwk_Obj_t * pObjNew, Vec_Vec_t * vLevels ); -extern void Nwk_ManVerifyLevel( Nwk_Man_t * pNtk ); +extern int Nwk_ManVerifyLevel( Nwk_Man_t * pNtk ); /*=== nwkUtil.c ============================================================*/ extern void Nwk_ManIncrementTravId( Nwk_Man_t * pNtk ); extern int Nwk_ManGetFaninMax( Nwk_Man_t * pNtk ); @@ -235,6 +246,7 @@ extern int Nwk_ManPoNum( Nwk_Man_t * pNtk ); extern int Nwk_ManGetAigNodeNum( Nwk_Man_t * pNtk ); extern int Nwk_NodeCompareLevelsIncrease( Nwk_Obj_t ** pp1, Nwk_Obj_t ** pp2 ); extern int Nwk_NodeCompareLevelsDecrease( Nwk_Obj_t ** pp1, Nwk_Obj_t ** pp2 ); +extern void Nwk_ObjPrint( Nwk_Obj_t * pObj ); #ifdef __cplusplus } diff --git a/src/aig/nwk/nwkDfs.c b/src/aig/nwk/nwkDfs.c index a5f5a660..bf669086 100644 --- a/src/aig/nwk/nwkDfs.c +++ b/src/aig/nwk/nwkDfs.c @@ -30,6 +30,63 @@ /**Function************************************************************* + Synopsis [Verifies that the objects are in a topo order.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Nwk_ManVerifyTopoOrder( Nwk_Man_t * pNtk ) +{ + Nwk_Obj_t * pObj, * pNext; + int i, k, iBox, iTerm1, nTerms; + Nwk_ManIncrementTravId( pNtk ); + Nwk_ManForEachObj( pNtk, pObj, i ) + { + if ( Nwk_ObjIsNode(pObj) || Nwk_ObjIsCo(pObj) ) + { + Nwk_ObjForEachFanin( pObj, pNext, k ) + { + if ( !Nwk_ObjIsTravIdCurrent(pNext) ) + { + printf( "Node %d has fanin %d that is not in a topological order.\n", pObj->Id, pNext->Id ); + return 0; + } + } + } + else if ( Nwk_ObjIsCi(pObj) ) + { + if ( pNtk->pManTime ) + { + iBox = Tim_ManBoxForCi( pNtk->pManTime, pObj->PioId ); + if ( iBox >= 0 ) // this is not a true PI + { + iTerm1 = Tim_ManBoxInputFirst( pNtk->pManTime, iBox ); + nTerms = Tim_ManBoxInputNum( pNtk->pManTime, iBox ); + for ( i = 0; i < nTerms; i++ ) + { + pNext = Nwk_ManCo( pNtk, iTerm1 + i ); + if ( !Nwk_ObjIsTravIdCurrent(pNext) ) + { + printf( "Box %d has input %d that is not in a topological order.\n", iBox, pNext->Id ); + return 0; + } + } + } + } + } + else + assert( 0 ); + Nwk_ObjSetTravIdCurrent( pObj ); + } + return 1; +} + +/**Function************************************************************* + Synopsis [Computes the number of logic levels not counting PIs/POs.] Description [Assumes that white boxes have unit level.] @@ -39,11 +96,12 @@ SeeAlso [] ***********************************************************************/ -int Nwk_ManLevel( Nwk_Man_t * pNtk ) +int Nwk_ManLevelBackup( Nwk_Man_t * pNtk ) { Tim_Man_t * pManTimeUnit; Nwk_Obj_t * pObj, * pFanin; int i, k, LevelMax, Level; + assert( Nwk_ManVerifyTopoOrder(pNtk) ); // clean the levels Nwk_ManForEachObj( pNtk, pObj, i ) Nwk_ObjSetLevel( pObj, 0 ); @@ -85,11 +143,9 @@ int Nwk_ManLevel( Nwk_Man_t * pNtk ) return LevelMax; } - - /**Function************************************************************* - Synopsis [Performs DFS for one node.] + Synopsis [Computes the number of logic levels not counting PIs/POs.] Description [] @@ -98,8 +154,9 @@ int Nwk_ManLevel( Nwk_Man_t * pNtk ) SeeAlso [] ***********************************************************************/ -void Nwk_ManLevel2_rec( Nwk_Obj_t * pObj ) +void Nwk_ManLevel_rec( Nwk_Obj_t * pObj ) { + Tim_Man_t * pManTime = pObj->pMan->pManTime; Nwk_Obj_t * pNext; int i, iBox, iTerm1, nTerms, LevelMax = 0; if ( Nwk_ObjIsTravIdCurrent( pObj ) ) @@ -107,30 +164,33 @@ void Nwk_ManLevel2_rec( Nwk_Obj_t * pObj ) Nwk_ObjSetTravIdCurrent( pObj ); if ( Nwk_ObjIsCi(pObj) ) { - iBox = Tim_ManBoxForCi( pObj->pMan->pManTime, pObj->PioId ); - if ( iBox >= 0 ) // this is not a true PI + if ( pManTime ) { - iTerm1 = Tim_ManBoxInputFirst( pObj->pMan->pManTime, iBox ); - nTerms = Tim_ManBoxInputNum( pObj->pMan->pManTime, iBox ); - for ( i = 0; i < nTerms; i++ ) + iBox = Tim_ManBoxForCi( pManTime, pObj->PioId ); + if ( iBox >= 0 ) // this is not a true PI { - pNext = Nwk_ManCo(pObj->pMan, iTerm1 + i); - Nwk_ManLevel2_rec( pNext ); - if ( LevelMax < Nwk_ObjLevel(pNext) ) - LevelMax = Nwk_ObjLevel(pNext); + iTerm1 = Tim_ManBoxInputFirst( pManTime, iBox ); + nTerms = Tim_ManBoxInputNum( pManTime, iBox ); + for ( i = 0; i < nTerms; i++ ) + { + pNext = Nwk_ManCo(pObj->pMan, iTerm1 + i); + Nwk_ManLevel_rec( pNext ); + if ( LevelMax < Nwk_ObjLevel(pNext) ) + LevelMax = Nwk_ObjLevel(pNext); + } + LevelMax++; } - LevelMax++; } } else if ( Nwk_ObjIsNode(pObj) || Nwk_ObjIsCo(pObj) ) { Nwk_ObjForEachFanin( pObj, pNext, i ) { - Nwk_ManLevel2_rec( pNext ); + Nwk_ManLevel_rec( pNext ); if ( LevelMax < Nwk_ObjLevel(pNext) ) LevelMax = Nwk_ObjLevel(pNext); } - if ( Nwk_ObjIsNode(pObj) ) + if ( Nwk_ObjIsNode(pObj) && Nwk_ObjFaninNum(pObj) > 0 ) LevelMax++; } else @@ -140,16 +200,16 @@ void Nwk_ManLevel2_rec( Nwk_Obj_t * pObj ) /**Function************************************************************* - Synopsis [Returns the DFS ordered array of all objects except latches.] + Synopsis [Computes the number of logic levels not counting PIs/POs.] - Description [] + Description [Does not assume that the objects are in a topo order.] SideEffects [] SeeAlso [] ***********************************************************************/ -int Nwk_ManLevel2( Nwk_Man_t * pNtk ) +int Nwk_ManLevel( Nwk_Man_t * pNtk ) { Nwk_Obj_t * pObj; int i, LevelMax = 0; @@ -158,7 +218,7 @@ int Nwk_ManLevel2( Nwk_Man_t * pNtk ) Nwk_ManIncrementTravId( pNtk ); Nwk_ManForEachPo( pNtk, pObj, i ) { - Nwk_ManLevel2_rec( pObj ); + Nwk_ManLevel_rec( pObj ); if ( LevelMax < Nwk_ObjLevel(pObj) ) LevelMax = Nwk_ObjLevel(pObj); } @@ -169,6 +229,27 @@ int Nwk_ManLevel2( Nwk_Man_t * pNtk ) Synopsis [Computes the number of logic levels not counting PIs/POs.] + Description [Does not assume that the objects are in a topo order.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Nwk_ManLevelMax( Nwk_Man_t * pNtk ) +{ + Nwk_Obj_t * pObj; + int i, LevelMax = 0; + Nwk_ManForEachPo( pNtk, pObj, i ) + if ( LevelMax < Nwk_ObjLevel(pObj) ) + LevelMax = Nwk_ObjLevel(pObj); + return LevelMax; +} + +/**Function************************************************************* + + Synopsis [Returns the array of objects in the AIG manager ordered by level.] + Description [] SideEffects [] @@ -181,7 +262,8 @@ Vec_Vec_t * Nwk_ManLevelize( Nwk_Man_t * pNtk ) Nwk_Obj_t * pObj; Vec_Vec_t * vLevels; int nLevels, i; - nLevels = Nwk_ManLevel( pNtk ); + assert( Nwk_ManVerifyLevel(pNtk) ); + nLevels = Nwk_ManLevelMax( pNtk ); vLevels = Vec_VecStart( nLevels + 1 ); Nwk_ManForEachNode( pNtk, pObj, i ) { diff --git a/src/aig/nwk/nwkMan.c b/src/aig/nwk/nwkMan.c index d05543e6..2d0254f2 100644 --- a/src/aig/nwk/nwkMan.c +++ b/src/aig/nwk/nwkMan.c @@ -93,6 +93,7 @@ void Nwk_ManFree( Nwk_Man_t * p ) ***********************************************************************/ void Nwk_ManPrintStats( Nwk_Man_t * p, If_Lib_t * pLutLib ) { + p->pLutLib = pLutLib; printf( "%-15s : ", p->pName ); printf( "pi = %5d ", Nwk_ManPiNum(p) ); printf( "po = %5d ", Nwk_ManPoNum(p) ); @@ -102,8 +103,8 @@ void Nwk_ManPrintStats( Nwk_Man_t * p, If_Lib_t * pLutLib ) printf( "node = %5d ", Nwk_ManNodeNum(p) ); printf( "aig = %6d ", Nwk_ManGetAigNodeNum(p) ); printf( "lev = %3d ", Nwk_ManLevel(p) ); -// printf( "lev2 = %3d ", Nwk_ManLevel2(p) ); - printf( "delay = %5.2f", Nwk_ManDelayTraceLut(p, pLutLib) ); +// printf( "lev2 = %3d ", Nwk_ManLevelBackup(p) ); + printf( "delay = %5.2f", Nwk_ManDelayTraceLut(p) ); printf( "\n" ); // Nwk_ManDelayTracePrint( p, pLutLib ); fflush( stdout ); diff --git a/src/aig/nwk/nwkMap.c b/src/aig/nwk/nwkMap.c index ed67966e..eae3bd24 100644 --- a/src/aig/nwk/nwkMap.c +++ b/src/aig/nwk/nwkMap.c @@ -96,50 +96,45 @@ void Nwk_ManSetIfParsDefault( If_Par_t * pPars ) SeeAlso [] ***********************************************************************/ -If_Man_t * Nwk_ManToIf( Aig_Man_t * p, If_Par_t * pPars ) +If_Man_t * Nwk_ManToIf( Aig_Man_t * p, If_Par_t * pPars, Vec_Ptr_t * vAigToIf ) { If_Man_t * pIfMan; - Aig_Obj_t * pNode;//, * pFanin, * pPrev; + If_Obj_t * pIfObj; + Aig_Obj_t * pNode, * pFanin, * pPrev; int i; // start the mapping manager and set its parameters pIfMan = If_ManStart( pPars ); - // print warning about excessive memory usage -// if ( 1.0 * Aig_ManObjNum(p) * pIfMan->nObjBytes / (1<<30) > 1.0 ) -// printf( "Warning: The mapper will allocate %.1f Gb for to represent the subject graph with %d AIG nodes.\n", -// 1.0 * Aig_ManObjNum(p) * pIfMan->nObjBytes / (1<<30), Aig_ManObjNum(p) ); // load the AIG into the mapper Aig_ManForEachObj( p, pNode, i ) { if ( Aig_ObjIsAnd(pNode) ) - pNode->pData = (Aig_Obj_t *)If_ManCreateAnd( pIfMan, - If_NotCond( (If_Obj_t *)Aig_ObjFanin0(pNode)->pData, Aig_ObjFaninC0(pNode) ), - If_NotCond( (If_Obj_t *)Aig_ObjFanin1(pNode)->pData, Aig_ObjFaninC1(pNode) ) ); + pIfObj = If_ManCreateAnd( pIfMan, + If_NotCond( Aig_ObjFanin0(pNode)->pData, Aig_ObjFaninC0(pNode) ), + If_NotCond( Aig_ObjFanin1(pNode)->pData, Aig_ObjFaninC1(pNode) ) ); else if ( Aig_ObjIsPi(pNode) ) { - pNode->pData = If_ManCreateCi( pIfMan ); - ((If_Obj_t *)pNode->pData)->Level = pNode->Level; - if ( pIfMan->nLevelMax < (int)pNode->Level ) - pIfMan->nLevelMax = (int)pNode->Level; + pIfObj = If_ManCreateCi( pIfMan ); + If_ObjSetLevel( pIfObj, Aig_ObjLevel(pNode) ); } else if ( Aig_ObjIsPo(pNode) ) - pNode->pData = If_ManCreateCo( pIfMan, If_NotCond( Aig_ObjFanin0(pNode)->pData, Aig_ObjFaninC0(pNode) ) ); + pIfObj = If_ManCreateCo( pIfMan, If_NotCond( Aig_ObjFanin0(pNode)->pData, Aig_ObjFaninC0(pNode) ) ); else if ( Aig_ObjIsConst1(pNode) ) - Aig_ManConst1(p)->pData = If_ManConst1( pIfMan ); + pIfObj = If_ManConst1( pIfMan ); else // add the node to the mapper assert( 0 ); + // save the result + assert( Vec_PtrEntry(vAigToIf, i) == NULL ); + Vec_PtrWriteEntry( vAigToIf, i, pIfObj ); + pNode->pData = pIfObj; // set up the choice node -// if ( Aig_AigNodeIsChoice( pNode ) ) -// { -// pIfMan->nChoices++; -// for ( pPrev = pNode, pFanin = pNode->pData; pFanin; pPrev = pFanin, pFanin = pFanin->pData ) -// If_ObjSetChoice( (If_Obj_t *)pPrev->pData, (If_Obj_t *)pFanin->pData ); -// If_ManCreateChoice( pIfMan, (If_Obj_t *)pNode->pData ); -// } + if ( Aig_ObjIsChoice( p, pNode ) ) { - If_Obj_t * pIfObj = pNode->pData; - assert( !If_IsComplement(pIfObj) ); - assert( pIfObj->Id == pNode->Id ); + pIfMan->nChoices++; + for ( pPrev = pNode, pFanin = pNode->pData; pFanin; pPrev = pFanin, pFanin = pFanin->pData ) + If_ObjSetChoice( pPrev->pData, pFanin->pData ); + If_ManCreateChoice( pIfMan, pNode->pData ); } + assert( If_ObjLevel(pIfObj) == Aig_ObjLevel(pNode) ); } return pIfMan; } @@ -243,7 +238,7 @@ Hop_Obj_t * Nwk_NodeIfToHop( Hop_Man_t * pHopMan, If_Man_t * pIfMan, If_Obj_t * SeeAlso [] ***********************************************************************/ -Nwk_Man_t * Nwk_ManFromIf( If_Man_t * pIfMan, Aig_Man_t * p ) +Nwk_Man_t * Nwk_ManFromIf( If_Man_t * pIfMan, Aig_Man_t * p, Vec_Ptr_t * vAigToIf ) { Nwk_Man_t * pNtk; Nwk_Obj_t * pObjNew; @@ -261,7 +256,7 @@ Nwk_Man_t * Nwk_ManFromIf( If_Man_t * pIfMan, Aig_Man_t * p ) pNtk->pSpec = Aig_UtilStrsav( p->pSpec ); Aig_ManForEachObj( p, pObj, i ) { - pIfObj = If_ManObj( pIfMan, i ); + pIfObj = Vec_PtrEntry( vAigToIf, i ); if ( pIfObj->nRefs == 0 && !If_ObjIsTerm(pIfObj) ) continue; if ( Aig_ObjIsNode(pObj) ) @@ -312,12 +307,13 @@ Nwk_Man_t * Nwk_MappingIf( Aig_Man_t * p, Tim_Man_t * pManTime, If_Par_t * pPars { Nwk_Man_t * pNtk; If_Man_t * pIfMan; - // perform FPGA mapping + Vec_Ptr_t * vAigToIf; // set the arrival times pPars->pTimesArr = ALLOC( float, Aig_ManPiNum(p) ); memset( pPars->pTimesArr, 0, sizeof(float) * Aig_ManPiNum(p) ); // translate into the mapper - pIfMan = Nwk_ManToIf( p, pPars ); + vAigToIf = Vec_PtrStart( Aig_ManObjNumMax(p) ); + pIfMan = Nwk_ManToIf( p, pPars, vAigToIf ); if ( pIfMan == NULL ) return NULL; pIfMan->pManTim = Tim_ManDup( pManTime, 0 ); @@ -327,8 +323,9 @@ Nwk_Man_t * Nwk_MappingIf( Aig_Man_t * p, Tim_Man_t * pManTime, If_Par_t * pPars return NULL; } // transform the result of mapping into the new network - pNtk = Nwk_ManFromIf( pIfMan, p ); + pNtk = Nwk_ManFromIf( pIfMan, p, vAigToIf ); If_ManStop( pIfMan ); + Vec_PtrFree( vAigToIf ); return pNtk; } diff --git a/src/aig/nwk/nwkObj.c b/src/aig/nwk/nwkObj.c index 0806eecf..6d1f0428 100644 --- a/src/aig/nwk/nwkObj.c +++ b/src/aig/nwk/nwkObj.c @@ -194,7 +194,6 @@ void Nwk_ManDeleteNode_rec( Nwk_Obj_t * pObj ) Vec_PtrFree( vNodes ); } - //////////////////////////////////////////////////////////////////////// /// END OF FILE /// //////////////////////////////////////////////////////////////////////// diff --git a/src/aig/nwk/nwkStrash.c b/src/aig/nwk/nwkStrash.c index 668889a6..627bfa67 100644 --- a/src/aig/nwk/nwkStrash.c +++ b/src/aig/nwk/nwkStrash.c @@ -95,11 +95,13 @@ Aig_Obj_t * Nwk_ManStrashNode( Aig_Man_t * p, Nwk_Obj_t * pObj ) ***********************************************************************/ Aig_Man_t * Nwk_ManStrash( Nwk_Man_t * pNtk ) { - Aig_Man_t * pMan; + Aig_Man_t * pMan;//, * pTemp; Aig_Obj_t * pObjNew; Nwk_Obj_t * pObj; int i, Level; pMan = Aig_ManStart( Nwk_ManGetAigNodeNum(pNtk) ); + pMan->pName = Aig_UtilStrsav( pNtk->pName ); + pMan->pSpec = Aig_UtilStrsav( pNtk->pSpec ); pMan->pManTime = Tim_ManDup( pNtk->pManTime, 1 ); Tim_ManIncrementTravId( pMan->pManTime ); Nwk_ManForEachObj( pNtk, pObj, i ) @@ -125,6 +127,8 @@ Aig_Man_t * Nwk_ManStrash( Nwk_Man_t * pNtk ) pObj->pCopy = pObjNew; } Aig_ManCleanup( pMan ); +// pMan = Aig_ManDup( pTemp = pMan, 1 ); +// Aig_ManStop( pTemp ); return pMan; } diff --git a/src/aig/nwk/nwkTiming.c b/src/aig/nwk/nwkTiming.c index 0cbcb7f8..5e4967da 100644 --- a/src/aig/nwk/nwkTiming.c +++ b/src/aig/nwk/nwkTiming.c @@ -24,10 +24,6 @@ /// DECLARATIONS /// //////////////////////////////////////////////////////////////////////// -static inline int Nwk_ManTimeEqual( float f1, float f2, float Eps ) { return (f1 < f2 + Eps) && (f2 < f1 + Eps); } -static inline int Nwk_ManTimeLess( float f1, float f2, float Eps ) { return (f1 < f2 + Eps); } -static inline int Nwk_ManTimeMore( float f1, float f2, float Eps ) { return (f1 + Eps > f2); } - //////////////////////////////////////////////////////////////////////// /// FUNCTION DEFINITIONS /// //////////////////////////////////////////////////////////////////////// @@ -100,7 +96,7 @@ void Nwk_ManDelayTraceSortPins( Nwk_Obj_t * pNode, int * pPinPerm, float * pPinD /**Function************************************************************* - Synopsis [Computes the arrival times for the given node.] + Synopsis [Sorts the pins in the decreasing order of delays.] Description [] @@ -109,14 +105,39 @@ void Nwk_ManDelayTraceSortPins( Nwk_Obj_t * pNode, int * pPinPerm, float * pPinD SeeAlso [] ***********************************************************************/ -float Nwk_NodeComputeArrival( Nwk_Obj_t * pObj, If_Lib_t * pLutLib, int fUseSorting ) +int Nwk_ManWhereIsPin( Nwk_Obj_t * pFanout, Nwk_Obj_t * pFanin, int * pPinPerm ) { + int i; + for ( i = 0; i < Nwk_ObjFaninNum(pFanout); i++ ) + if ( Nwk_ObjFanin(pFanout, pPinPerm[i]) == pFanin ) + return i; + return -1; +} + +/**Function************************************************************* + + Synopsis [Computes the arrival times for the given object.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +float Nwk_NodeComputeArrival( Nwk_Obj_t * pObj, int fUseSorting ) +{ + If_Lib_t * pLutLib = pObj->pMan->pLutLib; int pPinPerm[32]; float pPinDelays[32]; Nwk_Obj_t * pFanin; float tArrival, * pDelays; int k; - assert( Nwk_ObjIsNode(pObj) ); + assert( Nwk_ObjIsNode(pObj) || Nwk_ObjIsCi(pObj) || Nwk_ObjIsCo(pObj) ); + if ( Nwk_ObjIsCi(pObj) ) + return Nwk_ObjArrival(pObj); + if ( Nwk_ObjIsCo(pObj) ) + return Nwk_ObjArrival( Nwk_ObjFanin0(pObj) ); tArrival = -AIG_INFINITY; if ( pLutLib == NULL ) { @@ -164,28 +185,35 @@ float Nwk_NodeComputeArrival( Nwk_Obj_t * pObj, If_Lib_t * pLutLib, int fUseSort SeeAlso [] ***********************************************************************/ -float Nwk_NodeComputeRequired( Nwk_Obj_t * pObj, If_Lib_t * pLutLib, int fUseSorting ) +float Nwk_NodeComputeRequired( Nwk_Obj_t * pObj, int fUseSorting ) { + If_Lib_t * pLutLib = pObj->pMan->pLutLib; int pPinPerm[32]; float pPinDelays[32]; Nwk_Obj_t * pFanout; - float tRequired, * pDelays; - int k; - assert( Nwk_ObjIsNode(pObj) || Nwk_ObjIsCi(pObj) ); + float tRequired, tDelay, * pDelays; + int k, iFanin; + assert( Nwk_ObjIsNode(pObj) || Nwk_ObjIsCi(pObj) || Nwk_ObjIsCo(pObj) ); + if ( Nwk_ObjIsCo(pObj) ) + return Nwk_ObjRequired(pObj); tRequired = AIG_INFINITY; if ( pLutLib == NULL ) { Nwk_ObjForEachFanout( pObj, pFanout, k ) - if ( tRequired > Nwk_ObjRequired(pFanout) - 1.0 ) - tRequired = Nwk_ObjRequired(pFanout) - 1.0; + { + tDelay = Nwk_ObjIsCo(pFanout)? 0.0 : 1.0; + if ( tRequired > Nwk_ObjRequired(pFanout) - tDelay ) + tRequired = Nwk_ObjRequired(pFanout) - tDelay; + } } else if ( !pLutLib->fVarPinDelays ) { Nwk_ObjForEachFanout( pObj, pFanout, k ) { pDelays = pLutLib->pLutDelays[Nwk_ObjFaninNum(pFanout)]; - if ( tRequired > Nwk_ObjRequired(pFanout) - pDelays[0] ) - tRequired = Nwk_ObjRequired(pFanout) - pDelays[0]; + tDelay = Nwk_ObjIsCo(pFanout)? 0.0 : pDelays[0]; + if ( tRequired > Nwk_ObjRequired(pFanout) - tDelay ) + tRequired = Nwk_ObjRequired(pFanout) - tDelay; } } else @@ -196,8 +224,11 @@ float Nwk_NodeComputeRequired( Nwk_Obj_t * pObj, If_Lib_t * pLutLib, int fUseSor { pDelays = pLutLib->pLutDelays[Nwk_ObjFaninNum(pFanout)]; Nwk_ManDelayTraceSortPins( pFanout, pPinPerm, pPinDelays ); - if ( tRequired > Nwk_ObjRequired(Nwk_ObjFanout(pObj,pPinPerm[k])) - pDelays[k] ) - tRequired = Nwk_ObjRequired(Nwk_ObjFanout(pObj,pPinPerm[k])) - pDelays[k]; + iFanin = Nwk_ManWhereIsPin( pFanout, pObj, pPinPerm ); + assert( Nwk_ObjFanin(pFanout,pPinPerm[iFanin]) == pObj ); + tDelay = Nwk_ObjIsCo(pFanout)? 0.0 : pDelays[iFanin]; + if ( tRequired > Nwk_ObjRequired(pFanout) - tDelay ) + tRequired = Nwk_ObjRequired(pFanout) - tDelay; } } else @@ -205,8 +236,11 @@ float Nwk_NodeComputeRequired( Nwk_Obj_t * pObj, If_Lib_t * pLutLib, int fUseSor Nwk_ObjForEachFanout( pObj, pFanout, k ) { pDelays = pLutLib->pLutDelays[Nwk_ObjFaninNum(pFanout)]; - if ( tRequired > Nwk_ObjRequired(pFanout) - pDelays[k] ) - tRequired = Nwk_ObjRequired(pFanout) - pDelays[k]; + iFanin = Nwk_ObjFindFanin( pFanout, pObj ); + assert( Nwk_ObjFanin(pFanout,iFanin) == pObj ); + tDelay = Nwk_ObjIsCo(pFanout)? 0.0 : pDelays[iFanin]; + if ( tRequired > Nwk_ObjRequired(pFanout) - tDelay ) + tRequired = Nwk_ObjRequired(pFanout) - tDelay; } } } @@ -224,8 +258,9 @@ float Nwk_NodeComputeRequired( Nwk_Obj_t * pObj, If_Lib_t * pLutLib, int fUseSor SeeAlso [] ***********************************************************************/ -float Nwk_NodePropagateRequired( Nwk_Obj_t * pObj, If_Lib_t * pLutLib, int fUseSorting ) +float Nwk_NodePropagateRequired( Nwk_Obj_t * pObj, int fUseSorting ) { + If_Lib_t * pLutLib = pObj->pMan->pLutLib; int pPinPerm[32]; float pPinDelays[32]; Nwk_Obj_t * pFanin; @@ -284,9 +319,10 @@ float Nwk_NodePropagateRequired( Nwk_Obj_t * pObj, If_Lib_t * pLutLib, int fUseS SeeAlso [] ***********************************************************************/ -float Nwk_ManDelayTraceLut( Nwk_Man_t * pNtk, If_Lib_t * pLutLib ) +float Nwk_ManDelayTraceLut( Nwk_Man_t * pNtk ) { int fUseSorting = 1; + If_Lib_t * pLutLib = pNtk->pLutLib; Vec_Ptr_t * vNodes; Nwk_Obj_t * pObj; float tArrival, tRequired, tSlack; @@ -311,22 +347,11 @@ float Nwk_ManDelayTraceLut( Nwk_Man_t * pNtk, If_Lib_t * pLutLib ) Tim_ManIncrementTravId( pNtk->pManTime ); Nwk_ManForEachObj( pNtk, pObj, i ) { - if ( Nwk_ObjIsNode(pObj) ) - { - tArrival = Nwk_NodeComputeArrival( pObj, pLutLib, fUseSorting ); - } - else if ( Nwk_ObjIsCi(pObj) ) - { - tArrival = pNtk->pManTime? Tim_ManGetPiArrival( pNtk->pManTime, pObj->PioId ) : (float)0.0; - } - else if ( Nwk_ObjIsCo(pObj) ) - { - tArrival = Nwk_ObjArrival( Nwk_ObjFanin0(pObj) ); - if ( pNtk->pManTime ) - Tim_ManSetPoArrival( pNtk->pManTime, pObj->PioId, tArrival ); - } - else - assert( 0 ); + tArrival = Nwk_NodeComputeArrival( pObj, fUseSorting ); + if ( Nwk_ObjIsCo(pObj) && pNtk->pManTime ) + Tim_ManSetPoArrival( pNtk->pManTime, pObj->PioId, tArrival ); + if ( Nwk_ObjIsCi(pObj) && pNtk->pManTime ) + tArrival = Tim_ManGetPiArrival( pNtk->pManTime, pObj->PioId ); Nwk_ObjSetArrival( pObj, tArrival ); } @@ -343,15 +368,17 @@ float Nwk_ManDelayTraceLut( Nwk_Man_t * pNtk, If_Lib_t * pLutLib ) Tim_ManSetPoRequiredAll( pNtk->pManTime, tArrival ); } else - Nwk_ManForEachPo( pNtk, pObj, i ) + { + Nwk_ManForEachCo( pNtk, pObj, i ) Nwk_ObjSetRequired( pObj, tArrival ); + } // propagate the required times Vec_PtrForEachEntry( vNodes, pObj, i ) { if ( Nwk_ObjIsNode(pObj) ) { - Nwk_NodePropagateRequired( pObj, pLutLib, fUseSorting ); + Nwk_NodePropagateRequired( pObj, fUseSorting ); } else if ( Nwk_ObjIsCi(pObj) ) { @@ -370,7 +397,7 @@ float Nwk_ManDelayTraceLut( Nwk_Man_t * pNtk, If_Lib_t * pLutLib ) // set slack for this object tSlack = Nwk_ObjRequired(pObj) - Nwk_ObjArrival(pObj); - assert( tSlack + 0.001 > 0.0 ); + assert( tSlack + 0.01 > 0.0 ); Nwk_ObjSetSlack( pObj, tSlack < 0.0 ? 0.0 : tSlack ); } Vec_PtrFree( vNodes ); @@ -379,6 +406,38 @@ float Nwk_ManDelayTraceLut( Nwk_Man_t * pNtk, If_Lib_t * pLutLib ) /**Function************************************************************* + Synopsis [Computes the arrival times for the given node.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Nwk_ManVerifyTiming( Nwk_Man_t * pNtk ) +{ + Nwk_Obj_t * pObj; + float tArrival, tRequired; + int i; + Nwk_ManForEachObj( pNtk, pObj, i ) + { + tArrival = Nwk_NodeComputeArrival( pObj, 1 ); + tRequired = Nwk_NodeComputeRequired( pObj, 1 ); + if ( Nwk_ObjIsCi(pObj) && pNtk->pManTime ) + tArrival = Tim_ManGetPiArrival( pNtk->pManTime, pObj->PioId ); + if ( Nwk_ObjIsCo(pObj) && pNtk->pManTime ) + tArrival = Tim_ManGetPoRequired( pNtk->pManTime, pObj->PioId ); + if ( !Nwk_ManTimeEqual( tArrival, Nwk_ObjArrival(pObj), (float)0.01 ) ) + printf( "Nwk_ManVerifyTiming(): Arrival time of object %d is incorrect.\n", pObj->Id ); + if ( !Nwk_ManTimeEqual( tRequired, Nwk_ObjRequired(pObj), (float)0.01 ) ) + printf( "Nwk_ManVerifyTiming(): Required time of object %d is incorrect.\n", pObj->Id ); + } + return 1; +} + +/**Function************************************************************* + Synopsis [Prints the delay trace for the given network.] Description [] @@ -388,8 +447,9 @@ float Nwk_ManDelayTraceLut( Nwk_Man_t * pNtk, If_Lib_t * pLutLib ) SeeAlso [] ***********************************************************************/ -void Nwk_ManDelayTracePrint( Nwk_Man_t * pNtk, If_Lib_t * pLutLib ) +void Nwk_ManDelayTracePrint( Nwk_Man_t * pNtk ) { + If_Lib_t * pLutLib = pNtk->pLutLib; Nwk_Obj_t * pNode; int i, Nodes, * pCounters; float tArrival, tDelta, nSteps, Num; @@ -401,11 +461,11 @@ void Nwk_ManDelayTracePrint( Nwk_Man_t * pNtk, If_Lib_t * pLutLib ) return; } // decide how many steps - nSteps = pLutLib ? 20 : Nwk_ManLevel(pNtk); + nSteps = pLutLib ? 20 : Nwk_ManLevelMax(pNtk); pCounters = ALLOC( int, nSteps + 1 ); memset( pCounters, 0, sizeof(int)*(nSteps + 1) ); // perform delay trace - tArrival = Nwk_ManDelayTraceLut( pNtk, pLutLib ); + tArrival = Nwk_ManDelayTraceLut( pNtk ); tDelta = tArrival / nSteps; // count how many nodes have slack in the corresponding intervals Nwk_ManForEachNode( pNtk, pNode, i ) @@ -491,39 +551,66 @@ void Nwk_NodeUpdateAddToQueue( Vec_Ptr_t * vQueue, Nwk_Obj_t * pObj, int iCurren SeeAlso [] ***********************************************************************/ -void Nwk_NodeUpdateArrival( Nwk_Obj_t * pObj, If_Lib_t * pLutLib ) +void Nwk_NodeUpdateArrival( Nwk_Obj_t * pObj ) { + If_Lib_t * pLutLib = pObj->pMan->pLutLib; Tim_Man_t * pManTime = pObj->pMan->pManTime; Vec_Ptr_t * vQueue = pObj->pMan->vTemp; Nwk_Obj_t * pTemp, * pNext; float tArrival; - int i, k; + int i, k, iBox, iTerm1, nTerms; assert( Nwk_ObjIsNode(pObj) ); + // verify the arrival time + tArrival = Nwk_NodeComputeArrival( pObj, 1 ); + assert( Nwk_ManTimeLess( tArrival, Nwk_ObjRequired(pObj), (float)0.01 ) ); // initialize the queue with the node Vec_PtrClear( vQueue ); Vec_PtrPush( vQueue, pObj ); pObj->MarkA = 1; // process objects - Tim_ManTravIdDisable( pManTime ); + if ( pManTime ) + Tim_ManIncrementTravId( pManTime ); Vec_PtrForEachEntry( vQueue, pTemp, i ) { pTemp->MarkA = 0; - tArrival = Nwk_NodeComputeArrival( pTemp, pLutLib, 1 ); - if ( Nwk_ManTimeEqual( tArrival, Nwk_ObjArrival(pTemp), (float)0.001 ) ) + tArrival = Nwk_NodeComputeArrival( pTemp, 1 ); + if ( Nwk_ObjIsCi(pTemp) && pManTime ) + tArrival = Tim_ManGetPiArrival( pManTime, pTemp->PioId ); + if ( Nwk_ManTimeEqual( tArrival, Nwk_ObjArrival(pTemp), (float)0.01 ) ) continue; Nwk_ObjSetArrival( pTemp, tArrival ); // add the fanouts to the queue - Nwk_ObjForEachFanout( pTemp, pNext, k ) + if ( Nwk_ObjIsCo(pTemp) ) + { + if ( pManTime ) + { + Tim_ManSetPoArrival( pManTime, pTemp->PioId, tArrival ); + iBox = Tim_ManBoxForCo( pManTime, pNext->PioId ); + Tim_ManSetCurrentTravIdBoxInputs( pManTime, iBox ); + if ( iBox >= 0 ) // this is not a true PO + { + iTerm1 = Tim_ManBoxOutputFirst( pManTime, iBox ); + nTerms = Tim_ManBoxOutputNum( pManTime, iBox ); + for ( i = 0; i < nTerms; i++ ) + { + pNext = Nwk_ManCi(pNext->pMan, iTerm1 + i); + if ( pNext->MarkA ) + continue; + Nwk_NodeUpdateAddToQueue( vQueue, pNext, i, 1 ); + pNext->MarkA = 1; + } + } + } + } + else { - if ( Nwk_ObjIsCo(pNext) ) + Nwk_ObjForEachFanout( pTemp, pNext, k ) { - Nwk_ObjSetArrival( pNext, tArrival ); - continue; + if ( pNext->MarkA ) + continue; + Nwk_NodeUpdateAddToQueue( vQueue, pNext, i, 1 ); + pNext->MarkA = 1; } - if ( pNext->MarkA ) - continue; - Nwk_NodeUpdateAddToQueue( vQueue, pNext, i, 1 ); - pNext->MarkA = 1; } } } @@ -539,18 +626,27 @@ void Nwk_NodeUpdateArrival( Nwk_Obj_t * pObj, If_Lib_t * pLutLib ) SeeAlso [] ***********************************************************************/ -void Nwk_NodeUpdateRequired( Nwk_Obj_t * pObj, If_Lib_t * pLutLib ) +void Nwk_NodeUpdateRequired( Nwk_Obj_t * pObj ) { + If_Lib_t * pLutLib = pObj->pMan->pLutLib; Tim_Man_t * pManTime = pObj->pMan->pManTime; Vec_Ptr_t * vQueue = pObj->pMan->vTemp; Nwk_Obj_t * pTemp, * pNext; float tRequired; - int i, k; + int i, k, iBox, iTerm1, nTerms; assert( Nwk_ObjIsNode(pObj) ); + +if ( pObj->Id == 1384 ) +{ + int x = 0; +// Nwk_ObjPrint( Nwk_ManObj(pObj->pMan, 1384) ); +// Nwk_ObjPrint( Nwk_ManObj(pObj->pMan, 422) ); +} + // make sure the node's required time remained the same - tRequired = Nwk_NodeComputeRequired( pObj, pLutLib, 1 ); - assert( Nwk_ManTimeEqual( tRequired, Nwk_ObjRequired(pObj), (float)0.001 ) ); - // initialize the queue with the node's fanins + tRequired = Nwk_NodeComputeRequired( pObj, 1 ); + assert( Nwk_ManTimeEqual( tRequired, Nwk_ObjRequired(pObj), (float)0.01 ) ); + // initialize the queue with the node's faninsa and the old node's fanins Vec_PtrClear( vQueue ); Nwk_ObjForEachFanin( pObj, pNext, k ) { @@ -560,21 +656,49 @@ void Nwk_NodeUpdateRequired( Nwk_Obj_t * pObj, If_Lib_t * pLutLib ) pNext->MarkA = 1; } // process objects - Tim_ManTravIdDisable( pManTime ); + if ( pManTime ) + Tim_ManIncrementTravId( pManTime ); Vec_PtrForEachEntry( vQueue, pTemp, i ) { pTemp->MarkA = 0; - tRequired = Nwk_NodeComputeRequired( pTemp, pLutLib, 1 ); - if ( Nwk_ManTimeEqual( tRequired, Nwk_ObjRequired(pTemp), (float)0.001 ) ) + tRequired = Nwk_NodeComputeRequired( pTemp, 1 ); + if ( Nwk_ObjIsCo(pTemp) && pManTime ) + tRequired = Tim_ManGetPoRequired( pManTime, pTemp->PioId ); + if ( Nwk_ManTimeEqual( tRequired, Nwk_ObjRequired(pTemp), (float)0.01 ) ) continue; Nwk_ObjSetRequired( pTemp, tRequired ); - // schedule fanins of the node - Nwk_ObjForEachFanin( pTemp, pNext, k ) + // add the fanouts to the queue + if ( Nwk_ObjIsCi(pTemp) ) { - if ( pNext->MarkA ) - continue; - Nwk_NodeUpdateAddToQueue( vQueue, pNext, i, 0 ); - pNext->MarkA = 1; + if ( pManTime ) + { + Tim_ManSetPiRequired( pManTime, pTemp->PioId, tRequired ); + iBox = Tim_ManBoxForCi( pManTime, pNext->PioId ); + Tim_ManSetCurrentTravIdBoxOutputs( pManTime, iBox ); + if ( iBox >= 0 ) // this is not a true PO + { + iTerm1 = Tim_ManBoxInputFirst( pManTime, iBox ); + nTerms = Tim_ManBoxInputNum( pManTime, iBox ); + for ( i = 0; i < nTerms; i++ ) + { + pNext = Nwk_ManCo(pNext->pMan, iTerm1 + i); + if ( pNext->MarkA ) + continue; + Nwk_NodeUpdateAddToQueue( vQueue, pNext, i, 0 ); + pNext->MarkA = 1; + } + } + } + } + else + { + Nwk_ObjForEachFanin( pTemp, pNext, k ) + { + if ( pNext->MarkA ) + continue; + Nwk_NodeUpdateAddToQueue( vQueue, pNext, i, 0 ); + pNext->MarkA = 1; + } } } } @@ -592,10 +716,28 @@ void Nwk_NodeUpdateRequired( Nwk_Obj_t * pObj, If_Lib_t * pLutLib ) ***********************************************************************/ int Nwk_ObjLevelNew( Nwk_Obj_t * pObj ) { + Tim_Man_t * pManTime = pObj->pMan->pManTime; Nwk_Obj_t * pFanin; - int i, Level = 0; + int i, iBox, iTerm1, nTerms, Level = 0; if ( Nwk_ObjIsCi(pObj) || Nwk_ObjIsLatch(pObj) ) - return 0; + { + if ( pManTime ) + { + iBox = Tim_ManBoxForCi( pManTime, pObj->PioId ); + if ( iBox >= 0 ) // this is not a true PI + { + iTerm1 = Tim_ManBoxInputFirst( pManTime, iBox ); + nTerms = Tim_ManBoxInputNum( pManTime, iBox ); + for ( i = 0; i < nTerms; i++ ) + { + pFanin = Nwk_ManCo(pObj->pMan, iTerm1 + i); + Level = AIG_MAX( Level, Nwk_ObjLevel(pFanin) ); + } + Level++; + } + } + return Level; + } assert( Nwk_ObjIsNode(pObj) || Nwk_ObjIsCo(pObj) ); Nwk_ObjForEachFanin( pObj, pFanin, i ) Level = AIG_MAX( Level, Nwk_ObjLevel(pFanin) ); @@ -615,9 +757,10 @@ int Nwk_ObjLevelNew( Nwk_Obj_t * pObj ) ***********************************************************************/ void Nwk_ManUpdateLevel( Nwk_Obj_t * pObj ) { + Tim_Man_t * pManTime = pObj->pMan->pManTime; Vec_Ptr_t * vQueue = pObj->pMan->vTemp; Nwk_Obj_t * pTemp, * pNext; - int LevelNew, i, k; + int LevelNew, i, k, iBox, iTerm1, nTerms; assert( Nwk_ObjIsNode(pObj) ); // initialize the queue with the node Vec_PtrClear( vQueue ); @@ -632,17 +775,36 @@ void Nwk_ManUpdateLevel( Nwk_Obj_t * pObj ) continue; Nwk_ObjSetLevel( pTemp, LevelNew ); // add the fanouts to the queue - Nwk_ObjForEachFanout( pTemp, pNext, k ) + if ( Nwk_ObjIsCo(pTemp) ) + { + if ( pManTime ) + { + iBox = Tim_ManBoxForCo( pManTime, pNext->PioId ); + Tim_ManSetCurrentTravIdBoxInputs( pManTime, iBox ); + if ( iBox >= 0 ) // this is not a true PO + { + iTerm1 = Tim_ManBoxOutputFirst( pManTime, iBox ); + nTerms = Tim_ManBoxOutputNum( pManTime, iBox ); + for ( i = 0; i < nTerms; i++ ) + { + pNext = Nwk_ManCi(pNext->pMan, iTerm1 + i); + if ( pNext->MarkA ) + continue; + Nwk_NodeUpdateAddToQueue( vQueue, pNext, i, 1 ); + pNext->MarkA = 1; + } + } + } + } + else { - if ( Nwk_ObjIsCo(pNext) ) + Nwk_ObjForEachFanout( pTemp, pNext, k ) { - Nwk_ObjSetLevel( pNext, LevelNew ); - continue; + if ( pNext->MarkA ) + continue; + Nwk_NodeUpdateAddToQueue( vQueue, pNext, i, 1 ); + pNext->MarkA = 1; } - if ( pNext->MarkA ) - continue; - Nwk_NodeUpdateAddToQueue( vQueue, pNext, i, 1 ); - pNext->MarkA = 1; } } } @@ -658,7 +820,7 @@ void Nwk_ManUpdateLevel( Nwk_Obj_t * pObj ) SeeAlso [] ***********************************************************************/ -void Nwk_ManVerifyLevel( Nwk_Man_t * pNtk ) +int Nwk_ManVerifyLevel( Nwk_Man_t * pNtk ) { Nwk_Obj_t * pObj; int LevelNew, i; @@ -672,6 +834,7 @@ void Nwk_ManVerifyLevel( Nwk_Man_t * pNtk ) i, Nwk_ObjLevel(pObj), LevelNew ); } } + return 1; } /**Function************************************************************* @@ -687,6 +850,14 @@ void Nwk_ManVerifyLevel( Nwk_Man_t * pNtk ) ***********************************************************************/ void Nwk_ManUpdate( Nwk_Obj_t * pObj, Nwk_Obj_t * pObjNew, Vec_Vec_t * vLevels ) { +// float Temp; + assert( pObj->pMan == pObjNew->pMan ); + assert( pObj != pObjNew ); + assert( Nwk_ObjFanoutNum(pObj) > 0 ); + assert( Nwk_ObjIsNode(pObj) && !Nwk_ObjIsCo(pObjNew) ); +// Temp = Nwk_NodeComputeRequired( pObj, 1 ); + // transfer fanouts to the old node + Nwk_ObjTransferFanout( pObj, pObjNew ); // transfer the timing information // (this is needed because updating level happens if the level has changed; // when we set the old level, it will be recomputed by the level updating @@ -694,13 +865,16 @@ void Nwk_ManUpdate( Nwk_Obj_t * pObj, Nwk_Obj_t * pObjNew, Vec_Vec_t * vLevels ) pObjNew->Level = pObj->Level; pObjNew->tArrival = pObj->tArrival; pObjNew->tRequired = pObj->tRequired; - // replace the old node by the new node - Nwk_ObjReplace( pObj, pObjNew ); - // update the level of the node + // update required times of the old fanins + pObj->tRequired = AIG_INFINITY; + Nwk_NodeUpdateRequired( pObj ); + // remove the old node + Nwk_ManDeleteNode_rec( pObj ); + // update the information of the new node Nwk_ManUpdateLevel( pObjNew ); -//Nwk_ManVerifyLevel( pObjNew->pMan ); -// Nwk_NodeUpdateArrival( pObjNew, pObj->pMan->pLutLib ); -// Nwk_NodeUpdateRequired( pObjNew, pObj->pMan->pLutLib ); + Nwk_NodeUpdateArrival( pObjNew ); + Nwk_NodeUpdateRequired( pObjNew ); +//Nwk_ManVerifyTiming( pObjNew->pMan ); } diff --git a/src/aig/nwk/nwkUtil.c b/src/aig/nwk/nwkUtil.c index 47e76844..b25fd68a 100644 --- a/src/aig/nwk/nwkUtil.c +++ b/src/aig/nwk/nwkUtil.c @@ -207,6 +207,38 @@ int Nwk_NodeCompareLevelsDecrease( Nwk_Obj_t ** pp1, Nwk_Obj_t ** pp2 ) return 0; } +/**Function************************************************************* + + Synopsis [Deletes the node.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Nwk_ObjPrint( Nwk_Obj_t * pObj ) +{ + Nwk_Obj_t * pNext; + int i; + printf( "ObjId = %5d. ", pObj->Id ); + if ( Nwk_ObjIsPi(pObj) ) + printf( "PI" ); + if ( Nwk_ObjIsPo(pObj) ) + printf( "PO" ); + if ( Nwk_ObjIsNode(pObj) ) + printf( "Node" ); + printf( " Fanins = " ); + Nwk_ObjForEachFanin( pObj, pNext, i ) + printf( "%d ", pNext->Id ); + printf( " Fanouts = " ); + Nwk_ObjForEachFanout( pObj, pNext, i ) + printf( "%d ", pNext->Id ); + printf( "\n" ); +} + + //////////////////////////////////////////////////////////////////////// /// END OF FILE /// //////////////////////////////////////////////////////////////////////// diff --git a/src/aig/tim/tim.c b/src/aig/tim/tim.c index ea8a3df1..d66dbd35 100644 --- a/src/aig/tim/tim.c +++ b/src/aig/tim/tim.c @@ -78,6 +78,7 @@ struct Tim_Obj_t_ static inline Tim_Obj_t * Tim_ManPi( Tim_Man_t * p, int i ) { assert( i < p->nPis ); return p->pPis + i; } static inline Tim_Obj_t * Tim_ManPo( Tim_Man_t * p, int i ) { assert( i < p->nPos ); return p->pPos + i; } +static inline Tim_Box_t * Tim_ManBox( Tim_Man_t * p, int i ) { return Vec_PtrEntry(p->vBoxes, i); } static inline Tim_Box_t * Tim_ManPiBox( Tim_Man_t * p, int i ) { return Tim_ManPi(p,i)->iObj2Box < 0 ? NULL : Vec_PtrEntry( p->vBoxes, Tim_ManPi(p,i)->iObj2Box ); } static inline Tim_Box_t * Tim_ManPoBox( Tim_Man_t * p, int i ) { return Tim_ManPo(p,i)->iObj2Box < 0 ? NULL : Vec_PtrEntry( p->vBoxes, Tim_ManPo(p,i)->iObj2Box ); } @@ -363,6 +364,48 @@ void Tim_ManTravIdEnable( Tim_Man_t * p ) /**Function************************************************************* + Synopsis [Label box inputs.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Tim_ManSetCurrentTravIdBoxInputs( Tim_Man_t * p, int iBox ) +{ + Tim_Box_t * pBox; + Tim_Obj_t * pObj; + int i; + pBox = Tim_ManBox( p, iBox ); + Tim_ManBoxForEachInput( p, pBox, pObj, i ) + pObj->TravId = p->nTravIds; +} + +/**Function************************************************************* + + Synopsis [Label box outputs.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Tim_ManSetCurrentTravIdBoxOutputs( Tim_Man_t * p, int iBox ) +{ + Tim_Box_t * pBox; + Tim_Obj_t * pObj; + int i; + pBox = Tim_ManBox( p, iBox ); + Tim_ManBoxForEachOutput( p, pBox, pObj, i ) + pObj->TravId = p->nTravIds; +} + +/**Function************************************************************* + Synopsis [Sets the vector of timing tables associated with the manager.] Description [] @@ -469,6 +512,16 @@ void Tim_ManCreateBoxFirst( Tim_Man_t * p, int firstIn, int nIns, int firstOut, ***********************************************************************/ void Tim_ManIncrementTravId( Tim_Man_t * p ) { + int i; + if ( p->nTravIds >= (1<<30)-1 ) + { + p->nTravIds = 0; + for ( i = 0; i < p->nPis; i++ ) + p->pPis[i].TravId = 0; + for ( i = 0; i < p->nPos; i++ ) + p->pPos[i].TravId = 0; + } + assert( p->nTravIds < (1<<30)-1 ); p->nTravIds++; } diff --git a/src/aig/tim/tim.h b/src/aig/tim/tim.h index 6904984f..d092434e 100644 --- a/src/aig/tim/tim.h +++ b/src/aig/tim/tim.h @@ -65,6 +65,8 @@ extern void Tim_ManStop( Tim_Man_t * p ); extern void Tim_ManPrint( Tim_Man_t * p ); extern void Tim_ManTravIdDisable( Tim_Man_t * p ); extern void Tim_ManTravIdEnable( Tim_Man_t * p ); +extern void Tim_ManSetCurrentTravIdBoxInputs( Tim_Man_t * p, int iBox ); +extern void Tim_ManSetCurrentTravIdBoxOutputs( Tim_Man_t * p, int iBox ); extern void Tim_ManSetDelayTables( Tim_Man_t * p, Vec_Ptr_t * vDelayTables ); extern void Tim_ManCreateBox( Tim_Man_t * p, int * pIns, int nIns, int * pOuts, int nOuts, float * pDelayTable ); extern void Tim_ManCreateBoxFirst( Tim_Man_t * p, int firstIn, int nIns, int firstOut, int nOuts, float * pDelayTable ); diff --git a/src/base/abc/abcCheck.c b/src/base/abc/abcCheck.c index 79b76348..025d2001 100644 --- a/src/base/abc/abcCheck.c +++ b/src/base/abc/abcCheck.c @@ -154,10 +154,7 @@ bool Abc_NtkDoCheck( Abc_Ntk_t * pNtk ) if ( Abc_NtkIsNetlist(pNtk) ) { if ( Abc_NtkNetNum(pNtk) == 0 ) - { - fprintf( stdout, "NetworkCheck: Netlist has no nets.\n" ); - return 0; - } + fprintf( stdout, "NetworkCheck: Warning! Netlist has no nets.\n" ); // check the nets Abc_NtkForEachNet( pNtk, pNet, i ) if ( !Abc_NtkCheckNet( pNtk, pNet ) ) diff --git a/src/base/abc/abcNtk.c b/src/base/abc/abcNtk.c index 1e88859c..6f34fa0b 100644 --- a/src/base/abc/abcNtk.c +++ b/src/base/abc/abcNtk.c @@ -953,8 +953,8 @@ void Abc_NtkDelete( Abc_Ntk_t * pNtk ) Abc_NtkForEachObj( pNtk, pObj, i ) { // free large fanout arrays - if ( pNtk->pMmObj && pObj->vFanouts.nCap * 4 > LargePiece ) - FREE( pObj->vFanouts.pArray ); +// if ( pNtk->pMmObj && pObj->vFanouts.nCap * 4 > LargePiece ) +// FREE( pObj->vFanouts.pArray ); // these flags should be always zero // if this is not true, something is wrong somewhere assert( pObj->fMarkA == 0 ); diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c index 2f52248e..f77c90e5 100644 --- a/src/base/abci/abc.c +++ b/src/base/abci/abc.c @@ -17,7 +17,7 @@ Revision [$Id: abc.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $] ***********************************************************************/ - + #include "abc.h" #include "mainInt.h" #include "fraig.h" @@ -1781,8 +1781,8 @@ int Abc_CommandPrintDsd( Abc_Frame_t * pAbc, int argc, char ** argv ) pTruth = Hop_ManConvertAigToTruth( pNtk->pManFunc, Hop_Regular(pObj->pData), Abc_ObjFaninNum(pObj), vMemory, 0 ); if ( Hop_IsComplement(pObj->pData) ) Extra_TruthNot( pTruth, pTruth, Abc_ObjFaninNum(pObj) ); - Extra_PrintBinary( stdout, pTruth, 1 << Abc_ObjFaninNum(pObj) ); - printf( "\n" ); +// Extra_PrintBinary( stdout, pTruth, 1 << Abc_ObjFaninNum(pObj) ); +// printf( "\n" ); if ( fCofactor ) Kit_DsdPrintCofactors( pTruth, Abc_ObjFaninNum(pObj), nCofLevel, 1 ); else @@ -7108,7 +7108,7 @@ int Abc_CommandTest( Abc_Frame_t * pAbc, int argc, char ** argv ) // extern void Abc_NtkDarTestBlif( char * pFileName ); // extern Abc_Ntk_t * Abc_NtkDarPartition( Abc_Ntk_t * pNtk ); // extern Abc_Ntk_t * Abc_NtkTestExor( Abc_Ntk_t * pNtk, int fVerbose ); - extern Abc_Ntk_t * Abc_NtkNtkTest( Abc_Ntk_t * pNtk ); + extern Abc_Ntk_t * Abc_NtkNtkTest( Abc_Ntk_t * pNtk, If_Lib_t * pLutLib ); @@ -7295,7 +7295,7 @@ int Abc_CommandTest( Abc_Frame_t * pAbc, int argc, char ** argv ) // Abc_NtkDarPartition( pNtk ); - pNtkRes = Abc_NtkNtkTest( pNtk ); + pNtkRes = Abc_NtkNtkTest( pNtk, Abc_FrameReadLibLut() ); if ( pNtkRes == NULL ) { fprintf( pErr, "Command has failed.\n" ); @@ -15343,7 +15343,7 @@ int Abc_CommandAbc8Mfs( Abc_Frame_t * pAbc, int argc, char ** argv ) { Mfx_Par_t Pars, * pPars = &Pars; int c; - extern int Mfx_Perform( void * pNtk, Mfx_Par_t * pPars ); + extern int Mfx_Perform( void * pNtk, Mfx_Par_t * pPars, If_Lib_t * pLutLib ); // set defaults Mfx_ParsDefault( pPars ); @@ -15449,7 +15449,7 @@ int Abc_CommandAbc8Mfs( Abc_Frame_t * pAbc, int argc, char ** argv ) } // modify the current network - if ( !Mfx_Perform( pAbc->pAbc8Nwk, pPars ) ) + if ( !Mfx_Perform( pAbc->pAbc8Nwk, pPars, pAbc->pAbc8Lib ) ) { fprintf( stdout, "Abc_CommandAbc8Mfs(): Command has failed.\n" ); return 1; diff --git a/src/base/abci/abcAbc8.c b/src/base/abci/abcAbc8.c index 3c60bde0..e918417c 100644 --- a/src/base/abci/abcAbc8.c +++ b/src/base/abci/abcAbc8.c @@ -198,8 +198,9 @@ clk = clock(); PRT( "Time", clock() - clk ); pMan = Abc_NtkToNtkNew( pNtk ); + pMan->pLutLib = Abc_FrameReadLibLut(); clk = clock(); - printf( "%6.2f\n", Nwk_ManDelayTraceLut( pMan, Abc_FrameReadLibLut() ) ); + printf( "%6.2f\n", Nwk_ManDelayTraceLut( pMan ) ); PRT( "Time", clock() - clk ); pNtkNew = Abc_NtkFromNtkNew( pNtk, pMan ); @@ -218,9 +219,9 @@ PRT( "Time", clock() - clk ); SeeAlso [] ***********************************************************************/ -Abc_Ntk_t * Abc_NtkNtkTest( Abc_Ntk_t * pNtk ) +Abc_Ntk_t * Abc_NtkNtkTest( Abc_Ntk_t * pNtk, If_Lib_t * pLutLib ) { - extern int Mfx_Perform( Nwk_Man_t * pNtk, Mfx_Par_t * pPars ); + extern int Mfx_Perform( Nwk_Man_t * pNtk, Mfx_Par_t * pPars, If_Lib_t * pLutLib ); Mfx_Par_t Pars, * pPars = &Pars; Abc_Ntk_t * pNtkNew; @@ -228,7 +229,7 @@ Abc_Ntk_t * Abc_NtkNtkTest( Abc_Ntk_t * pNtk ) pMan = Abc_NtkToNtkNew( pNtk ); Mfx_ParsDefault( pPars ); - Mfx_Perform( pMan, pPars ); + Mfx_Perform( pMan, pPars, pLutLib ); pNtkNew = Abc_NtkFromNtkNew( pNtk, pMan ); Nwk_ManFree( pMan ); diff --git a/src/map/if/if.h b/src/map/if/if.h index 61f81622..e0b9584d 100644 --- a/src/map/if/if.h +++ b/src/map/if/if.h @@ -255,6 +255,8 @@ static inline If_Obj_t * If_ObjFanin1( If_Obj_t * pObj ) { r static inline int If_ObjFaninC0( If_Obj_t * pObj ) { return pObj->fCompl0; } static inline int If_ObjFaninC1( If_Obj_t * pObj ) { return pObj->fCompl1; } static inline void * If_ObjCopy( If_Obj_t * pObj ) { return pObj->pCopy; } +static inline int If_ObjLevel( If_Obj_t * pObj ) { return pObj->Level; } +static inline void If_ObjSetLevel( If_Obj_t * pObj, int Level ) { pObj->Level = Level; } static inline void If_ObjSetCopy( If_Obj_t * pObj, void * pCopy ) { pObj->pCopy = pCopy; } static inline void If_ObjSetChoice( If_Obj_t * pObj, If_Obj_t * pEqu ) { pObj->pEquiv = pEqu; } diff --git a/src/map/if/ifMan.c b/src/map/if/ifMan.c index 7bb7fcd1..d1a17b6a 100644 --- a/src/map/if/ifMan.c +++ b/src/map/if/ifMan.c @@ -191,6 +191,8 @@ If_Obj_t * If_ManCreateCo( If_Man_t * p, If_Obj_t * pDriver ) pObj->fCompl0 = If_IsComplement(pDriver); pDriver = If_Regular(pDriver); pObj->pFanin0 = pDriver; pDriver->nRefs++; pObj->Level = pDriver->Level; + if ( p->nLevelMax < (int)pObj->Level ) + p->nLevelMax = (int)pObj->Level; p->nObjs[IF_CO]++; return pObj; } diff --git a/src/misc/extra/extraUtilMemory.c b/src/misc/extra/extraUtilMemory.c index 6eccf015..376ed9b0 100644 --- a/src/misc/extra/extraUtilMemory.c +++ b/src/misc/extra/extraUtilMemory.c @@ -527,12 +527,12 @@ void Extra_MmStepStop( Extra_MmStep_t * p ) int i; for ( i = 0; i < p->nMems; i++ ) Extra_MmFixedStop( p->pMems[i] ); -// if ( p->pLargeChunks ) -// { -// for ( i = 0; i < p->nLargeChunks; i++ ) -// free( p->pLargeChunks[i] ); -// free( p->pLargeChunks ); -// } + if ( p->pLargeChunks ) + { + for ( i = 0; i < p->nLargeChunks; i++ ) + free( p->pLargeChunks[i] ); + free( p->pLargeChunks ); + } free( p->pMems ); free( p->pMap ); free( p ); @@ -556,18 +556,16 @@ char * Extra_MmStepEntryFetch( Extra_MmStep_t * p, int nBytes ) if ( nBytes > p->nMapSize ) { // printf( "Allocating %d bytes.\n", nBytes ); -/* +// return ALLOC( char, nBytes ); if ( p->nLargeChunks == p->nLargeChunksAlloc ) { if ( p->nLargeChunksAlloc == 0 ) - p->nLargeChunksAlloc = 5; + p->nLargeChunksAlloc = 32; p->nLargeChunksAlloc *= 2; p->pLargeChunks = REALLOC( char *, p->pLargeChunks, p->nLargeChunksAlloc ); } p->pLargeChunks[ p->nLargeChunks++ ] = ALLOC( char, nBytes ); return p->pLargeChunks[ p->nLargeChunks - 1 ]; -*/ - return ALLOC( char, nBytes ); } return Extra_MmFixedEntryFetch( p->pMap[nBytes] ); } @@ -590,7 +588,7 @@ void Extra_MmStepEntryRecycle( Extra_MmStep_t * p, char * pEntry, int nBytes ) return; if ( nBytes > p->nMapSize ) { - free( pEntry ); +// free( pEntry ); return; } Extra_MmFixedEntryRecycle( p->pMap[nBytes], pEntry ); diff --git a/src/sat/bsat/satMem.c b/src/sat/bsat/satMem.c index 7fa1a824..1dacb854 100644 --- a/src/sat/bsat/satMem.c +++ b/src/sat/bsat/satMem.c @@ -63,10 +63,14 @@ struct Sat_MmFlex_t_ struct Sat_MmStep_t_ { - int nMems; // the number of fixed memory managers employed - Sat_MmFixed_t ** pMems; // memory managers: 2^1 words, 2^2 words, etc - int nMapSize; // the size of the memory array - Sat_MmFixed_t ** pMap; // maps the number of bytes into its memory manager + int nMems; // the number of fixed memory managers employed + Sat_MmFixed_t ** pMems; // memory managers: 2^1 words, 2^2 words, etc + int nMapSize; // the size of the memory array + Sat_MmFixed_t ** pMap; // maps the number of bytes into its memory manager + // additional memory chunks + int nChunksAlloc; // the maximum number of memory chunks + int nChunks; // the current number of memory chunks + char ** pChunks; // the allocated memory }; //////////////////////////////////////////////////////////////////////// @@ -291,7 +295,7 @@ Sat_MmFlex_t * Sat_MmFlexStart() p->pCurrent = NULL; p->pEnd = NULL; - p->nChunkSize = (1 << 12); + p->nChunkSize = (1 << 16); p->nChunksAlloc = 64; p->nChunks = 0; p->pChunks = ALLOC( char *, p->nChunksAlloc ); @@ -436,6 +440,9 @@ Sat_MmStep_t * Sat_MmStepStart( int nSteps ) p->pMap[k] = p->pMems[i]; //for ( i = 1; i < 100; i ++ ) //printf( "%10d: size = %10d\n", i, p->pMap[i]->nEntrySize ); + p->nChunksAlloc = 64; + p->nChunks = 0; + p->pChunks = ALLOC( char *, p->nChunksAlloc ); return p; } @@ -453,6 +460,12 @@ Sat_MmStep_t * Sat_MmStepStart( int nSteps ) void Sat_MmStepStop( Sat_MmStep_t * p, int fVerbose ) { int i; + if ( p->nChunksAlloc ) + { + for ( i = 0; i < p->nChunks; i++ ) + free( p->pChunks[i] ); + free( p->pChunks ); + } for ( i = 0; i < p->nMems; i++ ) Sat_MmFixedStop( p->pMems[i], fVerbose ); free( p->pMems ); @@ -477,8 +490,13 @@ char * Sat_MmStepEntryFetch( Sat_MmStep_t * p, int nBytes ) return NULL; if ( nBytes > p->nMapSize ) { -// printf( "Allocating %d bytes.\n", nBytes ); - return ALLOC( char, nBytes ); + if ( p->nChunks == p->nChunksAlloc ) + { + p->nChunksAlloc *= 2; + p->pChunks = REALLOC( char *, p->pChunks, p->nChunksAlloc ); + } + p->pChunks[ p->nChunks++ ] = ALLOC( char, nBytes ); + return p->pChunks[p->nChunks-1]; } return Sat_MmFixedEntryFetch( p->pMap[nBytes] ); } @@ -501,7 +519,7 @@ void Sat_MmStepEntryRecycle( Sat_MmStep_t * p, char * pEntry, int nBytes ) return; if ( nBytes > p->nMapSize ) { - free( pEntry ); +// free( pEntry ); return; } Sat_MmFixedEntryRecycle( p->pMap[nBytes], pEntry ); |