diff options
Diffstat (limited to 'src')
| -rw-r--r-- | src/base/abci/abc.c | 16 | ||||
| -rw-r--r-- | src/opt/mfs/mfs.h | 1 | ||||
| -rw-r--r-- | src/opt/mfs/mfsCore.c | 1 | ||||
| -rw-r--r-- | src/opt/mfs/mfsInt.h | 4 | ||||
| -rw-r--r-- | src/opt/mfs/mfsMan.c | 43 | ||||
| -rw-r--r-- | src/opt/mfs/mfsResub.c | 7 | ||||
| -rw-r--r-- | src/opt/sfm/sfm.h | 3 | ||||
| -rw-r--r-- | src/opt/sfm/sfmCore.c | 26 | ||||
| -rw-r--r-- | src/opt/sfm/sfmInt.h | 3 | ||||
| -rw-r--r-- | src/opt/sfm/sfmSat.c | 31 | ||||
| -rw-r--r-- | src/opt/sfm/sfmWin.c | 84 |
11 files changed, 100 insertions, 119 deletions
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c index b5e1ebee..5f100fb0 100644 --- a/src/base/abci/abc.c +++ b/src/base/abci/abc.c @@ -4304,7 +4304,7 @@ int Abc_CommandMfs( Abc_Frame_t * pAbc, int argc, char ** argv ) // set defaults Abc_NtkMfsParsDefault( pPars ); Extra_UtilGetoptReset(); - while ( ( c = Extra_UtilGetopt( argc, argv, "WFDMLCraestpgvwh" ) ) != EOF ) + while ( ( c = Extra_UtilGetopt( argc, argv, "WFDMLCdraestpgvwh" ) ) != EOF ) { switch ( c ) { @@ -4374,6 +4374,9 @@ int Abc_CommandMfs( Abc_Frame_t * pAbc, int argc, char ** argv ) if ( pPars->nBTLimit < 0 ) goto usage; break; + case 'd': + pPars->fRrOnly ^= 1; + break; case 'r': pPars->fResub ^= 1; break; @@ -4428,7 +4431,7 @@ int Abc_CommandMfs( Abc_Frame_t * pAbc, int argc, char ** argv ) return 0; usage: - Abc_Print( -2, "usage: mfs [-WFDMLC <num>] [-raestpgvh]\n" ); + Abc_Print( -2, "usage: mfs [-WFDMLC <num>] [-draestpgvh]\n" ); Abc_Print( -2, "\t performs don't-care-based optimization of logic networks\n" ); Abc_Print( -2, "\t-W <num> : the number of levels in the TFO cone (0 <= num) [default = %d]\n", pPars->nWinTfoLevs ); Abc_Print( -2, "\t-F <num> : the max number of fanouts to skip (1 <= num) [default = %d]\n", pPars->nFanoutsMax ); @@ -4436,6 +4439,7 @@ usage: Abc_Print( -2, "\t-M <num> : the max node count of windows to consider (0 = no limit) [default = %d]\n", pPars->nWinSizeMax ); Abc_Print( -2, "\t-L <num> : the max increase in node level after resynthesis (0 <= num) [default = %d]\n", pPars->nGrowthLevel ); Abc_Print( -2, "\t-C <num> : 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" ); Abc_Print( -2, "\t-r : toggle resubstitution and dc-minimization [default = %s]\n", pPars->fResub? "resub": "dc-min" ); Abc_Print( -2, "\t-a : toggle minimizing area or area+edges [default = %s]\n", pPars->fArea? "area": "area+edges" ); Abc_Print( -2, "\t-e : toggle high-effort resubstitution [default = %s]\n", pPars->fMoreEffort? "yes": "no" ); @@ -4469,7 +4473,7 @@ int Abc_CommandMfs2( Abc_Frame_t * pAbc, int argc, char ** argv ) // set defaults Sfm_ParSetDefault( pPars ); Extra_UtilGetoptReset(); - while ( ( c = Extra_UtilGetopt( argc, argv, "WFDMNClaevwh" ) ) != EOF ) + while ( ( c = Extra_UtilGetopt( argc, argv, "WFDMNCdlaevwh" ) ) != EOF ) { switch ( c ) { @@ -4539,6 +4543,9 @@ int Abc_CommandMfs2( Abc_Frame_t * pAbc, int argc, char ** argv ) if ( pPars->nBTLimit < 0 ) goto usage; break; + case 'd': + pPars->fRrOnly ^= 1; + break; case 'l': pPars->fFixLevel ^= 1; break; @@ -4584,7 +4591,7 @@ int Abc_CommandMfs2( Abc_Frame_t * pAbc, int argc, char ** argv ) return 0; usage: - Abc_Print( -2, "usage: mfs2 [-WFDMNC <num>] [-laevwh]\n" ); + Abc_Print( -2, "usage: mfs2 [-WFDMNC <num>] [-dlaevwh]\n" ); Abc_Print( -2, "\t performs don't-care-based optimization of logic networks\n" ); Abc_Print( -2, "\t-W <num> : the number of levels in the TFO cone (0 <= num) [default = %d]\n", pPars->nTfoLevMax ); Abc_Print( -2, "\t-F <num> : the max number of fanouts to skip (1 <= num) [default = %d]\n", pPars->nFanoutMax ); @@ -4592,6 +4599,7 @@ usage: Abc_Print( -2, "\t-M <num> : the max node count of windows to consider (0 = no limit) [default = %d]\n", pPars->nWinSizeMax ); Abc_Print( -2, "\t-N <num> : the max number of divisors to consider (0 = no limit) [default = %d]\n", pPars->nDivNumMax ); Abc_Print( -2, "\t-C <num> : 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" ); Abc_Print( -2, "\t-l : allow logic level to increase [default = %s]\n", !pPars->fFixLevel? "yes": "no" ); Abc_Print( -2, "\t-a : toggle minimizing area or area+edges [default = %s]\n", pPars->fArea? "area": "area+edges" ); Abc_Print( -2, "\t-e : toggle high-effort resubstitution [default = %s]\n", pPars->fMoreEffort? "yes": "no" ); diff --git a/src/opt/mfs/mfs.h b/src/opt/mfs/mfs.h index 9916b582..8292e617 100644 --- a/src/opt/mfs/mfs.h +++ b/src/opt/mfs/mfs.h @@ -50,6 +50,7 @@ struct Mfs_Par_t_ int nWinSizeMax; // 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 int fResub; // performs resubstitution int fArea; // performs optimization for area int fMoreEffort; // performs high-affort minimization diff --git a/src/opt/mfs/mfsCore.c b/src/opt/mfs/mfsCore.c index 9e50333f..22a28e22 100644 --- a/src/opt/mfs/mfsCore.c +++ b/src/opt/mfs/mfsCore.c @@ -54,6 +54,7 @@ void Abc_NtkMfsParsDefault( Mfs_Par_t * pPars ) pPars->nWinSizeMax = 300; pPars->nGrowthLevel = 0; pPars->nBTLimit = 5000; + pPars->fRrOnly = 0; pPars->fResub = 1; pPars->fArea = 0; pPars->fMoreEffort = 0; diff --git a/src/opt/mfs/mfsInt.h b/src/opt/mfs/mfsInt.h index 44346997..23a59833 100644 --- a/src/opt/mfs/mfsInt.h +++ b/src/opt/mfs/mfsInt.h @@ -101,6 +101,10 @@ struct Mfs_Man_t_ int nCares; // the number of care minterms unsigned uCare[(MFS_FANIN_MAX<=5)?1:1<<(MFS_FANIN_MAX-5)]; // the computed care-set // performance statistics + int nTryRemoves; // number of fanin removals + int nTryResubs; // number of resubstitutions + int nRemoves; // number of fanin removals + int nResubs; // number of resubstitutions int nNodesTried; int nNodesResub; int nMintsCare; diff --git a/src/opt/mfs/mfsMan.c b/src/opt/mfs/mfsMan.c index caa82e68..3ed6436f 100644 --- a/src/opt/mfs/mfsMan.c +++ b/src/opt/mfs/mfsMan.c @@ -112,43 +112,26 @@ void Mfs_ManPrint( Mfs_Man_t * p ) { if ( p->pPars->fResub ) { -/* - printf( "Reduction in nodes = %5d. (%.2f %%) ", - p->nTotalNodesBeg-p->nTotalNodesEnd, - 100.0*(p->nTotalNodesBeg-p->nTotalNodesEnd)/p->nTotalNodesBeg ); - printf( "Reduction in edges = %5d. (%.2f %%) ", - p->nTotalEdgesBeg-p->nTotalEdgesEnd, - 100.0*(p->nTotalEdgesBeg-p->nTotalEdgesEnd)/p->nTotalEdgesBeg ); - printf( "\n" ); - printf( "Nodes = %d. Try = %d. Resub = %d. Div = %d. SAT calls = %d. Timeouts = %d.\n", + printf( "Nodes = %d. Try = %d. Resub = %d. Div = %d. SAT calls = %d. Timeouts = %d.\n", Abc_NtkNodeNum(p->pNtk), p->nNodesTried, p->nNodesResub, p->nTotalDivs, p->nSatCalls, p->nTimeOuts ); - if ( p->pPars->fSwapEdge ) - printf( "Swappable edges = %d. Total edges = %d. Ratio = %5.2f.\n", - p->nNodesResub, Abc_NtkGetTotalFanins(p->pNtk), 1.00 * p->nNodesResub / Abc_NtkGetTotalFanins(p->pNtk) ); - else - Abc_NtkMfsPrintResubStats( p ); -// printf( "Average ratio of DCs in the resubed nodes = %.2f.\n", 1.0*p->nDcMints/(64 * p->nNodesResub) ); -*/ - printf( "@@@------- Node( %4d, %4.2f%% ), ", - p->nTotalNodesBeg-p->nTotalNodesEnd, - 100.0*(p->nTotalNodesBeg-p->nTotalNodesEnd)/p->nTotalNodesBeg ); - printf( "Edge( %4d, %4.2f%% ), ", - p->nTotalEdgesBeg-p->nTotalEdgesEnd, - 100.0*(p->nTotalEdgesBeg-p->nTotalEdgesEnd)/p->nTotalEdgesBeg ); + + printf( "Attempts : " ); + printf( "Remove %6d out of %6d (%6.2f %%) ", p->nRemoves, p->nTryRemoves, 100.0*p->nRemoves/Abc_MaxInt(1, p->nTryRemoves) ); + printf( "Resub %6d out of %6d (%6.2f %%) ", p->nResubs, p->nTryResubs, 100.0*p->nResubs /Abc_MaxInt(1, p->nTryResubs) ); + printf( "\n" ); + + printf( "Reduction: " ); + printf( "Nodes %6d out of %6d (%6.2f %%) ", p->nTotalNodesBeg-p->nTotalNodesEnd, p->nTotalNodesEnd, 100.0*(p->nTotalNodesBeg-p->nTotalNodesEnd)/Abc_MaxInt(1, p->nTotalNodesBeg) ); + printf( "Edges %6d out of %6d (%6.2f %%) ", p->nTotalEdgesBeg-p->nTotalEdgesEnd, p->nTotalEdgesEnd, 100.0*(p->nTotalEdgesBeg-p->nTotalEdgesEnd)/Abc_MaxInt(1, p->nTotalEdgesBeg) ); + printf( "\n" ); + if (p->pPars->fPower) - printf( "Power( %5.2f, %4.2f%%) ", + printf( "Power( %5.2f, %4.2f%%) \n", p->TotalSwitchingBeg - p->TotalSwitchingEnd, 100.0*(p->TotalSwitchingBeg-p->TotalSwitchingEnd)/p->TotalSwitchingBeg ); - printf( "\n" ); -//#if 0 - printf( "Nodes = %d. Try = %d. Resub = %d. Div = %d. SAT calls = %d. Timeouts = %d.\n", - Abc_NtkNodeNum(p->pNtk), p->nNodesTried, p->nNodesResub, p->nTotalDivs, p->nSatCalls, p->nTimeOuts ); -//#endif if ( p->pPars->fSwapEdge ) printf( "Swappable edges = %d. Total edges = %d. Ratio = %5.2f.\n", p->nNodesResub, Abc_NtkGetTotalFanins(p->pNtk), 1.00 * p->nNodesResub / Abc_NtkGetTotalFanins(p->pNtk) ); - else - Abc_NtkMfsPrintResubStats( p ); // printf( "Average ratio of DCs in the resubed nodes = %.2f.\n", 1.0*p->nDcMints/(64 * p->nNodesResub) ); } else diff --git a/src/opt/mfs/mfsResub.c b/src/opt/mfs/mfsResub.c index 0d144f9b..0ecd0f67 100644 --- a/src/opt/mfs/mfsResub.c +++ b/src/opt/mfs/mfsResub.c @@ -172,6 +172,7 @@ int Abc_NtkMfsSolveSatResub( Mfs_Man_t * p, Abc_Obj_t * pNode, int iFanin, int f Abc_Obj_t * pFanin; Hop_Obj_t * pFunc; assert( iFanin >= 0 ); + p->nTryRemoves++; // clean simulation info Vec_PtrFillSimInfo( p->vDivCexes, 0, p->nDivWords ); @@ -215,13 +216,14 @@ clk = clock(); // update the network Abc_NtkMfsUpdateNetwork( p, pNode, p->vMfsFanins, pFunc ); p->timeInt += clock() - clk; + p->nRemoves++; return 1; } - if ( fOnlyRemove ) + if ( fOnlyRemove || p->pPars->fRrOnly ) return 0; -// return 0; + p->nTryResubs++; if ( fVeryVerbose ) { for ( i = 0; i < 9; i++ ) @@ -292,6 +294,7 @@ clk = clock(); Vec_PtrPush( p->vMfsFanins, Vec_PtrEntry(p->vDivs, iVar) ); Abc_NtkMfsUpdateNetwork( p, pNode, p->vMfsFanins, pFunc ); p->timeInt += clock() - clk; + p->nResubs++; return 1; } if ( p->nCexes >= p->pPars->nDivMax ) diff --git a/src/opt/sfm/sfm.h b/src/opt/sfm/sfm.h index f6380e65..c34ae859 100644 --- a/src/opt/sfm/sfm.h +++ b/src/opt/sfm/sfm.h @@ -45,10 +45,11 @@ struct Sfm_Par_t_ int nTfoLevMax; // the maximum fanout levels int nFanoutMax; // the maximum number of fanouts int nDepthMax; // the maximum depth to try - int nDivNumMax; // the maximum number of divisors int nWinSizeMax; // the maximum window size + int nDivNumMax; // the maximum number of divisors int nBTLimit; // the maximum number of conflicts in one SAT run int fFixLevel; // does not allow level to increase + int fRrOnly; // perform redundance removal int fArea; // performs optimization for area int fMoreEffort; // performs high-affort minimization int fVerbose; // enable basic stats diff --git a/src/opt/sfm/sfmCore.c b/src/opt/sfm/sfmCore.c index e9721ec7..9d96a1ac 100644 --- a/src/opt/sfm/sfmCore.c +++ b/src/opt/sfm/sfmCore.c @@ -47,11 +47,12 @@ void Sfm_ParSetDefault( Sfm_Par_t * pPars ) memset( pPars, 0, sizeof(Sfm_Par_t) ); pPars->nTfoLevMax = 2; // the maximum fanout levels pPars->nFanoutMax = 10; // the maximum number of fanouts - pPars->nDepthMax = 0; // the maximum depth to try - pPars->nDivNumMax = 300; // the maximum number of divisors + pPars->nDepthMax = 20; // the maximum depth to try pPars->nWinSizeMax = 300; // the maximum window size + pPars->nDivNumMax = 300; // the maximum number of divisors pPars->nBTLimit = 0; // the maximum number of conflicts in one SAT run pPars->fFixLevel = 1; // does not allow level to increase + pPars->fRrOnly = 0; // perform redundancy removal pPars->fArea = 0; // performs optimization for area pPars->fMoreEffort = 0; // performs high-affort minimization pPars->fVerbose = 0; // enable basic stats @@ -76,13 +77,13 @@ void Sfm_NtkPrintStats( Sfm_Ntk_t * p ) Sfm_NtkNodeNum(p), p->nNodesTried, p->nRemoves + p->nResubs, p->nTotalDivs, p->nSatCalls, p->nTimeOuts ); printf( "Attempts : " ); - printf( "Remove %6d -> %6d (%6.2f %%) ", p->nTryRemoves, p->nRemoves, 100.0*p->nRemoves/Abc_MaxInt(1, p->nTryRemoves) ); - printf( "Resub %6d -> %6d (%6.2f %%) ", p->nTryResubs, p->nResubs, 100.0*p->nResubs /Abc_MaxInt(1, p->nTryResubs) ); + printf( "Remove %6d out of %6d (%6.2f %%) ", p->nRemoves, p->nTryRemoves, p->nRemoves, 100.0*p->nRemoves/Abc_MaxInt(1, p->nTryRemoves) ); + printf( "Resub %6d out of %6d (%6.2f %%) ", p->nResubs, p->nTryResubs, p->nResubs, 100.0*p->nResubs /Abc_MaxInt(1, p->nTryResubs) ); printf( "\n" ); printf( "Reduction: " ); - printf( "Nodes %6d -> %6d (%6.2f %%) ", p->nTotalNodesBeg, p->nTotalNodesEnd, 100.0*(p->nTotalNodesBeg-p->nTotalNodesEnd)/Abc_MaxInt(1, p->nTotalNodesBeg) ); - printf( "Edges %6d -> %6d (%6.2f %%) ", p->nTotalEdgesBeg, p->nTotalEdgesEnd, 100.0*(p->nTotalEdgesBeg-p->nTotalEdgesEnd)/Abc_MaxInt(1, p->nTotalEdgesBeg) ); + printf( "Nodes %6d out of %6d (%6.2f %%) ", p->nTotalNodesBeg-p->nTotalNodesEnd, p->nTotalNodesEnd, 100.0*(p->nTotalNodesBeg-p->nTotalNodesEnd)/Abc_MaxInt(1, p->nTotalNodesBeg) ); + printf( "Edges %6d out of %6d (%6.2f %%) ", p->nTotalEdgesBeg-p->nTotalEdgesEnd, p->nTotalEdgesEnd, 100.0*(p->nTotalEdgesBeg-p->nTotalEdgesEnd)/Abc_MaxInt(1, p->nTotalEdgesBeg) ); printf( "\n" ); ABC_PRTP( "Win", p->timeWin , p->timeTotal ); @@ -117,10 +118,7 @@ int Sfm_NodeResubSolve( Sfm_Ntk_t * p, int iNode, int f, int fRemoveOnly ) { int i = 0; } - if ( fRemoveOnly ) - p->nTryRemoves++; - else - p->nTryResubs++; + p->nTryRemoves++; // report init stats if ( p->pPars->fVeryVerbose ) printf( "%5d : Lev =%3d. Leaf =%3d. Node =%3d. Div=%3d. Fanin = %d/%d. MFFC = %d\n", @@ -145,10 +143,10 @@ p->timeSat += clock() - clk; } if ( uTruth != SFM_SAT_SAT ) goto finish; - if ( fRemoveOnly || Vec_IntSize(p->vDivs) == 0 ) + if ( fRemoveOnly || p->pPars->fRrOnly || Vec_IntSize(p->vDivs) == 0 ) return 0; -// return 0; + p->nTryResubs++; if ( fVeryVerbose ) { for ( i = 0; i < 9; i++ ) @@ -197,7 +195,8 @@ finish: if ( iVar == -1 ) printf( "Node %d: Fanin %d (%d) can be removed. ", iNode, f, Sfm_ObjFanin(p, iNode, f) ); else - printf( "Node %d: Fanin %d (%d) can be replaced by divisor %d. ", iNode, f, Sfm_ObjFanin(p, iNode, f), iVar ); + printf( "Node %d: Fanin %d (%d) can be replaced by divisor %d (%d). ", + iNode, f, Sfm_ObjFanin(p, iNode, f), iVar, Vec_IntEntry(p->vDivs, iVar) ); Kit_DsdPrintFromTruth( (unsigned *)&uTruth, Vec_IntSize(p->vDivIds) ); printf( "\n" ); } if ( iVar == -1 ) @@ -218,7 +217,6 @@ int Sfm_NodeResub( Sfm_Ntk_t * p, int iNode ) if ( !Sfm_NtkCreateWindow( p, iNode, p->pPars->fVeryVerbose ) ) return 0; Sfm_NtkWindowToSolver( p ); - Sfm_NtkPrepareDivisors( p, iNode ); // try replacing area critical fanins Sfm_ObjForEachFanin( p, iNode, iFanin, i ) if ( Sfm_ObjIsNode(p, iFanin) && Sfm_ObjFanoutNum(p, iFanin) == 1 ) diff --git a/src/opt/sfm/sfmInt.h b/src/opt/sfm/sfmInt.h index 5c41e9f0..bdb1c600 100644 --- a/src/opt/sfm/sfmInt.h +++ b/src/opt/sfm/sfmInt.h @@ -152,6 +152,7 @@ static inline void Sfm_ObjSetLevel( Sfm_Ntk_t * p, int iObj, int Lev ) { Vec_In static inline int Sfm_ObjUpdateFaninCount( Sfm_Ntk_t * p, int iObj ) { return Vec_IntAddToEntry(&p->vCounts, iObj, -1); } static inline void Sfm_ObjResetFaninCount( Sfm_Ntk_t * p, int iObj ) { Vec_IntWriteEntry(&p->vCounts, iObj, Sfm_ObjFaninNum(p, iObj)-1); } +extern void Kit_DsdPrintFromTruth( unsigned * pTruth, int nVars ); //////////////////////////////////////////////////////////////////////// /// MACRO DEFINITIONS /// @@ -181,8 +182,6 @@ extern word Sfm_ComputeInterpolant( Sfm_Ntk_t * p ); /*=== sfmWin.c ==========================================================*/ extern int Sfm_ObjMffcSize( Sfm_Ntk_t * p, int iObj ); extern int Sfm_NtkCreateWindow( Sfm_Ntk_t * p, int iNode, int fVerbose ); -extern void Sfm_NtkPrepareDivisors( Sfm_Ntk_t * p, int iNode ); - ABC_NAMESPACE_HEADER_END diff --git a/src/opt/sfm/sfmSat.c b/src/opt/sfm/sfmSat.c index 4a06dde6..228a5fd8 100644 --- a/src/opt/sfm/sfmSat.c +++ b/src/opt/sfm/sfmSat.c @@ -42,28 +42,6 @@ static word s_Truths6[6] = { /**Function************************************************************* - Synopsis [Creates order of objects in the SAT solver.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Sfm_NtkOrderObjects( Sfm_Ntk_t * p ) -{ - int i, iNode; - assert( Vec_IntEntryLast(p->vNodes) == Vec_IntEntry(p->vDivs, Vec_IntSize(p->vLeaves) + Vec_IntSize(p->vNodes) - 1) ); - Vec_IntClear( p->vOrder ); - Vec_IntForEachEntryReverse( p->vNodes, iNode, i ) - Vec_IntPush( p->vOrder, iNode ); - Vec_IntForEachEntryStart( p->vDivs, iNode, i, Vec_IntSize(p->vLeaves) + Vec_IntSize(p->vNodes) ) - Vec_IntPush( p->vOrder, iNode ); -} - -/**Function************************************************************* - Synopsis [Converts a window into a SAT solver.] Description [] @@ -85,14 +63,17 @@ void Sfm_NtkWindowToSolver( Sfm_Ntk_t * p ) // create SAT variables Sfm_NtkCleanVars( p ); p->nSatVars = 1; - Sfm_NtkOrderObjects( p ); Vec_IntForEachEntry( p->vOrder, iNode, i ) Sfm_ObjSetSatVar( p, iNode, p->nSatVars++ ); - Vec_IntForEachEntry( p->vLeaves, iNode, i ) - Sfm_ObjSetSatVar( p, iNode, p->nSatVars++ ); + // create divisor variables + Vec_IntClear( p->vDivVars ); + Vec_IntForEachEntry( p->vDivs, iNode, i ) + Vec_IntPush( p->vDivVars, Sfm_ObjSatVar(p, iNode) ); // add CNF clauses for the TFI Vec_IntForEachEntry( p->vOrder, iNode, i ) { + if ( Sfm_ObjIsPi(p, iNode) ) + continue; // collect fanin variables Vec_IntClear( p->vFaninMap ); Sfm_ObjForEachFanin( p, iNode, iFanin, k ) diff --git a/src/opt/sfm/sfmWin.c b/src/opt/sfm/sfmWin.c index 887bf0f7..f96221c0 100644 --- a/src/opt/sfm/sfmWin.c +++ b/src/opt/sfm/sfmWin.c @@ -265,14 +265,51 @@ int Sfm_NtkCreateWindow( Sfm_Ntk_t * p, int iNode, int fVerbose ) else Vec_IntPush( p->vRoots, iNode ); p->timeWin += clock() - clk; - // collect divisors of the TFI nodes clk = clock(); - Vec_IntAppend( p->vDivs, p->vLeaves ); - Vec_IntAppend( p->vDivs, p->vNodes ); + // create ordering of the nodes + Vec_IntClear( p->vOrder ); + Vec_IntForEachEntryReverse( p->vNodes, iNode, i ) + Vec_IntPush( p->vOrder, iNode ); + Vec_IntForEachEntry( p->vLeaves, iNode, i ) + Vec_IntPush( p->vOrder, iNode ); + // mark fanins Sfm_NtkIncrementTravId2( p ); - Vec_IntForEachEntry( p->vDivs, iTemp, i ) - if ( iTemp != iNode && Vec_IntSize(p->vDivs) < p->pPars->nDivNumMax ) - Sfm_NtkAddDivisors( p, iTemp, Sfm_ObjLevel(p, iNode) ); + Sfm_ObjSetTravIdCurrent2( p, iNode ); + Sfm_ObjForEachFanin( p, iNode, iTemp, i ) + Sfm_ObjSetTravIdCurrent2( p, iTemp ); + // compact divisors + Vec_IntClear( p->vDivs ); + Vec_IntForEachEntry( p->vLeaves, iTemp, i ) + if ( !Sfm_ObjIsTravIdCurrent2( p, iTemp ) ) + Vec_IntPush( p->vDivs, iTemp ); + Vec_IntForEachEntry( p->vNodes, iTemp, i ) + if ( !Sfm_ObjIsTravIdCurrent2( p, iTemp ) ) + Vec_IntPush( p->vDivs, iTemp ); + // if we exceed the limit, remove the first few + if ( Vec_IntSize(p->vDivs) > p->pPars->nDivNumMax ) + { + int k = 0; + Vec_IntForEachEntryStart( p->vDivs, iTemp, i, Vec_IntSize(p->vDivs) - p->pPars->nDivNumMax ) + Vec_IntWriteEntry( p->vDivs, k++, iTemp ); + Vec_IntShrink( p->vDivs, k ); + assert( Vec_IntSize(p->vDivs) == p->pPars->nDivNumMax ); + } + // collect additional divisors of the TFI nodes + if ( Vec_IntSize(p->vDivs) < p->pPars->nDivNumMax ) + { + int nStartNew = Vec_IntSize(p->vDivs); + Sfm_NtkIncrementTravId2( p ); + Vec_IntForEachEntry( p->vDivs, iTemp, i ) + if ( Vec_IntSize(p->vDivs) < p->pPars->nDivNumMax ) + Sfm_NtkAddDivisors( p, iTemp, Sfm_ObjLevel(p, iNode) ); + if ( Vec_IntSize(p->vDivs) > p->pPars->nDivNumMax ) + Vec_IntShrink( p->vDivs, p->pPars->nDivNumMax ); + // add new divisor variable to the order + Vec_IntForEachEntryStart( p->vDivs, iTemp, i, nStartNew ) + Vec_IntPush( p->vOrder, iTemp ); + } + assert( Vec_IntSize(p->vDivs) <= p->pPars->nDivNumMax ); + // statistics p->nTotalDivs += Vec_IntSize(p->vDivs); p->timeDiv += clock() - clk; if ( !fVerbose ) @@ -294,41 +331,6 @@ void Sfm_NtkWindowTest( Sfm_Ntk_t * p, int iNode ) Sfm_NtkCreateWindow( p, i, 1 ); } -/**Function************************************************************* - - Synopsis [Removes node and its fanins from the array of divisors.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Sfm_NtkPrepareDivisors( Sfm_Ntk_t * p, int iNode ) -{ - int i, iFanin, k = 0; - // mark fanins - Sfm_NtkIncrementTravId( p ); - Sfm_ObjSetTravIdCurrent( p, iNode ); - Sfm_ObjForEachFanin( p, iNode, iFanin, i ) - Sfm_ObjSetTravIdCurrent( p, iFanin ); - // compact divisors - Vec_IntClear( p->vDivVars ); - Vec_IntForEachEntry( p->vDivs, iFanin, i ) - if ( !Sfm_ObjIsTravIdCurrent( p, iFanin ) ) - { - Vec_IntPush( p->vDivVars, Sfm_ObjSatVar(p, iFanin) ); - Vec_IntWriteEntry( p->vDivs, k++, iFanin ); - } - assert( Vec_IntSize(p->vDivs) == k + Sfm_ObjFaninNum(p, iNode) + 1 ); - Vec_IntShrink( p->vDivs, k ); - // collect fanins -// Vec_IntClear( p->vFans ); -// Sfm_ObjForEachFanin( p, iNode, iFanin, i ) -// Vec_IntPush( p->vFans, iFanin ); -} - //////////////////////////////////////////////////////////////////////// /// END OF FILE /// //////////////////////////////////////////////////////////////////////// |