Skip to content

A
abc
Commit ba309121 by Alan Mishchenko
Options

New MFS package.

parent 338845a2
Showing with 76 additions and 12 deletions
src/base/abci/abc.c
......@@ -4491,7 +4491,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, "WFDMCZdlaevwh" ) ) != EOF )
while ( ( c = Extra_UtilGetopt( argc, argv, "WFDMLCZdlaevwh" ) ) != EOF )
{
switch ( c )
{
......@@ -4539,6 +4539,17 @@ int Abc_CommandMfs2( Abc_Frame_t * pAbc, int argc, char ** argv )
if ( pPars->nWinSizeMax < 0 )
goto usage;
break;
case 'L':
if ( globalUtilOptind >= argc )
{
Abc_Print( -1, "Command line switch \"-L\" should be followed by an integer.\n" );
goto usage;
}
pPars->nGrowthLevel = atoi(argv[globalUtilOptind]);
globalUtilOptind++;
if ( pPars->nGrowthLevel < 0 || pPars->nGrowthLevel > ABC_INFINITY )
goto usage;
break;
case 'C':
if ( globalUtilOptind >= argc )
{
......@@ -4604,12 +4615,13 @@ int Abc_CommandMfs2( Abc_Frame_t * pAbc, int argc, char ** argv )
return 0;
usage:
Abc_Print( -2, "usage: mfs2 [-WFDMCZ <num>] [-dlaevwh]\n" );
Abc_Print( -2, "usage: mfs2 [-WFDMLCZ <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 );
Abc_Print( -2, "\t-D <num> : the max depth nodes to try (0 = no limit) [default = %d]\n", pPars->nDepthMax );
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-Z <num> : treat the first <num> logic nodes as fixed (0 = none) [default = %d]\n", pPars->nFirstFixed );
Abc_Print( -2, "\t-d : toggle performing redundancy removal [default = %s]\n", pPars->fRrOnly? "yes": "no" );
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
......
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
......
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
......
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); }
......@@ -158,6 +163,7 @@ extern void Kit_DsdPrintFromTruth( unsigned * pTruth, int nVars );
////////////////////////////////////////////////////////////////////////
#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++ )
......
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,14 +291,23 @@ 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 );
}
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 )
{
int iFanin = Sfm_ObjFanin( p, iNode, f );
......@@ -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) );
......
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 )
{
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment