Skip to content

A
abc
Commit 90a88462 by Alan Mishchenko
Options

New MFS package.

parent ba309121
Showing with 21 additions and 20 deletions
src/base/abci/abc.c
......@@ -4318,7 +4318,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, "WFDMLCdlraestpgvwh" ) ) != EOF )
while ( ( c = Extra_UtilGetopt( argc, argv, "WFDMLCdraestpgvwh" ) ) != EOF )
{
switch ( c )
{
......@@ -4391,9 +4391,6 @@ int Abc_CommandMfs( Abc_Frame_t * pAbc, int argc, char ** argv )
case 'd':
pPars->fRrOnly ^= 1;
break;
case 'l':
pPars->nGrowthLevel = 10000;
break;
case 'r':
pPars->fResub ^= 1;
break;
......@@ -4448,7 +4445,7 @@ int Abc_CommandMfs( Abc_Frame_t * pAbc, int argc, char ** argv )
return 0;
usage:
Abc_Print( -2, "usage: mfs [-WFDMLC <num>] [-dlraestpgvh]\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 );
......@@ -4457,7 +4454,6 @@ usage:
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-l : allow logic level to increase [default = %s]\n", (pPars->nGrowthLevel > 0)? "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" );
......@@ -4491,7 +4487,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, "WFDMLCZdlaevwh" ) ) != EOF )
while ( ( c = Extra_UtilGetopt( argc, argv, "WFDMLCZdaevwh" ) ) != EOF )
{
switch ( c )
{
......@@ -4575,9 +4571,6 @@ int Abc_CommandMfs2( Abc_Frame_t * pAbc, int argc, char ** argv )
case 'd':
pPars->fRrOnly ^= 1;
break;
case 'l':
pPars->fFixLevel ^= 1;
break;
case 'a':
pPars->fArea ^= 1;
break;
......@@ -4615,7 +4608,7 @@ int Abc_CommandMfs2( Abc_Frame_t * pAbc, int argc, char ** argv )
return 0;
usage:
Abc_Print( -2, "usage: mfs2 [-WFDMLCZ <num>] [-dlaevwh]\n" );
Abc_Print( -2, "usage: mfs2 [-WFDMLCZ <num>] [-daevwh]\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 );
......@@ -4625,7 +4618,6 @@ usage:
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" );
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" );
Abc_Print( -2, "\t-v : toggle printing optimization summary [default = %s]\n", pPars->fVerbose? "yes": "no" );
src/opt/sfm/sfm.h
......@@ -49,7 +49,6 @@ struct Sfm_Par_t_
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
int fRrOnly; // perform redundance removal
int fArea; // performs optimization for area
int fMoreEffort; // performs high-affort minimization
......
src/opt/sfm/sfmCore.c
......@@ -51,7 +51,6 @@ void Sfm_ParSetDefault( Sfm_Par_t * pPars )
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
pPars->fArea = 0; // performs optimization for area
pPars->fMoreEffort = 0; // performs high-affort minimization
......@@ -213,7 +212,8 @@ int Sfm_NodeResub( Sfm_Ntk_t * p, int iNode )
// prepare SAT solver
if ( !Sfm_NtkCreateWindow( p, iNode, p->pPars->fVeryVerbose ) )
return 0;
Sfm_NtkWindowToSolver( p );
if ( !Sfm_NtkWindowToSolver( p ) )
return 0;
// try replacing area critical fanins
Sfm_ObjForEachFanin( p, iNode, iFanin, i )
if ( Sfm_ObjIsNode(p, iFanin) && Sfm_ObjFanoutNum(p, iFanin) == 1 )
......
src/opt/sfm/sfmInt.h
......@@ -182,7 +182,7 @@ extern Sfm_Ntk_t * Sfm_ConstructNetwork( Vec_Wec_t * vFanins, int nPis, int nPo
extern void Sfm_NtkPrepare( Sfm_Ntk_t * p );
extern void Sfm_NtkUpdate( Sfm_Ntk_t * p, int iNode, int f, int iFaninNew, word uTruth );
/*=== sfmSat.c ==========================================================*/
extern void Sfm_NtkWindowToSolver( Sfm_Ntk_t * p );
extern int Sfm_NtkWindowToSolver( Sfm_Ntk_t * p );
extern word Sfm_ComputeInterpolant( Sfm_Ntk_t * p );
/*=== sfmWin.c ==========================================================*/
extern int Sfm_ObjMffcSize( Sfm_Ntk_t * p, int iObj );
......
src/opt/sfm/sfmSat.c
......@@ -51,7 +51,7 @@ static word s_Truths6[6] = {
SeeAlso []
***********************************************************************/
void Sfm_NtkWindowToSolver( Sfm_Ntk_t * p )
int Sfm_NtkWindowToSolver( Sfm_Ntk_t * p )
{
// p->vOrder contains all variables in the window in a good order
// p->vDivs is a subset of nodes in p->vOrder used as divisor candidates
......@@ -137,12 +137,14 @@ void Sfm_NtkWindowToSolver( Sfm_Ntk_t * p )
}
// make OR clause for the last nRoots variables
RetValue = sat_solver_addclause( p->pSat, Vec_IntArray(p->vLits), Vec_IntArray(p->vLits) + Vec_IntSize(p->vLits) );
assert( RetValue );
if ( RetValue == 0 )
return 0;
}
// finalize
RetValue = sat_solver_simplify( p->pSat );
assert( RetValue );
p->timeCnf += Abc_Clock() - clk;
return 1;
}
/**Function*************************************************************
......
src/opt/sfm/sfmWin.c
......@@ -214,8 +214,7 @@ void Sfm_NtkAddDivisors( Sfm_Ntk_t * p, int iNode, int nLevelMax )
if ( p->pPars->nFanoutMax && i > p->pPars->nFanoutMax )
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) )
if ( Sfm_ObjIsTravIdCurrent(p, iFanout) || Sfm_ObjIsPo(p, iFanout) || Sfm_ObjLevel(p, iFanout) > nLevelMax )
continue;
// handle single-input nodes
if ( Sfm_ObjFaninNum(p, iFanout) == 1 )
......@@ -362,6 +361,15 @@ int Sfm_NtkCreateWindow( Sfm_Ntk_t * p, int iNode, int fVerbose )
break;
}
if ( Vec_IntSize(p->vRoots) > 0 )
Vec_IntForEachEntry( p->vTfo, iTemp, i )
if ( Sfm_NtkCollectTfi_rec( p, iTemp, p->vOrder ) )
{
Vec_IntClear( p->vRoots );
Vec_IntClear( p->vTfo );
Vec_IntClear( p->vOrder );
break;
}
if ( Vec_IntSize(p->vRoots) > 0 )
Vec_IntForEachEntry( p->vDivs, iTemp, i )
if ( Sfm_NtkCollectTfi_rec( p, iTemp, p->vOrder ) )
{
......
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