From 94356f0d1fa8e671303299717f631ecf0ca2f17e Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Mon, 27 May 2013 14:39:08 -0700 Subject: Several small changes to the MFS packages. --- src/base/abci/abc.c | 6 +++--- src/base/abci/abcMfs.c | 3 ++- src/opt/mfs/mfs.h | 2 +- src/opt/mfs/mfsCore.c | 10 ++++++---- src/opt/mfs/mfsCore_.c | 1 - src/opt/mfs/mfsDiv.c | 11 ++++++----- src/opt/mfs/mfsInt.h | 1 + src/opt/mfs/mfsMan.c | 8 ++++---- src/opt/mfs/mfsResub.c | 4 ++-- src/opt/sfm/sfmWin.c | 1 + 10 files changed, 26 insertions(+), 21 deletions(-) diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c index 4493c361..d5bcb48f 100644 --- a/src/base/abci/abc.c +++ b/src/base/abci/abc.c @@ -4361,9 +4361,9 @@ int Abc_CommandMfs( Abc_Frame_t * pAbc, int argc, char ** argv ) Abc_Print( -1, "Command line switch \"-M\" should be followed by an integer.\n" ); goto usage; } - pPars->nWinSizeMax = atoi(argv[globalUtilOptind]); + pPars->nWinMax = atoi(argv[globalUtilOptind]); globalUtilOptind++; - if ( pPars->nWinSizeMax < 0 ) + if ( pPars->nWinMax < 0 ) goto usage; break; case 'L': @@ -4450,7 +4450,7 @@ usage: Abc_Print( -2, "\t-W : the number of levels in the TFO cone (0 <= num) [default = %d]\n", pPars->nWinTfoLevs ); Abc_Print( -2, "\t-F : the max number of fanouts to skip (1 <= num) [default = %d]\n", pPars->nFanoutsMax ); Abc_Print( -2, "\t-D : the max depth nodes to try (0 = no limit) [default = %d]\n", pPars->nDepthMax ); - Abc_Print( -2, "\t-M : the max node count of windows to consider (0 = no limit) [default = %d]\n", pPars->nWinSizeMax ); + Abc_Print( -2, "\t-M : the max node count of windows to consider (0 = no limit) [default = %d]\n", pPars->nWinMax ); Abc_Print( -2, "\t-L : the max increase in node level after resynthesis (0 <= num) [default = %d]\n", pPars->nGrowthLevel ); Abc_Print( -2, "\t-C : the max number of conflicts in one SAT run (0 = no limit) [default = %d]\n", pPars->nBTLimit ); Abc_Print( -2, "\t-d : toggle performing redundancy removal [default = %s]\n", pPars->fRrOnly? "yes": "no" ); diff --git a/src/base/abci/abcMfs.c b/src/base/abci/abcMfs.c index 76dfb162..dfd950dc 100644 --- a/src/base/abci/abcMfs.c +++ b/src/base/abci/abcMfs.c @@ -74,9 +74,10 @@ Vec_Ptr_t * Abc_NtkAssignIDs2( Abc_Ntk_t * pNtk ) vNodes = Vec_PtrAlloc( Abc_NtkNodeNum(pNtk) ); Abc_NtkForEachNode( pNtk, pObj, i ) { + pObj->iTemp = Abc_NtkCiNum(pNtk) + Vec_PtrSize(vNodes); Vec_PtrPush( vNodes, pObj ); - pObj->iTemp = Abc_NtkCiNum(pNtk) + i; } + assert( Vec_PtrSize(vNodes) == Abc_NtkNodeNum(pNtk) ); Abc_NtkForEachCo( pNtk, pObj, i ) pObj->iTemp = Abc_NtkCiNum(pNtk) + Vec_PtrSize(vNodes) + i; return vNodes; diff --git a/src/opt/mfs/mfs.h b/src/opt/mfs/mfs.h index 8292e617..4ca0df00 100644 --- a/src/opt/mfs/mfs.h +++ b/src/opt/mfs/mfs.h @@ -47,7 +47,7 @@ struct Mfs_Par_t_ int nFanoutsMax; // the maximum number of fanouts int nDepthMax; // the maximum number of logic levels int nDivMax; // the maximum number of divisors - int nWinSizeMax; // the maximum size of the window + int nWinMax; // the maximum size of the window int nGrowthLevel; // the maximum allowed growth in level int nBTLimit; // the maximum number of conflicts in one SAT run int fRrOnly; // perform redundance removal diff --git a/src/opt/mfs/mfsCore.c b/src/opt/mfs/mfsCore.c index d652d8cd..bb36b85c 100644 --- a/src/opt/mfs/mfsCore.c +++ b/src/opt/mfs/mfsCore.c @@ -50,8 +50,7 @@ void Abc_NtkMfsParsDefault( Mfs_Par_t * pPars ) pPars->nWinTfoLevs = 2; pPars->nFanoutsMax = 30; pPars->nDepthMax = 20; - pPars->nDivMax = 250; - pPars->nWinSizeMax = 300; + pPars->nWinMax = 300; pPars->nGrowthLevel = 0; pPars->nBTLimit = 5000; pPars->fRrOnly = 0; @@ -98,7 +97,7 @@ int Abc_WinNode(Mfs_Man_t * p, Abc_Obj_t *pNode) p->vRoots = Abc_MfsComputeRoots( pNode, p->pPars->nWinTfoLevs, p->pPars->nFanoutsMax ); p->vSupp = Abc_NtkNodeSupport( p->pNtk, (Abc_Obj_t **)Vec_PtrArray(p->vRoots), Vec_PtrSize(p->vRoots) ); p->vNodes = Abc_NtkDfsNodes( p->pNtk, (Abc_Obj_t **)Vec_PtrArray(p->vRoots), Vec_PtrSize(p->vRoots) ); - if ( p->pPars->nWinSizeMax && Vec_PtrSize(p->vNodes) > p->pPars->nWinSizeMax ) + if ( p->pPars->nWinMax && Vec_PtrSize(p->vNodes) > p->pPars->nWinMax ) return 1; // compute the divisors of the window p->vDivs = Abc_MfsComputeDivisors( p, pNode, Abc_ObjRequiredLevel(pNode) - 1 ); @@ -246,8 +245,11 @@ clk = clock(); p->vSupp = Abc_NtkNodeSupport( p->pNtk, (Abc_Obj_t **)Vec_PtrArray(p->vRoots), Vec_PtrSize(p->vRoots) ); p->vNodes = Abc_NtkDfsNodes( p->pNtk, (Abc_Obj_t **)Vec_PtrArray(p->vRoots), Vec_PtrSize(p->vRoots) ); p->timeWin += clock() - clk; - if ( p->pPars->nWinSizeMax && Vec_PtrSize(p->vNodes) > p->pPars->nWinSizeMax ) + if ( p->pPars->nWinMax && Vec_PtrSize(p->vNodes) > p->pPars->nWinMax ) + { + p->nMaxDivs++; return 1; + } // compute the divisors of the window clk = clock(); p->vDivs = Abc_MfsComputeDivisors( p, pNode, Abc_ObjRequiredLevel(pNode) - 1 ); diff --git a/src/opt/mfs/mfsCore_.c b/src/opt/mfs/mfsCore_.c index 49105da6..38e407bc 100644 --- a/src/opt/mfs/mfsCore_.c +++ b/src/opt/mfs/mfsCore_.c @@ -48,7 +48,6 @@ void Abc_NtkMfsParsDefault( Mfs_Par_t * pPars ) pPars->nWinTfoLevs = 2; pPars->nFanoutsMax = 10; pPars->nDepthMax = 20; - pPars->nDivMax = 250; pPars->nWinSizeMax = 300; pPars->nGrowthLevel = 0; pPars->nBTLimit = 5000; diff --git a/src/opt/mfs/mfsDiv.c b/src/opt/mfs/mfsDiv.c index 0b29673e..ece8ec64 100644 --- a/src/opt/mfs/mfsDiv.c +++ b/src/opt/mfs/mfsDiv.c @@ -223,7 +223,7 @@ Vec_Ptr_t * Abc_MfsComputeDivisors( Mfs_Man_t * p, Abc_Obj_t * pNode, int nLevDi // nodes to be avoided as divisors are marked with current trav ID // start collecting the divisors - vDivs = Vec_PtrAlloc( p->pPars->nDivMax ); + vDivs = Vec_PtrAlloc( p->pPars->nWinMax ); Vec_PtrForEachEntry( Abc_Obj_t *, vCone, pObj, k ) { if ( !Abc_NodeIsTravIdPrevious(pObj) ) @@ -231,13 +231,13 @@ Vec_Ptr_t * Abc_MfsComputeDivisors( Mfs_Man_t * p, Abc_Obj_t * pNode, int nLevDi if ( (int)pObj->Level > nLevDivMax ) continue; Vec_PtrPush( vDivs, pObj ); - if ( Vec_PtrSize(vDivs) >= p->pPars->nDivMax ) + if ( Vec_PtrSize(vDivs) >= p->pPars->nWinMax ) break; } Vec_PtrFree( vCone ); // explore the fanouts of already collected divisors - if ( Vec_PtrSize(vDivs) < p->pPars->nDivMax ) + if ( Vec_PtrSize(vDivs) < p->pPars->nWinMax ) Vec_PtrForEachEntry( Abc_Obj_t *, vDivs, pObj, k ) { // consider fanouts of this node @@ -273,12 +273,13 @@ Vec_Ptr_t * Abc_MfsComputeDivisors( Mfs_Man_t * p, Abc_Obj_t * pNode, int nLevDi Vec_PtrPushUnique( p->vNodes, pFanout ); Abc_NodeSetTravIdPrevious( pFanout ); nDivsPlus++; - if ( Vec_PtrSize(vDivs) >= p->pPars->nDivMax ) + if ( Vec_PtrSize(vDivs) >= p->pPars->nWinMax ) break; } - if ( Vec_PtrSize(vDivs) >= p->pPars->nDivMax ) + if ( Vec_PtrSize(vDivs) >= p->pPars->nWinMax ) break; } + p->nMaxDivs += (Vec_PtrSize(vDivs) >= p->pPars->nWinMax); // sort the divisors by level in the increasing order Vec_PtrSort( vDivs, (int (*)(void))Abc_NodeCompareLevelsIncrease ); diff --git a/src/opt/mfs/mfsInt.h b/src/opt/mfs/mfsInt.h index 23a59833..ddaa323d 100644 --- a/src/opt/mfs/mfsInt.h +++ b/src/opt/mfs/mfsInt.h @@ -114,6 +114,7 @@ struct Mfs_Man_t_ int nTimeOuts; int nTimeOutsLevel; int nDcMints; + int nMaxDivs; double dTotalRatios; // node/edge stats int nTotalNodesBeg; diff --git a/src/opt/mfs/mfsMan.c b/src/opt/mfs/mfsMan.c index 6042f15e..1132275f 100644 --- a/src/opt/mfs/mfsMan.c +++ b/src/opt/mfs/mfsMan.c @@ -52,8 +52,8 @@ Mfs_Man_t * Mfs_ManAlloc( Mfs_Par_t * pPars ) p->vProjVarsCnf = Vec_IntAlloc( 100 ); p->vProjVarsSat = Vec_IntAlloc( 100 ); p->vDivLits = Vec_IntAlloc( 100 ); - p->nDivWords = Abc_BitWordNum(p->pPars->nDivMax + MFS_FANIN_MAX); - p->vDivCexes = Vec_PtrAllocSimInfo( p->pPars->nDivMax+MFS_FANIN_MAX+1, p->nDivWords ); + p->nDivWords = Abc_BitWordNum(p->pPars->nWinMax + MFS_FANIN_MAX); + p->vDivCexes = Vec_PtrAllocSimInfo( p->pPars->nWinMax + MFS_FANIN_MAX + 1, p->nDivWords ); p->pMan = Int_ManAlloc(); p->vMem = Vec_IntAlloc( 0 ); p->vLevels = Vec_VecStart( 32 ); @@ -112,8 +112,8 @@ void Mfs_ManPrint( Mfs_Man_t * p ) { if ( p->pPars->fResub ) { - printf( "Nodes = %d. Try = %d. Resub = %d. Div = %d. SAT calls = %d. Timeouts = %d.\n", - p->nTotalNodesBeg, p->nNodesTried, p->nNodesResub, p->nTotalDivs, p->nSatCalls, p->nTimeOuts ); + printf( "Nodes = %d. Try = %d. Resub = %d. Div = %d. SAT calls = %d. Timeouts = %d. MaxDivs = %d.\n", + p->nTotalNodesBeg, p->nNodesTried, p->nNodesResub, p->nTotalDivs, p->nSatCalls, p->nTimeOuts, p->nMaxDivs ); printf( "Attempts : " ); printf( "Remove %6d out of %6d (%6.2f %%) ", p->nRemoves, p->nTryRemoves, 100.0*p->nRemoves/Abc_MaxInt(1, p->nTryRemoves) ); diff --git a/src/opt/mfs/mfsResub.c b/src/opt/mfs/mfsResub.c index 85eb8140..694b366c 100644 --- a/src/opt/mfs/mfsResub.c +++ b/src/opt/mfs/mfsResub.c @@ -297,7 +297,7 @@ p->timeInt += clock() - clk; p->nResubs++; return 1; } - if ( p->nCexes >= p->pPars->nDivMax ) + if ( p->nCexes >= p->pPars->nWinMax ) break; } if ( p->pPars->fVeryVerbose ) @@ -467,7 +467,7 @@ clk = clock(); p->timeInt += clock() - clk; return 1; } - if ( p->nCexes >= p->pPars->nDivMax ) + if ( p->nCexes >= p->pPars->nWinMax ) break; } return 0; diff --git a/src/opt/sfm/sfmWin.c b/src/opt/sfm/sfmWin.c index 3c30c480..9efe30d3 100644 --- a/src/opt/sfm/sfmWin.c +++ b/src/opt/sfm/sfmWin.c @@ -275,6 +275,7 @@ int Sfm_NtkCreateWindow( Sfm_Ntk_t * p, int iNode, int fVerbose ) Sfm_NtkIncrementTravId( p ); if ( Sfm_NtkCollectTfi_rec( p, iNode, p->pPars->nWinSizeMax ) ) { + p->nMaxDivs++; p->timeWin += clock() - clk; return 0; } -- cgit v1.2.3