From 0080244a89eaaccd64c64af8f394486ab5d3e5b5 Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Wed, 2 Apr 2008 08:01:00 -0700 Subject: Version abc80402 --- src/aig/aig/aig.h | 1 + src/aig/aig/aigDfs.c | 74 ++++++++++ src/aig/aig/aigFrames.c | 1 + src/aig/aig/aigHaig.c | 1 + src/aig/aig/aigMan.c | 8 +- src/aig/aig/aigMem.c | 41 +++--- src/aig/aig/aigObj.c | 1 + src/aig/aig/aigPart.c | 44 +++++- src/aig/aig/aigRepr.c | 1 + src/aig/aig/aigRet.c | 1 + src/aig/aig/aigScl.c | 1 + src/aig/dar/dar.h | 2 +- src/aig/dar/darBalance.c | 33 ++++- src/aig/dar/darScript.c | 37 ++--- src/aig/fra/fraBmc.c | 1 + src/aig/fra/fraClass.c | 1 + src/aig/fra/fraInd.c | 1 + src/aig/fra/fraMan.c | 1 + src/aig/kit/kitDsd.c | 4 +- src/aig/mem/mem.c | 2 +- src/aig/mfx/mfxCore.c | 64 ++++----- src/aig/mfx/mfxDiv.c | 14 +- src/aig/mfx/mfxInt.h | 2 +- src/aig/mfx/mfxMan.c | 4 +- src/aig/mfx/mfxResub.c | 7 - src/aig/nwk/nwk.h | 20 ++- src/aig/nwk/nwkDfs.c | 126 ++++++++++++++--- src/aig/nwk/nwkMan.c | 5 +- src/aig/nwk/nwkMap.c | 57 ++++---- src/aig/nwk/nwkObj.c | 1 - src/aig/nwk/nwkStrash.c | 6 +- src/aig/nwk/nwkTiming.c | 350 +++++++++++++++++++++++++++++++++++------------ src/aig/nwk/nwkUtil.c | 32 +++++ src/aig/tim/tim.c | 53 +++++++ src/aig/tim/tim.h | 2 + 35 files changed, 742 insertions(+), 257 deletions(-) (limited to 'src/aig') 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 /// @@ -28,6 +29,79 @@ /// FUNCTION DEFINITIONS /// //////////////////////////////////////////////////////////////////////// +/**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.] 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************************************************************* @@ -1535,6 +1536,46 @@ int Aig_ManChoiceLevel( Aig_Man_t * pNew ) return LevelMax; } +/**Function************************************************************* + + Synopsis [Constructively accumulates choices.] + + Description [] + + SideEffects [] + + 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.] @@ -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 ) @@ -437,6 +439,35 @@ Aig_Man_t * Dar_ManBalance( Aig_Man_t * p, int fUpdateLevel ) return pNew; } +/**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.] 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 @@ -28,6 +28,63 @@ /// FUNCTION DEFINITIONS /// //////////////////////////////////////////////////////////////////////// +/**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.] @@ -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,13 +397,45 @@ 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 ); return tArrival; } +/**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.] @@ -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 ); } @@ -361,6 +362,48 @@ void Tim_ManTravIdEnable( Tim_Man_t * p ) p->fUseTravId = 1; } +/**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.] @@ -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 ); -- cgit v1.2.3