luke
/
abc
mirror of https://github.com/YosysHQ/abc.git
1
0
Fork 0
Code Issues Packages Projects Releases Wiki Activity

Experiments with don't-cares.

This commit is contained in:
Alan Mishchenko 2017-04-02 21:51:47 -07:00
parent 3898ba5486
commit f765e666ca
10 changed files with 611 additions and 340 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

38
src/base/abci/abc.c
View File

@ -5676,30 +5676,19 @@ int Abc_CommandMfse( Abc_Frame_t * pAbc, int argc, char ** argv )
Acb_Par_t Pars, * pPars = &Pars; int c;
Acb_ParSetDefault( pPars );
Extra_UtilGetoptReset();
while ( ( c = Extra_UtilGetopt( argc, argv, "MDOFLCavwh" ) ) != EOF )
while ( ( c = Extra_UtilGetopt( argc, argv, "IOWFLCavwh" ) ) != EOF )
{
switch ( c )
{
case 'M':
case 'I':
if ( globalUtilOptind >= argc )
{
Abc_Print( -1, "Command line switch \"-M\" should be followed by an integer.\n" );
Abc_Print( -1, "Command line switch \"-I\" should be followed by an integer.\n" );
goto usage;
}
pPars->nTabooMax = atoi(argv[globalUtilOptind]);
pPars->nTfiLevMax = atoi(argv[globalUtilOptind]);
globalUtilOptind++;
if ( pPars->nTabooMax < 0 )
goto usage;
break;
case 'D':
if ( globalUtilOptind >= argc )
{
Abc_Print( -1, "Command line switch \"-D\" should be followed by an integer.\n" );
goto usage;
}
pPars->nDivMax = atoi(argv[globalUtilOptind]);
globalUtilOptind++;
if ( pPars->nDivMax < 0 )
if ( pPars->nTfiLevMax < 0 )
goto usage;
break;
case 'O':
@ -5713,6 +5702,17 @@ int Abc_CommandMfse( Abc_Frame_t * pAbc, int argc, char ** argv )
if ( pPars->nTfoLevMax < 0 )
goto usage;
break;
case 'W':
if ( globalUtilOptind >= argc )
{
Abc_Print( -1, "Command line switch \"-W\" should be followed by an integer.\n" );
goto usage;
}
pPars->nWinNodeMax = atoi(argv[globalUtilOptind]);
globalUtilOptind++;
if ( pPars->nWinNodeMax < 0 )
goto usage;
break;
case 'F':
if ( globalUtilOptind >= argc )
{
@ -5788,11 +5788,11 @@ int Abc_CommandMfse( Abc_Frame_t * pAbc, int argc, char ** argv )
return 0;
usage:
Abc_Print( -2, "usage: mfse [-MDOFLC <num>] [-avwh]\n" );
Abc_Print( -2, "usage: mfse [-IOWFLC <num>] [-avwh]\n" );
Abc_Print( -2, "\t performs don't-care-based optimization of logic networks\n" );
Abc_Print( -2, "\t-M <num> : the max number of fanin nodes to skip (num >= 1) [default = %d]\n", pPars->nTabooMax );
Abc_Print( -2, "\t-D <num> : the max number of divisors [default = %d]\n", pPars->nDivMax );
Abc_Print( -2, "\t-I <num> : the number of levels in the TFI cone (2 <= num) [default = %d]\n", pPars->nTfiLevMax );
Abc_Print( -2, "\t-O <num> : the number of levels in the TFO cone (0 <= num) [default = %d]\n", pPars->nTfoLevMax );
Abc_Print( -2, "\t-W <num> : the max number of nodes in the window (1 <= num) [default = %d]\n", pPars->nWinNodeMax );
Abc_Print( -2, "\t-F <num> : the max number of fanouts to skip (1 <= num) [default = %d]\n", pPars->nFanoutMax );
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 );

5
src/base/acb/acb.h
View File

@ -503,7 +503,10 @@ static inline void Acb_ObjRemoveFaninFanout( Acb_Ntk_t * p, int iObj )
{
int k, iFanin, * pFanins;
Acb_ObjForEachFaninFast( p, iObj, pFanins, iFanin, k )
Vec_IntRemove( Vec_WecEntry(&p->vFanouts, iFanin), iObj );
{
int RetValue = Vec_IntRemove( Vec_WecEntry(&p->vFanouts, iFanin), iObj );
assert( RetValue );
}
}
static inline void Acb_NtkCreateFanout( Acb_Ntk_t * p )
{

5
src/base/acb/acbAbc.c
View File

@ -210,10 +210,9 @@ void Acb_ParSetDefault( Acb_Par_t * pPars )
memset( pPars, 0, sizeof(Acb_Par_t) );
pPars->nLutSize = 4; // LUT size
pPars->nTfoLevMax = 2; // the maximum fanout levels
pPars->nTfiLevMax = 2; // the maximum fanin levels
pPars->nTfiLevMax = 3; // the maximum fanin levels
pPars->nFanoutMax = 20; // the maximum number of fanouts
pPars->nDivMax = 24; // the maximum divisor count
pPars->nTabooMax = 1; // the minimum MFFC size
pPars->nWinNodeMax = 100; // the maximum number of nodes in the window
pPars->nGrowthLevel = 0; // the maximum allowed growth in level
pPars->nBTLimit = 0; // the maximum number of conflicts in one SAT run
pPars->nNodesMax = 0; // the maximum number of nodes to try

852
src/base/acb/acbMfs.c
View File

File diff suppressed because it is too large Load Diff

3
src/base/acb/acbPar.h
View File

@ -42,8 +42,7 @@ struct Acb_Par_t_
int nTfoLevMax; // the maximum fanout levels
int nTfiLevMax; // the maximum fanin levels
int nFanoutMax; // the maximum number of fanouts
int nDivMax; // the maximum divisor count
int nTabooMax; // the minimum MFFC size
int nWinNodeMax; // the maximum number of nodes in the window
int nGrowthLevel; // the maximum allowed growth in level
int nBTLimit; // the maximum number of conflicts in one SAT run
int nNodesMax; // the maximum number of nodes to try

30
src/base/acb/acbUtil.c
View File

@ -308,14 +308,38 @@ void Acb_NtkCreateNode( Acb_Ntk_t * p, word uTruth, Vec_Int_t * vSupp )
Acb_ObjAddFaninFanout( p, Pivot );
Acb_ObjComputeLevelD( p, Pivot );
}
void Acb_NtkUpdateNode( Acb_Ntk_t * p, int Pivot, word uTruth, Vec_Int_t * vSupp )
void Acb_NtkResetNode( Acb_Ntk_t * p, int Pivot, word uTruth, Vec_Int_t * vSupp )
{
// remember old fanins
int k, iFanin, * pFanins;
Vec_Int_t * vFanins = Vec_IntAlloc( 6 );
assert( !Acb_ObjIsCio(p, Pivot) );
Acb_ObjForEachFaninFast( p, Pivot, pFanins, iFanin, k )
Vec_IntPush( vFanins, iFanin );
// update function
Vec_WrdSetEntry( &p->vObjTruth, Pivot, uTruth );
Vec_IntErase( Vec_WecEntry(&p->vCnfs, Pivot) );
// remove old fanins
Acb_ObjRemoveFaninFanout( p, Pivot );
Acb_ObjRemoveFanins( p, Pivot );
Acb_ObjAddFanins( p, Pivot, vSupp );
Acb_ObjAddFaninFanout( p, Pivot );
// add new fanins
if ( vSupp != NULL )
{
assert( Acb_ObjFanoutNum(p, Pivot) > 0 );
Acb_ObjAddFanins( p, Pivot, vSupp );
Acb_ObjAddFaninFanout( p, Pivot );
}
else if ( Acb_ObjFanoutNum(p, Pivot) == 0 )
Acb_ObjCleanType( p, Pivot );
// delete dangling fanins
Vec_IntForEachEntry( vFanins, iFanin, k )
if ( !Acb_ObjIsCio(p, iFanin) && Acb_ObjFanoutNum(p, iFanin) == 0 )
Acb_NtkResetNode( p, iFanin, 0, NULL );
Vec_IntFree( vFanins );
}
void Acb_NtkUpdateNode( Acb_Ntk_t * p, int Pivot, word uTruth, Vec_Int_t * vSupp )
{
Acb_NtkResetNode( p, Pivot, uTruth, vSupp );
if ( p->vQue == NULL )
Acb_NtkUpdateLevelD( p, Pivot );
else

4
src/opt/sfm/sfmCore.c
View File

@ -73,8 +73,8 @@ void Sfm_ParSetDefault( Sfm_Par_t * pPars )
void Sfm_NtkPrintStats( Sfm_Ntk_t * p )
{
p->timeOther = p->timeTotal - p->timeWin - p->timeDiv - p->timeCnf - p->timeSat;
printf( "Nodes = %d. Try = %d. Resub = %d. Div = %d. SAT calls = %d. Timeouts = %d. MaxDivs = %d.\n",
Sfm_NtkNodeNum(p), p->nNodesTried, p->nRemoves + p->nResubs, p->nTotalDivs, p->nSatCalls, p->nTimeOuts, p->nMaxDivs );
printf( "Nodes = %d. Try = %d. Resub = %d. Div = %d (ave = %d). SAT calls = %d. Timeouts = %d. MaxDivs = %d.\n",
Sfm_NtkNodeNum(p), p->nNodesTried, p->nRemoves + p->nResubs, p->nTotalDivs, p->nTotalDivs/Abc_MaxInt(1, p->nNodesTried), p->nSatCalls, p->nTimeOuts, p->nMaxDivs );
printf( "Attempts : " );
printf( "Remove %6d out of %6d (%6.2f %%) ", p->nRemoves, p->nTryRemoves, 100.0*p->nRemoves/Abc_MaxInt(1, p->nTryRemoves) );

4
src/sat/bsat/satUtil.c
View File

@ -85,7 +85,7 @@ void Sat_SolverWriteDimacs( sat_solver * p, char * pFileName, lit* assumpBegin,
nUnits++;
// start the file
pFile = fopen( pFileName, "wb" );
pFile = pFileName ? fopen( pFileName, "wb" ) : stdout;
if ( pFile == NULL )
{
printf( "Sat_SolverWriteDimacs(): Cannot open the ouput file.\n" );
@ -121,7 +121,7 @@ void Sat_SolverWriteDimacs( sat_solver * p, char * pFileName, lit* assumpBegin,
}
fprintf( pFile, "\n" );
fclose( pFile );
if ( pFileName ) fclose( pFile );
}
void Sat_Solver2WriteDimacs( sat_solver2 * p, char * pFileName, lit* assumpBegin, lit* assumpEnd, int incrementVars )
{

2
src/sat/cnf/cnf.h
View File

@ -156,7 +156,7 @@ extern Cnf_Dat_t * Cnf_DataAlloc( Aig_Man_t * pAig, int nVars, int nClauses,
extern Cnf_Dat_t * Cnf_DataDup( Cnf_Dat_t * p );
extern void Cnf_DataFree( Cnf_Dat_t * p );
extern void Cnf_DataLift( Cnf_Dat_t * p, int nVarsPlus );
extern Vec_Int_t * Cnf_DataCollectFlipLits( Cnf_Dat_t * p, int iFlipVar );
extern void Cnf_DataCollectFlipLits( Cnf_Dat_t * p, int iFlipVar, Vec_Int_t * vFlips );
extern void Cnf_DataLiftAndFlipLits( Cnf_Dat_t * p, int nVarsPlus, Vec_Int_t * vLits );
extern void Cnf_DataPrint( Cnf_Dat_t * p, int fReadable );
extern void Cnf_DataWriteIntoFile( Cnf_Dat_t * p, char * pFileName, int fReadable, Vec_Int_t * vForAlls, Vec_Int_t * vExists );

8
src/sat/cnf/cnfMan.c
View File

@ -215,14 +215,14 @@ void Cnf_DataLift( Cnf_Dat_t * p, int nVarsPlus )
for ( v = 0; v < p->nLiterals; v++ )
p->pClauses[0][v] += 2*nVarsPlus;
}
Vec_Int_t * Cnf_DataCollectFlipLits( Cnf_Dat_t * p, int iFlipVar )
void Cnf_DataCollectFlipLits( Cnf_Dat_t * p, int iFlipVar, Vec_Int_t * vFlips )
{
Vec_Int_t * vLits = Vec_IntAlloc( 100 ); int v;
int v;
assert( p->pMan == NULL );
Vec_IntClear( vFlips );
for ( v = 0; v < p->nLiterals; v++ )
if ( Abc_Lit2Var(p->pClauses[0][v]) == iFlipVar )
Vec_IntPush( vLits, v );
return vLits;
Vec_IntPush( vFlips, v );
}
void Cnf_DataLiftAndFlipLits( Cnf_Dat_t * p, int nVarsPlus, Vec_Int_t * vLits )
{