From 69b5bcad56f9352eea80d3e9b5e1322782522059 Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Thu, 3 Apr 2008 20:01:00 -0700 Subject: Version abc80403_2 --- src/aig/aig/aig.h | 2 +- src/aig/aig/aigDfs.c | 2 +- src/aig/aig/aigDup.c | 2 +- src/aig/aig/aigMan.c | 1 + src/aig/aig/aigPart.c | 81 ++++++++++++++++++++++++++++++++++++++++++----- src/aig/dar/darBalance.c | 2 +- src/aig/dar/darRefact.c | 4 +-- src/aig/dar/darScript.c | 26 +++++++++------ src/aig/fra/fra.h | 2 +- src/aig/fra/fraCec.c | 30 ++++++++++++------ src/aig/mfx/mfxCore.c | 4 +++ src/aig/ntl/ntlExtract.c | 2 +- src/aig/ntl/ntlInsert.c | 9 +++++- src/aig/ntl/ntlReadBlif.c | 4 +-- src/aig/nwk/nwkBidec.c | 5 +++ src/aig/nwk/nwkMap.c | 2 +- src/aig/nwk/nwkStrash.c | 10 ++++-- src/aig/nwk/nwkTiming.c | 51 ++++++++++++----------------- src/aig/tim/tim.c | 9 +++--- src/aig/tim/tim.h | 1 + 20 files changed, 172 insertions(+), 77 deletions(-) (limited to 'src/aig') diff --git a/src/aig/aig/aig.h b/src/aig/aig/aig.h index 18061a9c..f04a420d 100644 --- a/src/aig/aig/aig.h +++ b/src/aig/aig/aig.h @@ -528,7 +528,7 @@ extern Vec_Ptr_t * Aig_ManSupportsRegisters( Aig_Man_t * p ); extern Vec_Ptr_t * Aig_ManPartitionSmart( Aig_Man_t * p, int nPartSizeLimit, int fVerbose, Vec_Ptr_t ** pvPartSupps ); extern Vec_Ptr_t * Aig_ManPartitionSmartRegisters( Aig_Man_t * pAig, int nSuppSizeLimit, int fVerbose ); extern Vec_Ptr_t * Aig_ManPartitionNaive( Aig_Man_t * p, int nPartSize ); -extern Vec_Ptr_t * Aig_ManMiterPartitioned( Aig_Man_t * p1, Aig_Man_t * p2, int nPartSize ); +extern Vec_Ptr_t * Aig_ManMiterPartitioned( Aig_Man_t * p1, Aig_Man_t * p2, int nPartSize, int fSmart ); extern Aig_Man_t * Aig_ManChoicePartitioned( Vec_Ptr_t * vAigs, int nPartSize, int nConfMax, int nLevelMax, int fVerbose ); extern Aig_Man_t * Aig_ManFraigPartitioned( Aig_Man_t * pAig, int nPartSize, int nConfMax, int nLevelMax, int fVerbose ); extern Aig_Man_t * Aig_ManChoiceConstructive( Vec_Ptr_t * vAigs, int fVerbose ); diff --git a/src/aig/aig/aigDfs.c b/src/aig/aig/aigDfs.c index 9e43d7fd..34657a0b 100644 --- a/src/aig/aig/aigDfs.c +++ b/src/aig/aig/aigDfs.c @@ -418,7 +418,7 @@ void Aig_ManChoiceLevel_rec( Aig_Man_t * p, Aig_Obj_t * pObj ) LevelMax = Aig_ObjLevel(pNext); } } - else + else if ( !Aig_ObjIsConst1(pObj) ) assert( 0 ); Aig_ObjSetLevel( pObj, LevelMax ); } diff --git a/src/aig/aig/aigDup.c b/src/aig/aig/aigDup.c index 043a95a8..ca1f1cc3 100644 --- a/src/aig/aig/aigDup.c +++ b/src/aig/aig/aigDup.c @@ -359,7 +359,7 @@ Aig_Man_t * Aig_ManDupDfsOrder( Aig_Man_t * p, Aig_Man_t * pOrder ) } } Vec_PtrFree( vPios ); - assert( Aig_ManBufNum(p) != 0 || Aig_ManNodeNum(p) == Aig_ManNodeNum(pNew) ); +// assert( Aig_ManBufNum(p) != 0 || Aig_ManNodeNum(p) == Aig_ManNodeNum(pNew) ); if ( p->pEquivs == NULL && p->pReprs == NULL && (nNodes = Aig_ManCleanup( pNew )) ) printf( "Aig_ManDupDfs(): Cleanup after AIG duplication removed %d nodes.\n", nNodes ); // duplicate the timing manager diff --git a/src/aig/aig/aigMan.c b/src/aig/aig/aigMan.c index 0d5dfca9..58f0d797 100644 --- a/src/aig/aig/aigMan.c +++ b/src/aig/aig/aigMan.c @@ -208,6 +208,7 @@ void Aig_ManStop( Aig_Man_t * p ) if ( p->vFlopNums) Vec_IntFree( p->vFlopNums ); if ( p->pManExdc ) Aig_ManStop( p->pManExdc ); if ( p->vOnehots ) Vec_VecFree( (Vec_Vec_t *)p->vOnehots ); + FREE( p->pData ); FREE( p->pSeqModel ); FREE( p->pName ); FREE( p->pSpec ); diff --git a/src/aig/aig/aigPart.c b/src/aig/aig/aigPart.c index f129ae23..ce7221ae 100644 --- a/src/aig/aig/aigPart.c +++ b/src/aig/aig/aigPart.c @@ -1090,6 +1090,63 @@ Aig_Man_t * Aig_ManDupPartAll( Aig_Man_t * pOld, Vec_Int_t * vPart ) return pNew; } +/**Function************************************************************* + + Synopsis [Collects internal nodes in the DFS order.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Aig_ManSupportNodes_rec( Aig_Man_t * p, Aig_Obj_t * pObj, Vec_Int_t * vSupport ) +{ + if ( Aig_ObjIsTravIdCurrent(p, pObj) ) + return; + Aig_ObjSetTravIdCurrent(p, pObj); + if ( Aig_ObjIsPi(pObj) ) + { + Vec_IntPush( vSupport, Aig_ObjPioNum(pObj) ); + return; + } + Aig_ManSupportNodes_rec( p, Aig_ObjFanin0(pObj), vSupport ); + Aig_ManSupportNodes_rec( p, Aig_ObjFanin1(pObj), vSupport ); +} + +/**Function************************************************************* + + Synopsis [Collects internal nodes and PIs in the DFS order.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Vec_Ptr_t * Aig_ManSupportNodes( Aig_Man_t * p, Vec_Ptr_t * vParts ) +{ + Vec_Ptr_t * vPartSupps; + Vec_Int_t * vPart, * vSupport; + int i, k, iOut; + Aig_ManSetPioNumbers( p ); + vPartSupps = Vec_PtrAlloc( Vec_PtrSize(vParts) ); + Vec_PtrForEachEntry( vParts, vPart, i ) + { + vSupport = Vec_IntAlloc( 100 ); + Aig_ManIncrementTravId( p ); + Aig_ObjSetTravIdCurrent( p, Aig_ManConst1(p) ); + Vec_IntForEachEntry( vPart, iOut, k ) + Aig_ManSupportNodes_rec( p, Aig_ObjFanin0(Aig_ManPo(p, iOut)), vSupport ); +// Vec_IntSort( vSupport, 0 ); + Vec_PtrPush( vPartSupps, vSupport ); + } + Aig_ManCleanPioNumbers( p ); + return vPartSupps; +} + /**Function************************************************************* Synopsis [Create partitioned miter of the two AIGs.] @@ -1102,7 +1159,7 @@ Aig_Man_t * Aig_ManDupPartAll( Aig_Man_t * pOld, Vec_Int_t * vPart ) SeeAlso [] ***********************************************************************/ -Vec_Ptr_t * Aig_ManMiterPartitioned( Aig_Man_t * p1, Aig_Man_t * p2, int nPartSize ) +Vec_Ptr_t * Aig_ManMiterPartitioned( Aig_Man_t * p1, Aig_Man_t * p2, int nPartSize, int fSmart ) { Aig_Man_t * pNew; Aig_Obj_t * pMiter; @@ -1111,7 +1168,13 @@ Vec_Ptr_t * Aig_ManMiterPartitioned( Aig_Man_t * p1, Aig_Man_t * p2, int nPartSi Vec_Int_t * vPart, * vPartSupp; int i, k; // partition the first manager - vParts = Aig_ManPartitionSmart( p1, nPartSize, 0, &vPartSupps ); + if ( fSmart ) + vParts = Aig_ManPartitionSmart( p1, nPartSize, 0, &vPartSupps ); + else + { + vParts = Aig_ManPartitionNaive( p1, nPartSize ); + vPartSupps = Aig_ManSupportNodes( p1, vParts ); + } // derive miters vMiters = Vec_PtrAlloc( Vec_PtrSize(vParts) ); for ( i = 0; i < Vec_PtrSize(vParts); i++ ) @@ -1121,7 +1184,6 @@ Vec_Ptr_t * Aig_ManMiterPartitioned( Aig_Man_t * p1, Aig_Man_t * p2, int nPartSi vPartSupp = Vec_PtrEntry( vPartSupps, i ); // create the new miter pNew = Aig_ManStart( 1000 ); -// pNew->pName = Extra_UtilStrsav( p1->pName ); // create the PIs for ( k = 0; k < Vec_IntSize(vPartSupp); k++ ) Aig_ObjCreatePi( pNew ); @@ -1497,7 +1559,7 @@ void Aig_ManChoiceEval( Aig_Man_t * p ) ***********************************************************************/ Aig_Man_t * Aig_ManChoiceConstructive( Vec_Ptr_t * vAigs, int fVerbose ) { - Aig_Man_t * pNew, * pThis, * pPrev; + Aig_Man_t * pNew, * pThis, * pPrev, * pTemp; int i; // start AIG with choices pPrev = Vec_PtrEntry( vAigs, 0 ); @@ -1514,15 +1576,18 @@ Aig_Man_t * Aig_ManChoiceConstructive( Vec_Ptr_t * vAigs, int fVerbose ) pPrev = pThis; } // derive the result of choicing -//Aig_ManPrintStats( pNew ); pNew = Aig_ManRehash( pNew ); -//Aig_ManPrintStats( pNew ); // create the equivalent nodes lists Aig_ManMarkValidChoices( pNew ); -//Aig_ManPrintStats( pNew ); + // reconstruct the network + pNew = Aig_ManDupDfsOrder( pTemp = pNew, Vec_PtrEntry( vAigs, 0 ) ); + Aig_ManStop( pTemp ); + // duplicate the timing manager + pTemp = Vec_PtrEntry( vAigs, 0 ); + if ( pTemp->pManTime ) + pNew->pManTime = Tim_ManDup( pTemp->pManTime, 0 ); // reset levels Aig_ManChoiceLevel( pNew ); -// Aig_ManChoiceEval( pNew ); return pNew; } diff --git a/src/aig/dar/darBalance.c b/src/aig/dar/darBalance.c index 6e78041a..574c72d9 100644 --- a/src/aig/dar/darBalance.c +++ b/src/aig/dar/darBalance.c @@ -187,7 +187,7 @@ void Dar_BalancePermute( Aig_Man_t * p, Vec_Ptr_t * vSuper, int LeftBound, int f // get the two last nodes pObj1 = Vec_PtrEntry( vSuper, RightBound + 1 ); pObj2 = Vec_PtrEntry( vSuper, RightBound ); - if ( Aig_Regular(pObj1) == p->pConst1 || Aig_Regular(pObj2) == p->pConst1 ) + if ( Aig_Regular(pObj1) == p->pConst1 || Aig_Regular(pObj2) == p->pConst1 || Aig_Regular(pObj1) == Aig_Regular(pObj2) ) return; // find the first node that can be shared for ( i = RightBound; i >= LeftBound; i-- ) diff --git a/src/aig/dar/darRefact.c b/src/aig/dar/darRefact.c index e814840f..0637fee0 100644 --- a/src/aig/dar/darRefact.c +++ b/src/aig/dar/darRefact.c @@ -376,14 +376,14 @@ int Dar_ManRefactorTryCuts( Ref_Man_t * p, Aig_Obj_t * pObj, int nNodesSaved, in pTruth = Aig_ManCutTruth( pObj, vCut, p->vCutNodes, p->vTruthElem, p->vTruthStore ); if ( Kit_TruthIsConst0(pTruth, Vec_PtrSize(vCut)) ) { - p->GainBest = Vec_PtrSize(p->vCutNodes); + p->GainBest = Aig_NodeMffsSupp( p->pAig, pObj, 0, NULL ); p->pGraphBest = Kit_GraphCreateConst0(); Vec_PtrCopy( p->vLeavesBest, vCut ); return p->GainBest; } if ( Kit_TruthIsConst1(pTruth, Vec_PtrSize(vCut)) ) { - p->GainBest = Vec_PtrSize(p->vCutNodes); + p->GainBest = Aig_NodeMffsSupp( p->pAig, pObj, 0, NULL ); p->pGraphBest = Kit_GraphCreateConst1(); Vec_PtrCopy( p->vLeavesBest, vCut ); return p->GainBest; diff --git a/src/aig/dar/darScript.c b/src/aig/dar/darScript.c index 69810125..6d6b761c 100644 --- a/src/aig/dar/darScript.c +++ b/src/aig/dar/darScript.c @@ -82,19 +82,27 @@ Aig_Man_t * Dar_ManRwsat( Aig_Man_t * pAig, int fBalance, int fVerbose ) pAig = Aig_ManDupDfs( pAig ); if ( fVerbose ) Aig_ManPrintStats( pAig ); + + // balance + if ( fBalance ) + { + pAig = Dar_ManBalance( pTemp = pAig, 0 ); + Aig_ManStop( pTemp ); + if ( fVerbose ) Aig_ManPrintStats( pAig ); + } // rewrite Dar_ManRewrite( pAig, pParsRwr ); pAig = Aig_ManDupDfs( pTemp = pAig ); Aig_ManStop( pTemp ); if ( fVerbose ) Aig_ManPrintStats( pAig ); -/* + // refactor Dar_ManRefactor( pAig, pParsRef ); pAig = Aig_ManDupDfs( pTemp = pAig ); Aig_ManStop( pTemp ); if ( fVerbose ) Aig_ManPrintStats( pAig ); -*/ + // balance if ( fBalance ) { @@ -167,9 +175,9 @@ Aig_Man_t * Dar_ManCompress( Aig_Man_t * pAig, int fBalance, int fUpdateLevel, i // balance if ( fBalance ) { -// pAig = Dar_ManBalance( pTemp = pAig, fUpdateLevel ); -// Aig_ManStop( pTemp ); -// if ( fVerbose ) Aig_ManPrintStats( pAig ); + pAig = Dar_ManBalance( pTemp = pAig, fUpdateLevel ); + Aig_ManStop( pTemp ); + if ( fVerbose ) Aig_ManPrintStats( pAig ); } // rewrite @@ -239,9 +247,9 @@ Aig_Man_t * Dar_ManCompress2( Aig_Man_t * pAig, int fBalance, int fUpdateLevel, // balance if ( fBalance ) { -// pAig = Dar_ManBalance( pTemp = pAig, fUpdateLevel ); -// Aig_ManStop( pTemp ); -// if ( fVerbose ) Aig_ManPrintStats( pAig ); + pAig = Dar_ManBalance( pTemp = pAig, fUpdateLevel ); + Aig_ManStop( pTemp ); + if ( fVerbose ) Aig_ManPrintStats( pAig ); } @@ -336,7 +344,7 @@ Vec_Ptr_t * Dar_ManChoiceSynthesis( Aig_Man_t * pAig, int fBalance, int fUpdateL Aig_ManForEachObj( pAig, pObj, i ) pObj->pHaig = pObj; - pAig = Dar_ManCompress (pAig, 0, fUpdateLevel, fVerbose); + pAig = Dar_ManCompress (pAig, fBalance, fUpdateLevel, fVerbose); Vec_PtrPush( vAigs, pAig ); //Aig_ManPrintStats( pAig ); diff --git a/src/aig/fra/fra.h b/src/aig/fra/fra.h index dbe61522..7c2b95db 100644 --- a/src/aig/fra/fra.h +++ b/src/aig/fra/fra.h @@ -258,7 +258,7 @@ static inline int Fra_ImpCreate( int Left, int Right ) /*=== fraCec.c ========================================================*/ extern int Fra_FraigSat( Aig_Man_t * pMan, sint64 nConfLimit, sint64 nInsLimit, int fVerbose ); extern int Fra_FraigCec( Aig_Man_t ** ppAig, int fVerbose ); -extern int Fra_FraigCecPartitioned( Aig_Man_t * pMan1, Aig_Man_t * pMan2, int nPartSize, int fVerbose ); +extern int Fra_FraigCecPartitioned( Aig_Man_t * pMan1, Aig_Man_t * pMan2, int nPartSize, int fSmart, int fVerbose ); /*=== fraClass.c ========================================================*/ extern int Fra_BmcNodeIsConst( Aig_Obj_t * pObj ); extern int Fra_BmcNodesAreEqual( Aig_Obj_t * pObj0, Aig_Obj_t * pObj1 ); diff --git a/src/aig/fra/fraCec.c b/src/aig/fra/fraCec.c index 779337bf..05f2493a 100644 --- a/src/aig/fra/fraCec.c +++ b/src/aig/fra/fraCec.c @@ -166,8 +166,7 @@ PRT( "Time", clock() - clk ); // duplicate the AIG clk = clock(); -// pAig = Aig_ManDupDfs( pTemp = pAig ); - pAig = Dar_ManRwsat( pTemp = pAig, 0, 0 ); + pAig = Dar_ManRwsat( pTemp = pAig, 1, 0 ); Aig_ManStop( pTemp ); if ( fVerbose ) { @@ -247,22 +246,25 @@ PRT( "Time", clock() - clk ); SeeAlso [] ***********************************************************************/ -int Fra_FraigCecPartitioned( Aig_Man_t * pMan1, Aig_Man_t * pMan2, int nPartSize, int fVerbose ) +int Fra_FraigCecPartitioned( Aig_Man_t * pMan1, Aig_Man_t * pMan2, int nPartSize, int fSmart, int fVerbose ) { Aig_Man_t * pAig; Vec_Ptr_t * vParts; int i, RetValue = 1, nOutputs; // create partitions - vParts = Aig_ManMiterPartitioned( pMan1, pMan2, nPartSize ); + vParts = Aig_ManMiterPartitioned( pMan1, pMan2, nPartSize, fSmart ); // solve the partitions nOutputs = -1; Vec_PtrForEachEntry( vParts, pAig, i ) { nOutputs++; if ( fVerbose ) + { printf( "Verifying part %4d (out of %4d) PI = %5d. PO = %5d. And = %6d. Lev = %4d.\r", i+1, Vec_PtrSize(vParts), Aig_ManPiNum(pAig), Aig_ManPoNum(pAig), Aig_ManNodeNum(pAig), Aig_ManLevelNum(pAig) ); + fflush( stdout ); + } RetValue = Fra_FraigMiterStatus( pAig ); if ( RetValue == 1 ) continue; @@ -306,8 +308,9 @@ int Fra_FraigCecPartitioned( Aig_Man_t * pMan1, Aig_Man_t * pMan2, int nPartSize SeeAlso [] ***********************************************************************/ -int Fra_FraigCecTop( Aig_Man_t * pMan1, Aig_Man_t * pMan2, int nConfLimit, int fPartition, int fVerbose ) +int Fra_FraigCecTop( Aig_Man_t * pMan1, Aig_Man_t * pMan2, int nConfLimit, int nPartSize, int fSmart, int fVerbose ) { + Aig_Man_t * pTemp; //Abc_NtkDarCec( pNtk1, pNtk2, fPartition, fVerbose ); int RetValue, clkTotal = clock(); @@ -324,10 +327,19 @@ int Fra_FraigCecTop( Aig_Man_t * pMan1, Aig_Man_t * pMan2, int nConfLimit, int f assert( Aig_ManPiNum(pMan1) == Aig_ManPiNum(pMan1) ); assert( Aig_ManPoNum(pMan1) == Aig_ManPoNum(pMan1) ); - if ( fPartition ) - RetValue = Fra_FraigCecPartitioned( pMan1, pMan2, 100, fVerbose ); - else - RetValue = Fra_FraigCecPartitioned( pMan1, pMan2, Aig_ManPoNum(pMan1), fVerbose ); + // make sure that the first miter has more nodes + if ( Aig_ManNodeNum(pMan1) < Aig_ManNodeNum(pMan2) ) + { + pTemp = pMan1; + pMan1 = pMan2; + pMan2 = pTemp; + } + assert( Aig_ManNodeNum(pMan1) >= Aig_ManNodeNum(pMan2) ); + + if ( nPartSize ) + RetValue = Fra_FraigCecPartitioned( pMan1, pMan2, nPartSize, fSmart, fVerbose ); + else // no partitioning + RetValue = Fra_FraigCecPartitioned( pMan1, pMan2, Aig_ManPoNum(pMan1), 0, fVerbose ); // report the miter if ( RetValue == 1 ) diff --git a/src/aig/mfx/mfxCore.c b/src/aig/mfx/mfxCore.c index 6e47c986..bea7c6b0 100644 --- a/src/aig/mfx/mfxCore.c +++ b/src/aig/mfx/mfxCore.c @@ -312,6 +312,10 @@ int Mfx_Perform( Nwk_Man_t * pNtk, Mfx_Par_t * pPars, If_Lib_t * pLutLib ) // free the manager p->timeTotal = clock() - clk; Mfx_ManStop( p ); + + // update network into the topological order +// if ( pPars->fResub ) +// Nwk_ManTopological( pNtk ); return 1; } diff --git a/src/aig/ntl/ntlExtract.c b/src/aig/ntl/ntlExtract.c index 0654bb27..55356654 100644 --- a/src/aig/ntl/ntlExtract.c +++ b/src/aig/ntl/ntlExtract.c @@ -387,7 +387,7 @@ int Ntl_ManExtract_rec( Ntl_Man_t * p, Ntl_Net_t * pNet ) // add box inputs/outputs to COs/CIs if ( Ntl_ObjIsBox(pObj) ) { - int LevelCur, LevelMax = -AIG_INFINITY; + int LevelCur, LevelMax = -TIME_ETERNITY; Vec_IntPush( p->vBox1Cos, Aig_ManPoNum(p->pAig) ); Ntl_ObjForEachFanin( pObj, pNetFanin, i ) { diff --git a/src/aig/ntl/ntlInsert.c b/src/aig/ntl/ntlInsert.c index 2eb48e84..f02b4716 100644 --- a/src/aig/ntl/ntlInsert.c +++ b/src/aig/ntl/ntlInsert.c @@ -137,6 +137,7 @@ int Ntl_ManInsert( Ntl_Man_t * p, Vec_Ptr_t * vMapping, Aig_Man_t * pAig ) int Ntl_ManInsertNtk( Ntl_Man_t * p, Nwk_Man_t * pNtk ) { char Buffer[100]; + Vec_Ptr_t * vObjs; Vec_Int_t * vTruth; Vec_Int_t * vCover; Ntl_Mod_t * pRoot; @@ -160,8 +161,13 @@ int Ntl_ManInsertNtk( Ntl_Man_t * p, Nwk_Man_t * pNtk ) vTruth = Vec_IntAlloc( 1 << 16 ); vCover = Vec_IntAlloc( 1 << 16 ); nDigits = Aig_Base10Log( Nwk_ManNodeNum(pNtk) ); - Nwk_ManForEachNode( pNtk, pObj, i ) +// Nwk_ManForEachObj( pNtk, pObj, i ) + vObjs = Nwk_ManDfs( pNtk ); + Vec_PtrForEachEntry( vObjs, pObj, i ) +// Nwk_ManForEachNode( pNtk, pObj, i ) { + if ( !Nwk_ObjIsNode(pObj) ) + continue; pNode = Ntl_ModelCreateNode( pRoot, Nwk_ObjFaninNum(pObj) ); pTruth = Hop_ManConvertAigToTruth( pNtk->pManHop, Hop_Regular(pObj->pFunc), Nwk_ObjFaninNum(pObj), vTruth, 0 ); if ( Hop_IsComplement(pObj->pFunc) ) @@ -194,6 +200,7 @@ int Ntl_ManInsertNtk( Ntl_Man_t * p, Nwk_Man_t * pNtk ) } pObj->pCopy = pNet; } + Vec_PtrFree( vObjs ); Vec_IntFree( vCover ); Vec_IntFree( vTruth ); // mark CIs and outputs of the registers diff --git a/src/aig/ntl/ntlReadBlif.c b/src/aig/ntl/ntlReadBlif.c index e5a94610..81ea2a2c 100644 --- a/src/aig/ntl/ntlReadBlif.c +++ b/src/aig/ntl/ntlReadBlif.c @@ -974,9 +974,9 @@ static int Ioa_ReadParseLineTimes( Ioa_ReadMod_t * p, char * pLine, int fOutput // find the delay number pTokenNum = Vec_PtrEntryLast(vTokens); if ( !strcmp( pTokenNum, "-inf" ) ) - Delay = -AIG_INFINITY; + Delay = -TIME_ETERNITY; else if ( !strcmp( pTokenNum, "inf" ) ) - Delay = AIG_INFINITY; + Delay = TIME_ETERNITY; else Delay = atof( pTokenNum ); if ( Delay == 0.0 && pTokenNum[0] != '0' ) diff --git a/src/aig/nwk/nwkBidec.c b/src/aig/nwk/nwkBidec.c index 5d0b454e..e30d2c02 100644 --- a/src/aig/nwk/nwkBidec.c +++ b/src/aig/nwk/nwkBidec.c @@ -88,6 +88,11 @@ void Nwk_ManBidecResyn( Nwk_Man_t * pNtk, int fVerbose ) int clk = clock(); pPars->nVarsMax = Nwk_ManGetFaninMax( pNtk ); pPars->fVerbose = fVerbose; + if ( pPars->nVarsMax < 2 ) + { + printf( "Resynthesis is not performed for networks whose nodes are less than 2 inputs.\n" ); + return; + } if ( pPars->nVarsMax > 15 ) { if ( fVerbose ) diff --git a/src/aig/nwk/nwkMap.c b/src/aig/nwk/nwkMap.c index 44aecc03..ee7f56ad 100644 --- a/src/aig/nwk/nwkMap.c +++ b/src/aig/nwk/nwkMap.c @@ -52,7 +52,7 @@ void Nwk_ManSetIfParsDefault( If_Par_t * pPars ) pPars->nFlowIters = 1; pPars->nAreaIters = 2; pPars->DelayTarget = -1; - pPars->Epsilon = (float)0.01; + pPars->Epsilon = (float)0.001; pPars->fPreprocess = 1; pPars->fArea = 0; pPars->fFancy = 0; diff --git a/src/aig/nwk/nwkStrash.c b/src/aig/nwk/nwkStrash.c index 3bcfcd41..b5e2b387 100644 --- a/src/aig/nwk/nwkStrash.c +++ b/src/aig/nwk/nwkStrash.c @@ -95,7 +95,8 @@ 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;//, * pTemp; + Vec_Ptr_t * vObjs; + Aig_Man_t * pMan; Aig_Obj_t * pObjNew; Nwk_Obj_t * pObj; int i, Level; @@ -105,6 +106,10 @@ Aig_Man_t * Nwk_ManStrash( Nwk_Man_t * pNtk ) pMan->pManTime = Tim_ManDup( pNtk->pManTime, 1 ); Tim_ManIncrementTravId( pMan->pManTime ); Nwk_ManForEachObj( pNtk, pObj, i ) + pObj->pCopy = NULL; +// Nwk_ManForEachObj( pNtk, pObj, i ) + vObjs = Nwk_ManDfs( pNtk ); + Vec_PtrForEachEntry( vObjs, pObj, i ) { if ( Nwk_ObjIsCi(pObj) ) { @@ -126,9 +131,8 @@ Aig_Man_t * Nwk_ManStrash( Nwk_Man_t * pNtk ) assert( 0 ); pObj->pCopy = pObjNew; } + Vec_PtrFree( vObjs ); Aig_ManCleanup( pMan ); -// pMan = Aig_ManDupOrdered( pTemp = pMan ); -// Aig_ManStop( pTemp ); return pMan; } diff --git a/src/aig/nwk/nwkTiming.c b/src/aig/nwk/nwkTiming.c index 5e4967da..9bf1d6a1 100644 --- a/src/aig/nwk/nwkTiming.c +++ b/src/aig/nwk/nwkTiming.c @@ -17,7 +17,7 @@ Revision [$Id: nwkTiming.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $] ***********************************************************************/ - + #include "nwk.h" //////////////////////////////////////////////////////////////////////// @@ -46,7 +46,7 @@ void Nwk_ManCleanTiming( Nwk_Man_t * pNtk ) Nwk_ManForEachObj( pNtk, pObj, i ) { pObj->tArrival = pObj->tSlack = 0.0; - pObj->tRequired = AIG_INFINITY; + pObj->tRequired = TIME_ETERNITY; } } @@ -138,7 +138,7 @@ float Nwk_NodeComputeArrival( Nwk_Obj_t * pObj, int fUseSorting ) return Nwk_ObjArrival(pObj); if ( Nwk_ObjIsCo(pObj) ) return Nwk_ObjArrival( Nwk_ObjFanin0(pObj) ); - tArrival = -AIG_INFINITY; + tArrival = -TIME_ETERNITY; if ( pLutLib == NULL ) { Nwk_ObjForEachFanin( pObj, pFanin, k ) @@ -196,7 +196,7 @@ float Nwk_NodeComputeRequired( Nwk_Obj_t * pObj, int fUseSorting ) assert( Nwk_ObjIsNode(pObj) || Nwk_ObjIsCi(pObj) || Nwk_ObjIsCo(pObj) ); if ( Nwk_ObjIsCo(pObj) ) return Nwk_ObjRequired(pObj); - tRequired = AIG_INFINITY; + tRequired = TIME_ETERNITY; if ( pLutLib == NULL ) { Nwk_ObjForEachFanout( pObj, pFanout, k ) @@ -333,7 +333,7 @@ float Nwk_ManDelayTraceLut( Nwk_Man_t * pNtk ) { printf( "The max LUT size (%d) is less than the max fanin count (%d).\n", pLutLib->LutMax, Nwk_ManGetFaninMax(pNtk) ); - return -AIG_INFINITY; + return -TIME_ETERNITY; } // compute the reverse order of all objects @@ -356,7 +356,7 @@ float Nwk_ManDelayTraceLut( Nwk_Man_t * pNtk ) } // get the latest arrival times - tArrival = -AIG_INFINITY; + tArrival = -TIME_ETERNITY; Nwk_ManForEachPo( pNtk, pObj, i ) if ( tArrival < Nwk_ObjArrival(pObj) ) tArrival = Nwk_ObjArrival(pObj); @@ -388,11 +388,12 @@ float Nwk_ManDelayTraceLut( Nwk_Man_t * pNtk ) else if ( Nwk_ObjIsCo(pObj) ) { if ( pNtk->pManTime ) + { tRequired = Tim_ManGetPoRequired( pNtk->pManTime, pObj->PioId ); - else - tRequired = Nwk_ObjRequired(pObj); - if ( Nwk_ObjRequired(Nwk_ObjFanin0(pObj)) > tRequired ) - Nwk_ObjSetRequired( Nwk_ObjFanin0(pObj), tRequired ); + Nwk_ObjSetRequired( pObj, tRequired ); + } + if ( Nwk_ObjRequired(Nwk_ObjFanin0(pObj)) > Nwk_ObjRequired(pObj) ) + Nwk_ObjSetRequired( Nwk_ObjFanin0(pObj), Nwk_ObjRequired(pObj) ); } // set slack for this object @@ -424,14 +425,12 @@ int Nwk_ManVerifyTiming( Nwk_Man_t * pNtk ) { 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 ); + printf( "Nwk_ManVerifyTiming(): Object %d has different arrival time (%.2f) from computed (%.2f).\n", + pObj->Id, Nwk_ObjArrival(pObj), tArrival ); if ( !Nwk_ManTimeEqual( tRequired, Nwk_ObjRequired(pObj), (float)0.01 ) ) - printf( "Nwk_ManVerifyTiming(): Required time of object %d is incorrect.\n", pObj->Id ); + printf( "Nwk_ManVerifyTiming(): Object %d has different required time (%.2f) from computed (%.2f).\n", + pObj->Id, Nwk_ObjRequired(pObj), tRequired ); } return 1; } @@ -586,9 +585,9 @@ void Nwk_NodeUpdateArrival( Nwk_Obj_t * pObj ) { 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 { + Tim_ManSetCurrentTravIdBoxInputs( pManTime, iBox ); iTerm1 = Tim_ManBoxOutputFirst( pManTime, iBox ); nTerms = Tim_ManBoxOutputNum( pManTime, iBox ); for ( i = 0; i < nTerms; i++ ) @@ -635,14 +634,6 @@ void Nwk_NodeUpdateRequired( Nwk_Obj_t * pObj ) float tRequired; 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, 1 ); assert( Nwk_ManTimeEqual( tRequired, Nwk_ObjRequired(pObj), (float)0.01 ) ); @@ -667,16 +658,16 @@ if ( pObj->Id == 1384 ) if ( Nwk_ManTimeEqual( tRequired, Nwk_ObjRequired(pTemp), (float)0.01 ) ) continue; Nwk_ObjSetRequired( pTemp, tRequired ); - // add the fanouts to the queue + // add the fanins to the queue if ( Nwk_ObjIsCi(pTemp) ) { 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 { + Tim_ManSetCurrentTravIdBoxOutputs( pManTime, iBox ); iTerm1 = Tim_ManBoxInputFirst( pManTime, iBox ); nTerms = Tim_ManBoxInputNum( pManTime, iBox ); for ( i = 0; i < nTerms; i++ ) @@ -780,9 +771,9 @@ void Nwk_ManUpdateLevel( Nwk_Obj_t * pObj ) if ( pManTime ) { iBox = Tim_ManBoxForCo( pManTime, pNext->PioId ); - Tim_ManSetCurrentTravIdBoxInputs( pManTime, iBox ); if ( iBox >= 0 ) // this is not a true PO { + Tim_ManSetCurrentTravIdBoxInputs( pManTime, iBox ); iTerm1 = Tim_ManBoxOutputFirst( pManTime, iBox ); nTerms = Tim_ManBoxOutputNum( pManTime, iBox ); for ( i = 0; i < nTerms; i++ ) @@ -850,12 +841,10 @@ int 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 @@ -866,7 +855,7 @@ void Nwk_ManUpdate( Nwk_Obj_t * pObj, Nwk_Obj_t * pObjNew, Vec_Vec_t * vLevels ) pObjNew->tArrival = pObj->tArrival; pObjNew->tRequired = pObj->tRequired; // update required times of the old fanins - pObj->tRequired = AIG_INFINITY; + pObj->tRequired = TIME_ETERNITY; Nwk_NodeUpdateRequired( pObj ); // remove the old node Nwk_ManDeleteNode_rec( pObj ); diff --git a/src/aig/tim/tim.c b/src/aig/tim/tim.c index d66dbd35..62e29fe9 100644 --- a/src/aig/tim/tim.c +++ b/src/aig/tim/tim.c @@ -31,7 +31,6 @@ #define AIG_MIN(a,b) (((a) < (b))? (a) : (b)) #define AIG_MAX(a,b) (((a) > (b))? (a) : (b)) #define AIG_ABS(a) (((a) >= 0)? (a) :-(a)) -#define AIG_INFINITY (100000000) //////////////////////////////////////////////////////////////////////// /// DECLARATIONS /// @@ -133,7 +132,7 @@ Tim_Man_t * Tim_ManStart( int nPis, int nPos ) { p->pPis[i].Id = i; p->pPis[i].iObj2Box = p->pPis[i].iObj2Num = -1; - p->pPis[i].timeReq = AIG_INFINITY; + p->pPis[i].timeReq = TIME_ETERNITY; p->pPis[i].timeArr = 0.0; p->pPis[i].TravId = 0; } @@ -141,7 +140,7 @@ Tim_Man_t * Tim_ManStart( int nPis, int nPos ) { p->pPos[i].Id = i; p->pPos[i].iObj2Box = p->pPos[i].iObj2Num = -1; - p->pPos[i].timeReq = AIG_INFINITY; + p->pPos[i].timeReq = TIME_ETERNITY; p->pPos[i].timeArr = 0.0; p->pPos[i].TravId = 0; } @@ -673,7 +672,7 @@ float Tim_ManGetPiArrival( Tim_Man_t * p, int iPi ) Tim_ManBoxForEachOutput( p, pBox, pObjRes, i ) { pDelays = pBox->pDelayTable + i * pBox->nInputs; - DelayBest = -AIG_INFINITY; + DelayBest = -TIME_ETERNITY; Tim_ManBoxForEachInput( p, pBox, pObj, k ) DelayBest = AIG_MAX( DelayBest, pObj->timeArr + pDelays[k] ); pObjRes->timeArr = DelayBest; @@ -718,7 +717,7 @@ float Tim_ManGetPoRequired( Tim_Man_t * p, int iPo ) // compute the required times for each input of the box (POs) Tim_ManBoxForEachInput( p, pBox, pObjRes, i ) { - DelayBest = AIG_INFINITY; + DelayBest = TIME_ETERNITY; Tim_ManBoxForEachOutput( p, pBox, pObj, k ) { pDelays = pBox->pDelayTable + k * pBox->nInputs; diff --git a/src/aig/tim/tim.h b/src/aig/tim/tim.h index d092434e..d73a89d8 100644 --- a/src/aig/tim/tim.h +++ b/src/aig/tim/tim.h @@ -43,6 +43,7 @@ typedef struct Tim_Man_t_ Tim_Man_t; /// MACRO DEFINITIONS /// //////////////////////////////////////////////////////////////////////// +#define TIME_ETERNITY 10000 //////////////////////////////////////////////////////////////////////// /// ITERATORS /// -- cgit v1.2.3