From ba309121d7f1dbc9071a552d459bcaa6be7da31b Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Fri, 31 May 2013 00:56:10 -0700 Subject: New MFS package. --- src/opt/mfs/mfs.h | 1 - src/opt/sfm/sfm.h | 1 + src/opt/sfm/sfmCore.c | 1 + src/opt/sfm/sfmInt.h | 8 ++++++- src/opt/sfm/sfmNtk.c | 62 +++++++++++++++++++++++++++++++++++++++++++-------- src/opt/sfm/sfmWin.c | 5 +++-- 6 files changed, 65 insertions(+), 13 deletions(-) (limited to 'src/opt') diff --git a/src/opt/mfs/mfs.h b/src/opt/mfs/mfs.h index 4ca0df00..cf7e2f6e 100644 --- a/src/opt/mfs/mfs.h +++ b/src/opt/mfs/mfs.h @@ -46,7 +46,6 @@ struct Mfs_Par_t_ int nWinTfoLevs; // the maximum fanout levels int nFanoutsMax; // the maximum number of fanouts int nDepthMax; // the maximum number of logic levels - int nDivMax; // the maximum number of divisors 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 diff --git a/src/opt/sfm/sfm.h b/src/opt/sfm/sfm.h index 18960183..ef04da02 100644 --- a/src/opt/sfm/sfm.h +++ b/src/opt/sfm/sfm.h @@ -46,6 +46,7 @@ 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 nGrowthLevel; // the maximum allowed growth in level 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/sfmCore.c b/src/opt/sfm/sfmCore.c index af2cb836..9efb70e2 100644 --- a/src/opt/sfm/sfmCore.c +++ b/src/opt/sfm/sfmCore.c @@ -49,6 +49,7 @@ 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->nGrowthLevel = 0; // the maximum allowed growth in level pPars->nBTLimit = 5000; // the maximum number of conflicts in one SAT run pPars->fFixLevel = 1; // does not allow level to increase pPars->fRrOnly = 0; // perform redundancy removal diff --git a/src/opt/sfm/sfmInt.h b/src/opt/sfm/sfmInt.h index 60648b44..c9ccbc89 100644 --- a/src/opt/sfm/sfmInt.h +++ b/src/opt/sfm/sfmInt.h @@ -58,6 +58,7 @@ struct Sfm_Ntk_t_ int nPos; // PO count (POs should be last objects) int nNodes; // internal nodes int nObjs; // total objects + int nLevelMax; // maximum level // user data Vec_Str_t * vFixed; // persistent objects Vec_Wrd_t * vTruths; // truth tables @@ -65,6 +66,7 @@ struct Sfm_Ntk_t_ // attributes Vec_Wec_t vFanouts; // fanouts Vec_Int_t vLevels; // logic level + Vec_Int_t vLevelsR; // logic level Vec_Int_t vCounts; // fanin counters Vec_Int_t vId2Var; // ObjId -> SatVar Vec_Int_t vVar2Id; // SatVar -> ObjId @@ -148,6 +150,9 @@ static inline void Sfm_NtkCleanVars( Sfm_Ntk_t * p ) { int i; static inline int Sfm_ObjLevel( Sfm_Ntk_t * p, int iObj ) { return Vec_IntEntry( &p->vLevels, iObj ); } static inline void Sfm_ObjSetLevel( Sfm_Ntk_t * p, int iObj, int Lev ) { Vec_IntWriteEntry( &p->vLevels, iObj, Lev ); } +static inline int Sfm_ObjLevelR( Sfm_Ntk_t * p, int iObj ) { return Vec_IntEntry( &p->vLevelsR, iObj ); } +static inline void Sfm_ObjSetLevelR( Sfm_Ntk_t * p, int iObj, int Lev ) { Vec_IntWriteEntry( &p->vLevelsR, iObj, Lev ); } + 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); } @@ -157,7 +162,8 @@ extern void Kit_DsdPrintFromTruth( unsigned * pTruth, int nVars ); /// MACRO DEFINITIONS /// //////////////////////////////////////////////////////////////////////// -#define Sfm_NtkForEachNode( p, i ) for ( i = p->nPis; i + p->nPos < p->nObjs; i++ ) +#define Sfm_NtkForEachNode( p, i ) for ( i = p->nPis; i + p->nPos < p->nObjs; i++ ) +#define Sfm_NtkForEachNodeReverse( p, i ) for ( i = p->nObjs - p->nPos - 1; i >= p->nPis; i-- ) #define Sfm_ObjForEachFanin( p, Node, Fan, i ) for ( i = 0; i < Sfm_ObjFaninNum(p, Node) && ((Fan = Sfm_ObjFanin(p, Node, i)), 1); i++ ) #define Sfm_ObjForEachFanout( p, Node, Fan, i ) for ( i = 0; i < Sfm_ObjFanoutNum(p, Node) && ((Fan = Sfm_ObjFanout(p, Node, i)), 1); i++ ) diff --git a/src/opt/sfm/sfmNtk.c b/src/opt/sfm/sfmNtk.c index e66e6e8e..1e650454 100644 --- a/src/opt/sfm/sfmNtk.c +++ b/src/opt/sfm/sfmNtk.c @@ -107,21 +107,49 @@ void Sfm_CreateFanout( Vec_Wec_t * vFanins, Vec_Wec_t * vFanouts ) SeeAlso [] ***********************************************************************/ -static inline int Sfm_ObjCreateLevel( Vec_Int_t * vArray, Vec_Int_t * vLevels ) +static inline int Sfm_ObjLevelNew( Vec_Int_t * vArray, Vec_Int_t * vLevels ) { int k, Fanin, Level = 0; Vec_IntForEachEntry( vArray, Fanin, k ) - Level = Abc_MaxInt( Level, Vec_IntEntry(vLevels, Fanin) + 1 ); - return Level; + Level = Abc_MaxInt( Level, Vec_IntEntry(vLevels, Fanin) ); + return Level + 1; } void Sfm_CreateLevel( Vec_Wec_t * vFanins, Vec_Int_t * vLevels ) { Vec_Int_t * vArray; int i; assert( Vec_IntSize(vLevels) == 0 ); - Vec_IntGrow( vLevels, Vec_WecSize(vFanins) ); + Vec_IntFill( vLevels, Vec_WecSize(vFanins), 0 ); Vec_WecForEachLevel( vFanins, vArray, i ) - Vec_IntPush( vLevels, Sfm_ObjCreateLevel(vArray, vLevels) ); + Vec_IntWriteEntry( vLevels, i, Sfm_ObjLevelNew(vArray, vLevels) ); +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +static inline int Sfm_ObjLevelNewR( Vec_Int_t * vArray, Vec_Int_t * vLevelsR ) +{ + int k, Fanout, LevelR = 0; + Vec_IntForEachEntry( vArray, Fanout, k ) + LevelR = Abc_MaxInt( LevelR, Vec_IntEntry(vLevelsR, Fanout) ); + return LevelR + 1; +} +void Sfm_CreateLevelR( Vec_Wec_t * vFanouts, Vec_Int_t * vLevelsR ) +{ + Vec_Int_t * vArray; + int i; + assert( Vec_IntSize(vLevelsR) == 0 ); + Vec_IntFill( vLevelsR, Vec_WecSize(vFanouts), 0 ); + Vec_WecForEachLevelReverse( vFanouts, vArray, i ) + Vec_IntWriteEntry( vLevelsR, i, Sfm_ObjLevelNewR(vArray, vLevelsR) ); } /**Function************************************************************* @@ -152,6 +180,7 @@ Sfm_Ntk_t * Sfm_NtkConstruct( Vec_Wec_t * vFanins, int nPis, int nPos, Vec_Str_t // attributes Sfm_CreateFanout( &p->vFanins, &p->vFanouts ); Sfm_CreateLevel( &p->vFanins, &p->vLevels ); + Sfm_CreateLevelR( &p->vFanouts, &p->vLevelsR ); Vec_IntFill( &p->vCounts, p->nObjs, 0 ); Vec_IntFill( &p->vTravIds, p->nObjs, 0 ); Vec_IntFill( &p->vTravIds2, p->nObjs, 0 ); @@ -163,6 +192,7 @@ Sfm_Ntk_t * Sfm_NtkConstruct( Vec_Wec_t * vFanins, int nPis, int nPos, Vec_Str_t } void Sfm_NtkPrepare( Sfm_Ntk_t * p ) { + p->nLevelMax = Vec_IntFindMax(&p->vLevels) + p->pPars->nGrowthLevel; p->vNodes = Vec_IntAlloc( 1000 ); p->vDivs = Vec_IntAlloc( 100 ); p->vRoots = Vec_IntAlloc( 1000 ); @@ -187,6 +217,7 @@ void Sfm_NtkFree( Sfm_Ntk_t * p ) // attributes Vec_WecErase( &p->vFanouts ); ABC_FREE( p->vLevels.pArray ); + ABC_FREE( p->vLevelsR.pArray ); ABC_FREE( p->vCounts.pArray ); ABC_FREE( p->vTravIds.pArray ); ABC_FREE( p->vTravIds2.pArray ); @@ -260,13 +291,22 @@ void Sfm_NtkDeleteObj_rec( Sfm_Ntk_t * p, int iNode ) void Sfm_NtkUpdateLevel_rec( Sfm_Ntk_t * p, int iNode ) { int i, iFanout; - int LevelNew = Sfm_ObjCreateLevel( Sfm_ObjFiArray(p, iNode), &p->vLevels ); + int LevelNew = Sfm_ObjLevelNew( Sfm_ObjFiArray(p, iNode), &p->vLevels ); if ( LevelNew == Sfm_ObjLevel(p, iNode) ) return; Sfm_ObjSetLevel( p, iNode, LevelNew ); - if ( Sfm_ObjIsNode(p, iNode) ) - Sfm_ObjForEachFanout( p, iNode, iFanout, i ) - Sfm_NtkUpdateLevel_rec( p, iFanout ); + Sfm_ObjForEachFanout( p, iNode, iFanout, i ) + Sfm_NtkUpdateLevel_rec( p, iFanout ); +} +void Sfm_NtkUpdateLevelR_rec( Sfm_Ntk_t * p, int iNode ) +{ + int i, iFanin; + int LevelNew = Sfm_ObjLevelNewR( Sfm_ObjFoArray(p, iNode), &p->vLevelsR ); + if ( LevelNew == Sfm_ObjLevelR(p, iNode) ) + return; + Sfm_ObjSetLevelR( p, iNode, LevelNew ); + Sfm_ObjForEachFanin( p, iNode, iFanin, i ) + Sfm_NtkUpdateLevelR_rec( p, iFanin ); } void Sfm_NtkUpdate( Sfm_Ntk_t * p, int iNode, int f, int iFaninNew, word uTruth ) { @@ -292,6 +332,10 @@ void Sfm_NtkUpdate( Sfm_Ntk_t * p, int iNode, int f, int iFaninNew, word uTruth } // update logic level Sfm_NtkUpdateLevel_rec( p, iNode ); + if ( iFaninNew != -1 ) + Sfm_NtkUpdateLevelR_rec( p, iFaninNew ); + if ( Sfm_ObjFanoutNum(p, iFanin) > 0 ) + Sfm_NtkUpdateLevelR_rec( p, iFanin ); // update truth table Vec_WrdWriteEntry( p->vTruths, iNode, uTruth ); Sfm_TruthToCnf( uTruth, Sfm_ObjFaninNum(p, iNode), p->vCover, (Vec_Str_t *)Vec_WecEntry(p->vCnfs, iNode) ); diff --git a/src/opt/sfm/sfmWin.c b/src/opt/sfm/sfmWin.c index db6bd0ea..f12474c9 100644 --- a/src/opt/sfm/sfmWin.c +++ b/src/opt/sfm/sfmWin.c @@ -215,7 +215,7 @@ void Sfm_NtkAddDivisors( Sfm_Ntk_t * p, int iNode, int nLevelMax ) return; // skip TFI nodes, PO nodes, or nodes with high logic level if ( Sfm_ObjIsTravIdCurrent(p, iFanout) || Sfm_ObjIsPo(p, iFanout) || - (p->pPars->fFixLevel && Sfm_ObjLevel(p, iFanout) >= nLevelMax) ) + (p->pPars->fFixLevel && Sfm_ObjLevel(p, iFanout) > nLevelMax) ) continue; // handle single-input nodes if ( Sfm_ObjFaninNum(p, iFanout) == 1 ) @@ -311,7 +311,8 @@ int Sfm_NtkCreateWindow( Sfm_Ntk_t * p, int iNode, int fVerbose ) Sfm_NtkIncrementTravId2( p ); Vec_IntForEachEntry( p->vDivs, iTemp, i ) if ( Vec_IntSize(p->vDivs) < p->pPars->nWinSizeMax + 0 ) - Sfm_NtkAddDivisors( p, iTemp, Sfm_ObjLevel(p, iNode) ); +// Sfm_NtkAddDivisors( p, iTemp, Sfm_ObjLevel(p, iNode) - 1 ); + Sfm_NtkAddDivisors( p, iTemp, p->nLevelMax - Sfm_ObjLevelR(p, iNode) ); } if ( Vec_IntSize(p->vDivs) > p->pPars->nWinSizeMax ) { -- cgit v1.2.3