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

BMS fixes and start gates parameter.

This commit is contained in:
Mathias Soeken 2016-08-25 10:56:59 +02:00
parent 360e85fce2
commit e5636522bf
3 changed files with 34 additions and 26 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

2
src/base/abc/abc.h
View File

@ -646,7 +646,7 @@ extern ABC_DLL Vec_Ptr_t * Abc_AigGetLevelizedOrder( Abc_Ntk_t * pNtk, in
extern ABC_DLL int Abc_ExactInputNum(); extern ABC_DLL int Abc_ExactInputNum();
extern ABC_DLL int Abc_ExactIsRunning(); extern ABC_DLL int Abc_ExactIsRunning();
extern ABC_DLL Abc_Obj_t * Abc_ExactBuildNode( word * pTruth, int nVars, int * pArrTimeProfile, Abc_Obj_t ** pFanins, Abc_Ntk_t * pNtk ); extern ABC_DLL Abc_Obj_t * Abc_ExactBuildNode( word * pTruth, int nVars, int * pArrTimeProfile, Abc_Obj_t ** pFanins, Abc_Ntk_t * pNtk );
extern ABC_DLL Abc_Ntk_t * Abc_NtkFindExact( word * pTruth, int nVars, int nFunc, int nMaxDepth, int * pArrivalTimes, int nBTLimit, int fVerbose ); extern ABC_DLL Abc_Ntk_t * Abc_NtkFindExact( word * pTruth, int nVars, int nFunc, int nMaxDepth, int * pArrivalTimes, int nBTLimit, int nStartGates, int fVerbose );
/*=== abcFanio.c ==========================================================*/ /*=== abcFanio.c ==========================================================*/
extern ABC_DLL void Abc_ObjAddFanin( Abc_Obj_t * pObj, Abc_Obj_t * pFanin ); extern ABC_DLL void Abc_ObjAddFanin( Abc_Obj_t * pObj, Abc_Obj_t * pFanin );
extern ABC_DLL void Abc_ObjDeleteFanin( Abc_Obj_t * pObj, Abc_Obj_t * pFanin ); extern ABC_DLL void Abc_ObjDeleteFanin( Abc_Obj_t * pObj, Abc_Obj_t * pFanin );

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

@ -7291,9 +7291,9 @@ usage:
***********************************************************************/ ***********************************************************************/
int Abc_CommandExact( Abc_Frame_t * pAbc, int argc, char ** argv ) int Abc_CommandExact( Abc_Frame_t * pAbc, int argc, char ** argv )
{ {
extern Gia_Man_t * Gia_ManFindExact( word * pTruth, int nVars, int nFunc, int nMaxDepth, int * pArrivalTimes, int nBTLimit, int fVerbose ); extern Gia_Man_t * Gia_ManFindExact( word * pTruth, int nVars, int nFunc, int nMaxDepth, int * pArrivalTimes, int nBTLimit, int nStartGates, int fVerbose );
int c, nMaxDepth = -1, fMakeAIG = 0, fTest = 0, fVerbose = 0, nVars = 0, nVarsTmp, nFunc = 0, nBTLimit = 100; int c, nMaxDepth = -1, fMakeAIG = 0, fTest = 0, fVerbose = 0, nVars = 0, nVarsTmp, nFunc = 0, nStartGates = 1, nBTLimit = 100;
char * p1, * p2; char * p1, * p2;
word pTruth[64]; word pTruth[64];
int pArrTimeProfile[8], fHasArrTimeProfile = 0; int pArrTimeProfile[8], fHasArrTimeProfile = 0;
@ -7301,7 +7301,7 @@ int Abc_CommandExact( Abc_Frame_t * pAbc, int argc, char ** argv )
Gia_Man_t * pGiaRes; Gia_Man_t * pGiaRes;
Extra_UtilGetoptReset(); Extra_UtilGetoptReset();
while ( ( c = Extra_UtilGetopt( argc, argv, "DACatvh" ) ) != EOF ) while ( ( c = Extra_UtilGetopt( argc, argv, "DASCatvh" ) ) != EOF )
{ {
switch ( c ) switch ( c )
{ {
@ -7341,6 +7341,17 @@ int Abc_CommandExact( Abc_Frame_t * pAbc, int argc, char ** argv )
++p2; ++p2;
} }
break; break;
case 'S':
if ( globalUtilOptind >= argc )
{
Abc_Print( -1, "Command line switch \"-S\" should be followed by an integer.\n" );
goto usage;
}
nStartGates = atoi(argv[globalUtilOptind]);
globalUtilOptind++;
if ( nStartGates < 1 )
goto usage;
break;
case 'C': case 'C':
if ( globalUtilOptind >= argc ) if ( globalUtilOptind >= argc )
{ {
@ -7406,7 +7417,7 @@ int Abc_CommandExact( Abc_Frame_t * pAbc, int argc, char ** argv )
if ( fMakeAIG ) if ( fMakeAIG )
{ {
pGiaRes = Gia_ManFindExact( pTruth, nVars, nFunc, nMaxDepth, fHasArrTimeProfile ? pArrTimeProfile : NULL, nBTLimit, fVerbose ); pGiaRes = Gia_ManFindExact( pTruth, nVars, nFunc, nMaxDepth, fHasArrTimeProfile ? pArrTimeProfile : NULL, nBTLimit, nStartGates - 1, fVerbose );
if ( pGiaRes ) if ( pGiaRes )
Abc_FrameUpdateGia( pAbc, pGiaRes ); Abc_FrameUpdateGia( pAbc, pGiaRes );
else else
@ -7414,7 +7425,7 @@ int Abc_CommandExact( Abc_Frame_t * pAbc, int argc, char ** argv )
} }
else else
{ {
pNtkRes = Abc_NtkFindExact( pTruth, nVars, nFunc, nMaxDepth, fHasArrTimeProfile ? pArrTimeProfile : NULL, nBTLimit, fVerbose ); pNtkRes = Abc_NtkFindExact( pTruth, nVars, nFunc, nMaxDepth, fHasArrTimeProfile ? pArrTimeProfile : NULL, nBTLimit, nStartGates - 1, fVerbose );
if ( pNtkRes ) if ( pNtkRes )
{ {
Abc_FrameReplaceCurrentNetwork( pAbc, pNtkRes ); Abc_FrameReplaceCurrentNetwork( pAbc, pNtkRes );
@ -7426,10 +7437,11 @@ int Abc_CommandExact( Abc_Frame_t * pAbc, int argc, char ** argv )
return 0; return 0;
usage: usage:
Abc_Print( -2, "usage: exact [-D <num>] [-atvh] <truth1> <truth2> ...\n" ); Abc_Print( -2, "usage: exact [-DSC <num>] [-A <list>] [-atvh] <truth1> <truth2> ...\n" );
Abc_Print( -2, "\t finds optimum networks using SAT-based exact synthesis for hex truth tables <truth1> <truth2> ...\n" ); Abc_Print( -2, "\t finds optimum networks using SAT-based exact synthesis for hex truth tables <truth1> <truth2> ...\n" );
Abc_Print( -2, "\t-D <num> : constrain maximum depth (if too low, algorithm may not terminate)\n" ); Abc_Print( -2, "\t-D <num> : constrain maximum depth (if too low, algorithm may not terminate)\n" );
Abc_Print( -2, "\t-A <list> : input arrival times (comma separated list)\n" ); Abc_Print( -2, "\t-A <list> : input arrival times (comma separated list)\n" );
Abc_Print( -2, "\t-S <num> : number of start gates in search [default = %s]\n", nStartGates );
Abc_Print( -2, "\t-C <num> : the limit on the number of conflicts [default = %d]\n", nBTLimit ); Abc_Print( -2, "\t-C <num> : the limit on the number of conflicts [default = %d]\n", nBTLimit );
Abc_Print( -2, "\t-a : toggle create AIG [default = %s]\n", fMakeAIG ? "yes" : "no" ); Abc_Print( -2, "\t-a : toggle create AIG [default = %s]\n", fMakeAIG ? "yes" : "no" );
Abc_Print( -2, "\t-t : run test suite\n" ); Abc_Print( -2, "\t-t : run test suite\n" );

34
src/base/abci/abcExact.c
View File

@ -966,17 +966,11 @@ static int Ses_ManCreateClauses( Ses_Man_t * pSes )
{ {
pLits[0] = Abc_Var2Lit( Ses_ManOutputVar( pSes, 0, i ), 1 ); pLits[0] = Abc_Var2Lit( Ses_ManOutputVar( pSes, 0, i ), 1 );
if ( !sat_solver_addclause( pSes->pSat, pLits, pLits + 1 ) ) if ( !sat_solver_addclause( pSes->pSat, pLits, pLits + 1 ) )
{
Vec_IntFree( vLits );
return 0; return 0;
} }
}
pLits[0] = Abc_Var2Lit( Ses_ManOutputVar( pSes, 0, pSes->nGates - 1 ), 0 ); pLits[0] = Abc_Var2Lit( Ses_ManOutputVar( pSes, 0, pSes->nGates - 1 ), 0 );
if ( !sat_solver_addclause( pSes->pSat, pLits, pLits + 1 ) ) if ( !sat_solver_addclause( pSes->pSat, pLits, pLits + 1 ) )
{
Vec_IntFree( vLits );
return 0; return 0;
}
vLits = Vec_IntAlloc( 0u ); vLits = Vec_IntAlloc( 0u );
} }
@ -1744,7 +1738,7 @@ static int Ses_ManFindMinimumSize( Ses_Man_t * pSes )
pSes->fHitResLimit = 0; pSes->fHitResLimit = 0;
/* do the arrival times allow for a network? */ /* do the arrival times allow for a network? */
if ( pSes->nMaxDepth != -1 && !Ses_CheckDepthConsistency( pSes ) ) if ( pSes->nMaxDepth != -1 && pSes->pArrTimeProfile && !Ses_CheckDepthConsistency( pSes ) )
return 0; return 0;
//Ses_ManStoreDepthAndArrivalTimes( pSes ); //Ses_ManStoreDepthAndArrivalTimes( pSes );
@ -1818,7 +1812,7 @@ static int Ses_ManFindMinimumSize( Ses_Man_t * pSes )
SeeAlso [] SeeAlso []
***********************************************************************/ ***********************************************************************/
Abc_Ntk_t * Abc_NtkFindExact( word * pTruth, int nVars, int nFunc, int nMaxDepth, int * pArrTimeProfile, int nBTLimit, int fVerbose ) Abc_Ntk_t * Abc_NtkFindExact( word * pTruth, int nVars, int nFunc, int nMaxDepth, int * pArrTimeProfile, int nBTLimit, int nStartGates, int fVerbose )
{ {
Ses_Man_t * pSes; Ses_Man_t * pSes;
char * pSol; char * pSol;
@ -1831,6 +1825,7 @@ Abc_Ntk_t * Abc_NtkFindExact( word * pTruth, int nVars, int nFunc, int nMaxDepth
timeStart = Abc_Clock(); timeStart = Abc_Clock();
pSes = Ses_ManAlloc( pTruth, nVars, nFunc, nMaxDepth, pArrTimeProfile, 0, nBTLimit, fVerbose ); pSes = Ses_ManAlloc( pTruth, nVars, nFunc, nMaxDepth, pArrTimeProfile, 0, nBTLimit, fVerbose );
pSes->nStartGates = nStartGates;
if ( fVerbose ) if ( fVerbose )
Ses_ManPrintFuncs( pSes ); Ses_ManPrintFuncs( pSes );
@ -1852,7 +1847,7 @@ Abc_Ntk_t * Abc_NtkFindExact( word * pTruth, int nVars, int nFunc, int nMaxDepth
return pNtk; return pNtk;
} }
Gia_Man_t * Gia_ManFindExact( word * pTruth, int nVars, int nFunc, int nMaxDepth, int * pArrTimeProfile, int nBTLimit, int fVerbose ) Gia_Man_t * Gia_ManFindExact( word * pTruth, int nVars, int nFunc, int nMaxDepth, int * pArrTimeProfile, int nBTLimit, int nStartGates, int fVerbose )
{ {
Ses_Man_t * pSes; Ses_Man_t * pSes;
char * pSol; char * pSol;
@ -1865,6 +1860,7 @@ Gia_Man_t * Gia_ManFindExact( word * pTruth, int nVars, int nFunc, int nMaxDepth
timeStart = Abc_Clock(); timeStart = Abc_Clock();
pSes = Ses_ManAlloc( pTruth, nVars, nFunc, nMaxDepth, pArrTimeProfile, 1, nBTLimit, fVerbose ); pSes = Ses_ManAlloc( pTruth, nVars, nFunc, nMaxDepth, pArrTimeProfile, 1, nBTLimit, fVerbose );
pSes->nStartGates = nStartGates;
pSes->fVeryVerbose = 1; pSes->fVeryVerbose = 1;
pSes->fExtractVerbose = 1; pSes->fExtractVerbose = 1;
pSes->fSatVerbose = 1; pSes->fSatVerbose = 1;
@ -1920,30 +1916,30 @@ void Abc_ExactTestSingleOutput( int fVerbose )
pNtk = Abc_NtkFromTruthTable( pTruth, 4 ); pNtk = Abc_NtkFromTruthTable( pTruth, 4 );
pNtk2 = Abc_NtkFindExact( pTruth, 4, 1, -1, NULL, 0, fVerbose ); pNtk2 = Abc_NtkFindExact( pTruth, 4, 1, -1, NULL, 0, 0, fVerbose );
Abc_NtkShortNames( pNtk2 ); Abc_NtkShortNames( pNtk2 );
Abc_NtkCecSat( pNtk, pNtk2, 10000, 0 ); Abc_NtkCecSat( pNtk, pNtk2, 10000, 0 );
assert( pNtk2 ); assert( pNtk2 );
assert( Abc_NtkNodeNum( pNtk2 ) == 6 ); assert( Abc_NtkNodeNum( pNtk2 ) == 6 );
Abc_NtkDelete( pNtk2 ); Abc_NtkDelete( pNtk2 );
pNtk3 = Abc_NtkFindExact( pTruth, 4, 1, 3, NULL, 0, fVerbose ); pNtk3 = Abc_NtkFindExact( pTruth, 4, 1, 3, NULL, 0, 0, fVerbose );
Abc_NtkShortNames( pNtk3 ); Abc_NtkShortNames( pNtk3 );
Abc_NtkCecSat( pNtk, pNtk3, 10000, 0 ); Abc_NtkCecSat( pNtk, pNtk3, 10000, 0 );
assert( pNtk3 ); assert( pNtk3 );
assert( Abc_NtkLevel( pNtk3 ) <= 3 ); assert( Abc_NtkLevel( pNtk3 ) <= 3 );
Abc_NtkDelete( pNtk3 ); Abc_NtkDelete( pNtk3 );
pNtk4 = Abc_NtkFindExact( pTruth, 4, 1, 9, pArrTimeProfile, 50000, fVerbose ); pNtk4 = Abc_NtkFindExact( pTruth, 4, 1, 9, pArrTimeProfile, 50000, 0, fVerbose );
Abc_NtkShortNames( pNtk4 ); Abc_NtkShortNames( pNtk4 );
Abc_NtkCecSat( pNtk, pNtk4, 10000, 0 ); Abc_NtkCecSat( pNtk, pNtk4, 10000, 0 );
assert( pNtk4 ); assert( pNtk4 );
assert( Abc_NtkLevel( pNtk4 ) <= 9 ); assert( Abc_NtkLevel( pNtk4 ) <= 9 );
Abc_NtkDelete( pNtk4 ); Abc_NtkDelete( pNtk4 );
assert( !Abc_NtkFindExact( pTruth, 4, 1, 2, NULL, 50000, fVerbose ) ); assert( !Abc_NtkFindExact( pTruth, 4, 1, 2, NULL, 50000, 0, fVerbose ) );
assert( !Abc_NtkFindExact( pTruth, 4, 1, 8, pArrTimeProfile, 50000, fVerbose ) ); assert( !Abc_NtkFindExact( pTruth, 4, 1, 8, pArrTimeProfile, 50000, 0, fVerbose ) );
Abc_NtkDelete( pNtk ); Abc_NtkDelete( pNtk );
} }
@ -1962,27 +1958,27 @@ void Abc_ExactTestSingleOutputAIG( int fVerbose )
Abc_NtkToAig( pNtk ); Abc_NtkToAig( pNtk );
pGia = Abc_NtkAigToGia( pNtk, 1 ); pGia = Abc_NtkAigToGia( pNtk, 1 );
pGia2 = Gia_ManFindExact( pTruth, 4, 1, -1, NULL, 0, fVerbose ); pGia2 = Gia_ManFindExact( pTruth, 4, 1, -1, NULL, 0, 0, fVerbose );
pMiter = Gia_ManMiter( pGia, pGia2, 0, 1, 0, 0, 1 ); pMiter = Gia_ManMiter( pGia, pGia2, 0, 1, 0, 0, 1 );
assert( pMiter ); assert( pMiter );
Cec_ManVerify( pMiter, pPars ); Cec_ManVerify( pMiter, pPars );
Gia_ManStop( pMiter ); Gia_ManStop( pMiter );
pGia3 = Gia_ManFindExact( pTruth, 4, 1, 3, NULL, 0, fVerbose ); pGia3 = Gia_ManFindExact( pTruth, 4, 1, 3, NULL, 0, 0, fVerbose );
pMiter = Gia_ManMiter( pGia, pGia3, 0, 1, 0, 0, 1 ); pMiter = Gia_ManMiter( pGia, pGia3, 0, 1, 0, 0, 1 );
assert( pMiter ); assert( pMiter );
Cec_ManVerify( pMiter, pPars ); Cec_ManVerify( pMiter, pPars );
Gia_ManStop( pMiter ); Gia_ManStop( pMiter );
pGia4 = Gia_ManFindExact( pTruth, 4, 1, 9, pArrTimeProfile, 50000, fVerbose ); pGia4 = Gia_ManFindExact( pTruth, 4, 1, 9, pArrTimeProfile, 50000, 0, fVerbose );
pMiter = Gia_ManMiter( pGia, pGia4, 0, 1, 0, 0, 1 ); pMiter = Gia_ManMiter( pGia, pGia4, 0, 1, 0, 0, 1 );
assert( pMiter ); assert( pMiter );
Cec_ManVerify( pMiter, pPars ); Cec_ManVerify( pMiter, pPars );
Gia_ManStop( pMiter ); Gia_ManStop( pMiter );
assert( !Gia_ManFindExact( pTruth, 4, 1, 2, NULL, 50000, fVerbose ) ); assert( !Gia_ManFindExact( pTruth, 4, 1, 2, NULL, 50000, 0, fVerbose ) );
assert( !Gia_ManFindExact( pTruth, 4, 1, 8, pArrTimeProfile, 50000, fVerbose ) ); assert( !Gia_ManFindExact( pTruth, 4, 1, 8, pArrTimeProfile, 50000, 0, fVerbose ) );
Gia_ManStop( pGia ); Gia_ManStop( pGia );
Gia_ManStop( pGia2 ); Gia_ManStop( pGia2 );