diff options
author | Alan Mishchenko <alanmi@berkeley.edu> | 2013-05-26 13:34:24 -0700 |
---|---|---|
committer | Alan Mishchenko <alanmi@berkeley.edu> | 2013-05-26 13:34:24 -0700 |
commit | ed3d3dfc8ea16ac226bbce6cabbb207ee89ce474 (patch) | |
tree | bfe7b8b0490a4153bd98f67995d2481c8e95cb28 /src/opt/sfm | |
parent | 8e639c3d79224a471d14ac4a34a6a21902157eda (diff) | |
download | abc-ed3d3dfc8ea16ac226bbce6cabbb207ee89ce474.tar.gz abc-ed3d3dfc8ea16ac226bbce6cabbb207ee89ce474.tar.bz2 abc-ed3d3dfc8ea16ac226bbce6cabbb207ee89ce474.zip |
New MFS package.
Diffstat (limited to 'src/opt/sfm')
-rw-r--r-- | src/opt/sfm/sfm.h | 1 | ||||
-rw-r--r-- | src/opt/sfm/sfmCnf.c | 8 | ||||
-rw-r--r-- | src/opt/sfm/sfmCore.c | 18 | ||||
-rw-r--r-- | src/opt/sfm/sfmNtk.c | 32 | ||||
-rw-r--r-- | src/opt/sfm/sfmSat.c | 2 | ||||
-rw-r--r-- | src/opt/sfm/sfmWin.c | 67 |
6 files changed, 68 insertions, 60 deletions
diff --git a/src/opt/sfm/sfm.h b/src/opt/sfm/sfm.h index 025d0dfa..9323aa47 100644 --- a/src/opt/sfm/sfm.h +++ b/src/opt/sfm/sfm.h @@ -46,7 +46,6 @@ struct Sfm_Par_t_ int nFanoutMax; // the maximum number of fanouts int nDepthMax; // the maximum depth to try 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 nFirstFixed; // the number of first nodes to be treated as fixed int fFixLevel; // does not allow level to increase diff --git a/src/opt/sfm/sfmCnf.c b/src/opt/sfm/sfmCnf.c index f04a6970..02744cf4 100644 --- a/src/opt/sfm/sfmCnf.c +++ b/src/opt/sfm/sfmCnf.c @@ -73,6 +73,7 @@ int Sfm_TruthToCnf( word Truth, int nVars, Vec_Int_t * vCover, Vec_Str_t * vCnf Vec_StrClear( vCnf ); if ( Truth == 0 || ~Truth == 0 ) { +// assert( nVars == 0 ); Vec_StrPush( vCnf, (char)(Truth == 0) ); Vec_StrPush( vCnf, (char)-1 ); return 1; @@ -80,6 +81,7 @@ int Sfm_TruthToCnf( word Truth, int nVars, Vec_Int_t * vCover, Vec_Str_t * vCnf else { int i, k, c, RetValue, Literal, Cube, nCubes = 0; + assert( nVars > 0 ); for ( c = 0; c < 2; c ++ ) { Truth = c ? ~Truth : Truth; @@ -159,11 +161,9 @@ void Sfm_TranslateCnf( Vec_Wec_t * vRes, Vec_Str_t * vCnf, Vec_Int_t * vFaninMap { Lit = (int)Entry; if ( Lit == -1 ) - { vClause = Vec_WecPushLevel( vRes ); - continue; - } - Vec_IntPush( vClause, Abc_Lit2LitV( Vec_IntArray(vFaninMap), Lit ) ); + else + Vec_IntPush( vClause, Abc_Lit2LitV( Vec_IntArray(vFaninMap), Lit ) ); } } diff --git a/src/opt/sfm/sfmCore.c b/src/opt/sfm/sfmCore.c index 67cbaa3a..92f94562 100644 --- a/src/opt/sfm/sfmCore.c +++ b/src/opt/sfm/sfmCore.c @@ -49,7 +49,6 @@ void Sfm_ParSetDefault( Sfm_Par_t * pPars ) pPars->nFanoutMax = 30; // the maximum number of fanouts 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 @@ -82,8 +81,8 @@ void Sfm_NtkPrintStats( Sfm_Ntk_t * p ) 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( "Nodes %6d out of %6d (%6.2f %%) ", p->nTotalNodesBeg-p->nTotalNodesEnd, p->nTotalNodesBeg, 100.0*(p->nTotalNodesBeg-p->nTotalNodesEnd)/Abc_MaxInt(1, p->nTotalNodesBeg) ); + printf( "Edges %6d out of %6d (%6.2f %%) ", p->nTotalEdgesBeg-p->nTotalEdgesEnd, p->nTotalEdgesBeg, 100.0*(p->nTotalEdgesBeg-p->nTotalEdgesEnd)/Abc_MaxInt(1, p->nTotalEdgesBeg) ); printf( "\n" ); ABC_PRTP( "Win", p->timeWin , p->timeTotal ); @@ -254,14 +253,14 @@ int Sfm_NodeResub( Sfm_Ntk_t * p, int iNode ) ***********************************************************************/ int Sfm_NtkPerform( Sfm_Ntk_t * p, Sfm_Par_t * pPars ) { - int i, Counter = 0; + int i, k, Counter = 0; p->timeTotal = clock(); p->pPars = pPars; Sfm_NtkPrepare( p ); // Sfm_ComputeInterpolantCheck( p ); // return 0; - p->nTotalNodesBeg = Vec_WecSizeUsed(&p->vFanins) - Sfm_NtkPoNum(p); - p->nTotalEdgesBeg = Vec_WecSizeSize(&p->vFanins); + p->nTotalNodesBeg = Vec_WecSize(&p->vFanins) - Sfm_NtkPiNum(p) - Sfm_NtkPoNum(p); + p->nTotalEdgesBeg = Vec_WecSizeSize(&p->vFanins) - Sfm_NtkPoNum(p); Sfm_NtkForEachNode( p, i ) { if ( Sfm_ObjIsFixed( p, i ) ) @@ -270,11 +269,12 @@ int Sfm_NtkPerform( Sfm_Ntk_t * p, Sfm_Par_t * pPars ) continue; if ( Sfm_ObjFaninNum(p, i) < 2 || Sfm_ObjFaninNum(p, i) > 6 ) continue; - while ( Sfm_NodeResub(p, i) ) - Counter++; + for ( k = 0; Sfm_NodeResub(p, i); k++ ) + ; + Counter += (k > 0); } p->nTotalNodesEnd = Vec_WecSizeUsed(&p->vFanins) - Sfm_NtkPoNum(p); - p->nTotalEdgesEnd = Vec_WecSizeSize(&p->vFanins); + p->nTotalEdgesEnd = Vec_WecSizeSize(&p->vFanins) - Sfm_NtkPoNum(p); p->timeTotal = clock() - p->timeTotal; if ( pPars->fVerbose ) Sfm_NtkPrintStats( p ); diff --git a/src/opt/sfm/sfmNtk.c b/src/opt/sfm/sfmNtk.c index 3783e368..79b7bb6a 100644 --- a/src/opt/sfm/sfmNtk.c +++ b/src/opt/sfm/sfmNtk.c @@ -168,7 +168,7 @@ void Sfm_NtkPrepare( Sfm_Ntk_t * p ) p->vDivs = Vec_IntAlloc( 100 ); p->vRoots = Vec_IntAlloc( 1000 ); p->vTfo = Vec_IntAlloc( 1000 ); - p->vDivCexes = Vec_WrdStart( p->pPars->nDivNumMax ); + p->vDivCexes = Vec_WrdStart( p->pPars->nWinSizeMax ); p->vOrder = Vec_IntAlloc( 100 ); p->vDivVars = Vec_IntAlloc( 100 ); p->vDivIds = Vec_IntAlloc( 1000 ); @@ -177,6 +177,7 @@ void Sfm_NtkPrepare( Sfm_Ntk_t * p ) p->vClauses = Vec_WecAlloc( 100 ); p->vFaninMap = Vec_IntAlloc( 10 ); p->pSat = sat_solver_new(); + sat_solver_setnvars( p->pSat, p->pPars->nWinSizeMax ); } void Sfm_NtkFree( Sfm_Ntk_t * p ) { @@ -226,6 +227,8 @@ void Sfm_NtkFree( Sfm_Ntk_t * p ) void Sfm_NtkRemoveFanin( Sfm_Ntk_t * p, int iNode, int iFanin ) { int RetValue; + assert( Sfm_ObjIsNode(p, iNode) ); + assert( !Sfm_ObjIsPo(p, iFanin) ); RetValue = Vec_IntRemove( Sfm_ObjFiArray(p, iNode), iFanin ); assert( RetValue ); RetValue = Vec_IntRemove( Sfm_ObjFoArray(p, iFanin), iNode ); @@ -235,6 +238,8 @@ void Sfm_NtkAddFanin( Sfm_Ntk_t * p, int iNode, int iFanin ) { if ( iFanin < 0 ) return; + assert( Sfm_ObjIsNode(p, iNode) ); + assert( !Sfm_ObjIsPo(p, iFanin) ); assert( Vec_IntFind( Sfm_ObjFiArray(p, iNode), iFanin ) == -1 ); assert( Vec_IntFind( Sfm_ObjFoArray(p, iFanin), iNode ) == -1 ); Vec_IntPush( Sfm_ObjFiArray(p, iNode), iFanin ); @@ -268,13 +273,26 @@ void Sfm_NtkUpdateLevel_rec( Sfm_Ntk_t * p, int iNode ) void Sfm_NtkUpdate( Sfm_Ntk_t * p, int iNode, int f, int iFaninNew, word uTruth ) { int iFanin = Sfm_ObjFanin( p, iNode, f ); - assert( iFanin != iFaninNew ); - // replace old fanin by new fanin assert( Sfm_ObjIsNode(p, iNode) ); - Sfm_NtkRemoveFanin( p, iNode, iFanin ); - Sfm_NtkAddFanin( p, iNode, iFaninNew ); - // recursively remove MFFC - Sfm_NtkDeleteObj_rec( p, iFanin ); + assert( iFanin != iFaninNew ); + if ( uTruth == 0 || ~uTruth == 0 ) + { + Sfm_ObjForEachFanin( p, iNode, iFanin, f ) + { + int RetValue = Vec_IntRemove( Sfm_ObjFoArray(p, iFanin), iNode ); assert( RetValue ); + if ( Sfm_ObjFanoutNum(p, iFanin) == 0 ) + Sfm_NtkDeleteObj_rec( p, iFanin ); + } + Vec_IntClear( Sfm_ObjFiArray(p, iNode) ); + } + else + { + // replace old fanin by new fanin + Sfm_NtkRemoveFanin( p, iNode, iFanin ); + Sfm_NtkAddFanin( p, iNode, iFaninNew ); + // recursively remove MFFC + Sfm_NtkDeleteObj_rec( p, iFanin ); + } // update logic level Sfm_NtkUpdateLevel_rec( p, iNode ); // update truth table diff --git a/src/opt/sfm/sfmSat.c b/src/opt/sfm/sfmSat.c index bf6a06b0..01b9d4cf 100644 --- a/src/opt/sfm/sfmSat.c +++ b/src/opt/sfm/sfmSat.c @@ -59,7 +59,7 @@ void Sfm_NtkWindowToSolver( Sfm_Ntk_t * p ) // if ( p->pSat ) // printf( "%d ", p->pSat->stats.learnts ); sat_solver_restart( p->pSat ); - sat_solver_setnvars( p->pSat, 1 + Vec_IntSize(p->vDivs) + 2 * Vec_IntSize(p->vTfo) + Vec_IntSize(p->vRoots) + 100 ); + sat_solver_setnvars( p->pSat, 1 + Vec_IntSize(p->vDivs) + 2 * Vec_IntSize(p->vTfo) + Vec_IntSize(p->vRoots) + 50 ); // create SAT variables Sfm_NtkCleanVars( p ); p->nSatVars = 1; diff --git a/src/opt/sfm/sfmWin.c b/src/opt/sfm/sfmWin.c index 1d2919f9..8ddd7865 100644 --- a/src/opt/sfm/sfmWin.c +++ b/src/opt/sfm/sfmWin.c @@ -192,7 +192,7 @@ void Sfm_NtkAddDivisors( Sfm_Ntk_t * p, int iNode, int nLevelMax ) if ( p->pPars->nFanoutMax && i > p->pPars->nFanoutMax ) break; // skip TFI nodes, PO nodes, or nodes with high logic level - if ( Sfm_ObjIsTravIdCurrent(p, iFanout) || Sfm_ObjIsPo(p, iFanout) || + if ( Sfm_ObjIsTravIdCurrent(p, iFanout) || Sfm_ObjIsPo(p, iFanout) || Sfm_ObjIsFixed(p, iFanout) || (p->pPars->fFixLevel && Sfm_ObjLevel(p, iFanout) >= nLevelMax) ) continue; // handle single-input nodes @@ -241,7 +241,7 @@ int Sfm_NtkCollectTfi_rec( Sfm_Ntk_t * p, int iNode, int nWinSizeMax ) } int Sfm_NtkCreateWindow( Sfm_Ntk_t * p, int iNode, int fVerbose ) { - int i, iTemp; + int i, k, iTemp, nDivStart; clock_t clk = clock(); assert( Sfm_ObjIsNode( p, iNode ) ); Vec_IntClear( p->vLeaves ); // leaves @@ -272,56 +272,47 @@ int Sfm_NtkCreateWindow( Sfm_Ntk_t * p, int iNode, int fVerbose ) Vec_IntPush( p->vRoots, iNode ); p->timeWin += clock() - clk; clk = clock(); + // create divisors + Vec_IntClear( p->vDivs ); + Vec_IntForEachEntry( p->vLeaves, iTemp, i ) + Vec_IntPush( p->vDivs, iTemp ); + Vec_IntForEachEntry( p->vNodes, iTemp, i ) + Vec_IntPush( p->vDivs, iTemp ); + Vec_IntPop( p->vDivs ); + // add non-topological divisors + nDivStart = Vec_IntSize(p->vDivs); + if ( Vec_IntSize(p->vDivs) < p->pPars->nWinSizeMax ) + { + Sfm_NtkIncrementTravId2( p ); + Vec_IntForEachEntry( p->vDivs, iTemp, i ) + if ( Vec_IntSize(p->vDivs) < p->pPars->nWinSizeMax ) + Sfm_NtkAddDivisors( p, iTemp, Sfm_ObjLevel(p, iNode) ); + } + if ( Vec_IntSize(p->vDivs) > p->pPars->nWinSizeMax ) + Vec_IntShrink( p->vDivs, p->pPars->nWinSizeMax ); + assert( Vec_IntSize(p->vDivs) <= p->pPars->nWinSizeMax ); + p->nMaxDivs += (Vec_IntSize(p->vDivs) == p->pPars->nWinSizeMax); // create ordering of the nodes Vec_IntClear( p->vOrder ); Vec_IntForEachEntryReverse( p->vNodes, iTemp, i ) Vec_IntPush( p->vOrder, iTemp ); Vec_IntForEachEntry( p->vLeaves, iTemp, i ) Vec_IntPush( p->vOrder, iTemp ); + Vec_IntForEachEntryStart( p->vDivs, iTemp, i, nDivStart ) + Vec_IntPush( p->vOrder, iTemp ); + // remove fanins from divisors // mark fanins Sfm_NtkIncrementTravId2( p ); 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 ) + k = 0; + Vec_IntForEachEntry( p->vDivs, 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 ); - } -//Vec_IntPrint( p->vLeaves ); -//Vec_IntPrint( p->vNodes ); -//Vec_IntPrint( p->vDivs ); - // collect additional divisors of the TFI nodes - if ( Vec_IntSize(p->vDivs) < p->pPars->nDivNumMax ) - { - int nStartNew = Vec_IntSize(p->vDivs); - Sfm_NtkIncrementTravId2( p ); - Sfm_ObjForEachFanin( p, iNode, iTemp, i ) - if ( Vec_IntSize(p->vDivs) < p->pPars->nDivNumMax ) - Sfm_NtkAddDivisors( p, iTemp, Sfm_ObjLevel(p, iNode) ); - 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 ); - p->nMaxDivs += (Vec_IntSize(p->vDivs) == p->pPars->nDivNumMax); + Vec_IntShrink( p->vDivs, k ); + assert( Vec_IntSize(p->vDivs) <= p->pPars->nWinSizeMax ); // statistics p->nTotalDivs += Vec_IntSize(p->vDivs); p->timeDiv += clock() - clk; |