Skip to content

A
abc
Commit 11ec4318 by Mathias Soeken
Options

Exact synthesis minimization.

parent 718266f6
Showing with 209 additions and 42 deletions
src/base/abci/abc.c
......@@ -136,6 +136,8 @@ static int Abc_CommandExtract ( Abc_Frame_t * pAbc, int argc, cha
static int Abc_CommandVarMin ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandDetect ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandExact ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandBmsStart ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandBmsPs ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandLogic ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandComb ( Abc_Frame_t * pAbc, int argc, char ** argv );
......@@ -777,6 +779,9 @@ void Abc_Init( Abc_Frame_t * pAbc )
Cmd_CommandAdd( pAbc, "Synthesis", "detect", Abc_CommandDetect, 0 );
Cmd_CommandAdd( pAbc, "Synthesis", "exact", Abc_CommandExact, 1 );
Cmd_CommandAdd( pAbc, "Exact synthesis", "bms_start", Abc_CommandBmsStart, 0 );
Cmd_CommandAdd( pAbc, "Exact synthesis", "bms_ps", Abc_CommandBmsPs, 0 );
Cmd_CommandAdd( pAbc, "Various", "logic", Abc_CommandLogic, 1 );
Cmd_CommandAdd( pAbc, "Various", "comb", Abc_CommandComb, 1 );
Cmd_CommandAdd( pAbc, "Various", "miter", Abc_CommandMiter, 1 );
......@@ -7407,6 +7412,118 @@ usage:
SeeAlso []
***********************************************************************/
int Abc_CommandBmsStart( Abc_Frame_t * pAbc, int argc, char ** argv )
{
extern int Abc_ExactIsRunning();
extern void Abc_ExactStart( int nBTLimit, int fVerbose );
int c, fVerbose = 0, nBTLimit = 10000;
Extra_UtilGetoptReset();
while ( ( c = Extra_UtilGetopt( argc, argv, "Cvh" ) ) != EOF )
{
switch ( c )
{
case 'C':
if ( globalUtilOptind >= argc )
{
Abc_Print( -1, "Command line switch \"-C\" should be followed by an integer.\n" );
goto usage;
}
nBTLimit = atoi(argv[globalUtilOptind]);
globalUtilOptind++;
break;
case 'v':
fVerbose ^= 1;
break;
case 'h':
goto usage;
default:
goto usage;
}
}
if ( Abc_ExactIsRunning() )
{
Abc_Print( -1, "BMS manager is already started." );
return 1;
}
Abc_ExactStart( nBTLimit, fVerbose );
return 0;
usage:
Abc_Print( -2, "usage: bms_start [-C <num>] [-vh]\n" );
Abc_Print( -2, "\t starts BMS manager for recording optimum networks\n" );
Abc_Print( -2, "\t-C <num> : the limit on the number of conflicts [default = %d]\n", nBTLimit );
Abc_Print( -2, "\t-v : toggle verbose printout [default = %s]\n", fVerbose ? "yes" : "no" );
Abc_Print( -2, "\t-h : print the command usage\n" );
Abc_Print( -2, "\t\n" );
Abc_Print( -2, "\t This command was contributed by Mathias Soeken from EPFL in July 2016.\n" );
Abc_Print( -2, "\t The author can be contacted as mathias.soeken at epfl.ch\n" );
return 1;
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Abc_CommandBmsPs( Abc_Frame_t * pAbc, int argc, char ** argv )
{
extern int Abc_ExactIsRunning();
extern void Abc_ExactStats();
int c;
Extra_UtilGetoptReset();
while ( ( c = Extra_UtilGetopt( argc, argv, "h" ) ) != EOF )
{
switch ( c )
{
case 'h':
goto usage;
default:
goto usage;
}
}
if ( !Abc_ExactIsRunning() )
{
Abc_Print( -1, "BMS manager is not started." );
return 1;
}
Abc_ExactStats();
return 0;
usage:
Abc_Print( -2, "usage: bms_ps [-h]\n" );
Abc_Print( -2, "\t shows statistics about BMS manager\n" );
Abc_Print( -2, "\t-h : print the command usage\n" );
Abc_Print( -2, "\t\n" );
Abc_Print( -2, "\t This command was contributed by Mathias Soeken from EPFL in July 2016.\n" );
Abc_Print( -2, "\t The author can be contacted as mathias.soeken at epfl.ch\n" );
return 1;
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Abc_CommandLogic( Abc_Frame_t * pAbc, int argc, char ** argv )
{
Abc_Ntk_t * pNtk, * pNtkRes;
......@@ -16928,7 +17045,7 @@ int Abc_CommandIf( Abc_Frame_t * pAbc, int argc, char ** argv )
}
if ( Abc_NtkRecInputNum3() != pPars->nLutSize )
{
printf( "The number of library inputs (%d) different from the K parameters (%d).\n", Abc_NtkRecInputNum3(), pPars->nLutSize );
printf( "The number of library inputs (%d) is different from the K parameters (%d).\n", Abc_NtkRecInputNum3(), pPars->nLutSize );
return 0;
}
}
......@@ -16937,12 +17054,12 @@ int Abc_CommandIf( Abc_Frame_t * pAbc, int argc, char ** argv )
{
if ( !Abc_ExactIsRunning() )
{
printf( "LMS manager is not running (use \"rec_start3\").\n" );
printf( "BMS manager is not running (use \"bms_start\").\n" );
return 0;
}
if ( Abc_ExactInputNum() != pPars->nLutSize )
if ( Abc_ExactInputNum() < pPars->nLutSize )
{
printf( "The number of library inputs (%d) different from the K parameters (%d).\n", Abc_ExactInputNum(), pPars->nLutSize );
printf( "The number of library inputs (%d) is smaller than the K parameters (%d).\n", Abc_ExactInputNum(), pPars->nLutSize );
return 0;
}
}
src/base/abci/abcExact.c
......@@ -123,6 +123,10 @@ struct Ses_Store_t_
int fVerbose; /* be verbose */
int nBTLimit; /* conflict limit */
Ses_TruthEntry_t * pEntries[SES_STORE_TABLE_SIZE]; /* hash table for truth table entries */
unsigned long nCutCount;
unsigned long pCutCount[9];
unsigned long nCacheHit;
};
static Ses_Store_t * s_pSesStore = NULL;
......@@ -162,6 +166,10 @@ static inline Ses_Store_t * Ses_StoreAlloc( int nBTLimit, int fVerbose )
pStore->nBTLimit = nBTLimit;
memset( pStore->pEntries, 0, SES_STORE_TABLE_SIZE );
pStore->nCutCount = 0;
memset( pStore->pCutCount, 0, 9 );
pStore->nCacheHit = 0;
return pStore;
}
......@@ -524,7 +532,7 @@ static inline void Ses_ManCreateMainClause( Ses_Man_t * pSes, int t, int i, int
assert( value );
}
static void Ses_ManCreateClauses( Ses_Man_t * pSes )
static int Ses_ManCreateClauses( Ses_Man_t * pSes )
{
extern int Extra_TruthVarsSymm( unsigned * pTruth, int nVars, int iVar0, int iVar1 );
......@@ -731,10 +739,13 @@ static void Ses_ManCreateClauses( Ses_Man_t * pSes )
{
pLits[0] = Abc_Var2Lit( Ses_ManOutputVar( pSes, h, i ), 1 );
pLits[1] = Abc_Var2Lit( Ses_ManDepthVar( pSes, i, pSes->nMaxDepth ), 1 );
assert( sat_solver_addclause( pSes->pSat, pLits, pLits + 2 ) );
if ( !sat_solver_addclause( pSes->pSat, pLits, pLits + 2 ) )
return 0;
}
}
}
return 1;
}
/**Function*************************************************************
......@@ -1129,7 +1140,8 @@ static int Ses_ManFindMinimumSize( Ses_Man_t * pSes )
return 0;
Ses_ManCreateVars( pSes, nGates );
Ses_ManCreateClauses( pSes );
if ( !Ses_ManCreateClauses( pSes ) )
return 0; /* proven UNSAT while creating clauses */
switch ( Ses_ManSolve( pSes ) )
{
......@@ -1355,7 +1367,7 @@ void Abc_ExactStart( int nBTLimit, int fVerbose )
if ( !s_pSesStore )
s_pSesStore = Ses_StoreAlloc( nBTLimit, fVerbose );
else
printf( "exact store manager already started\n" );
printf( "BMS manager already started\n" );
}
// stop exact store manager
void Abc_ExactStop()
......@@ -1363,46 +1375,84 @@ void Abc_ExactStop()
if ( s_pSesStore )
Ses_StoreClean( s_pSesStore );
else
printf( "exact store manager has not been started\n" );
printf( "BMS manager has not been started\n" );
}
// show statistics about store manager
void Abc_ExactStats()
{
int i;
if ( !s_pSesStore )
{
printf( "BMS manager has not been started\n" );
return;
}
printf( "number of considered cuts :" );
for ( i = 2; i < 9; ++i )
printf( " %d = %lu ", i, s_pSesStore->pCutCount[i] );
printf( " total = %lu\n", s_pSesStore->nCutCount );
printf( "cache hits : %lu\n", s_pSesStore->nCacheHit );
}
// this procedure takes TT and input arrival times (pArrTimeProfile) and return the smallest output arrival time;
// it also returns the pin-to-pin delays (pPerm) between each cut leaf and the cut output and the cut area cost (Cost)
// the area cost should not exceed 2048, if the cut is implementable; otherwise, it should be ABC_INFINITY
int Abc_ExactDelayCost( word * pTruth, int nVars, int * pArrTimeProfile, char * pPerm, int * Cost, int AigLevel )
{
int i, l;
Ses_Man_t * pSes;
int i, l, fExists = 0;
Ses_Man_t * pSes = NULL;
char * pSol = NULL, * p;
int Delay = ABC_INFINITY, nMaxDepth;
abctime timeStart;
/* some checks */
assert( nVars >= 2 && nVars <= 8 );
if ( nVars < 2 || nVars > 8 )
{
printf( "invalid truth table size %d\n", nVars );
assert( 0 );
}
nMaxDepth = pArrTimeProfile[0];
for ( i = 1; i < nVars; ++i )
nMaxDepth = Abc_MaxInt( nMaxDepth, pArrTimeProfile[i] );
nMaxDepth = Abc_MinInt( AigLevel, nMaxDepth + nVars + 1 );
/* statistics */
s_pSesStore->nCutCount++;
s_pSesStore->pCutCount[nVars]++;
timeStart = Abc_Clock();
pSol = Ses_StoreGetEntry( s_pSesStore, pTruth, nVars, pArrTimeProfile );
if ( pSol )
{
s_pSesStore->nCacheHit++;
fExists = 1;
}
else
{
nMaxDepth = pArrTimeProfile[0];
for ( i = 1; i < nVars; ++i )
nMaxDepth = Abc_MaxInt( nMaxDepth, pArrTimeProfile[i] );
nMaxDepth = Abc_MinInt( AigLevel, nMaxDepth + nVars + 1 );
*Cost = ABC_INFINITY;
timeStart = Abc_Clock();
pSes = Ses_ManAlloc( pTruth, nVars, 1 /* fSpecFunc */, nMaxDepth, pArrTimeProfile, 1 /* fMakeAIG */, s_pSesStore->fVerbose );
pSes->nBTLimit = s_pSesStore->nBTLimit;
*Cost = ABC_INFINITY;
while ( 1 ) /* there is improvement */
{
printf( "try with %d\n", pSes->nMaxDepth );
if ( Ses_ManFindMinimumSize( pSes ) )
pSes = Ses_ManAlloc( pTruth, nVars, 1 /* fSpecFunc */, nMaxDepth, pArrTimeProfile, 1 /* fMakeAIG */, s_pSesStore->fVerbose );
pSes->nBTLimit = s_pSesStore->nBTLimit;
while ( 1 ) /* there is improvement */
{
if ( pSol )
ABC_FREE( pSol );
pSol = Ses_ManExtractSolution( pSes );
pSes->nMaxDepth--;
if ( Ses_ManFindMinimumSize( pSes ) )
{
if ( pSol )
ABC_FREE( pSol );
pSol = Ses_ManExtractSolution( pSes );
pSes->nMaxDepth--;
}
else
break;
}
else
break;
pSes->timeTotal = Abc_Clock() - timeStart;
/* cleanup */
Ses_ManClean( pSes );
}
if ( pSol )
......@@ -1414,15 +1464,10 @@ int Abc_ExactDelayCost( word * pTruth, int nVars, int * pArrTimeProfile, char *
pPerm[l] = *p++;
/* store solution */
if ( !Ses_StoreAddEntry( s_pSesStore, pTruth, nVars, pArrTimeProfile, pSol ) )
ABC_FREE( pSol ); /* store entry already exists, so free solution */
if ( !fExists )
Ses_StoreAddEntry( s_pSesStore, pTruth, nVars, pArrTimeProfile, pSol );
}
pSes->timeTotal = Abc_Clock() - timeStart;
/* cleanup */
Ses_ManClean( pSes );
return Delay;
}
// this procedure returns a new node whose output in terms of the given fanins
......@@ -1430,7 +1475,7 @@ int Abc_ExactDelayCost( word * pTruth, int nVars, int * pArrTimeProfile, char *
Abc_Obj_t * Abc_ExactBuildNode( word * pTruth, int nVars, int * pArrTimeProfile, Abc_Obj_t ** pFanins )
{
char * pSol;
int i;
int i, j;
char const * p;
Abc_Obj_t * pObj;
Vec_Ptr_t * pGates;
......@@ -1468,6 +1513,11 @@ Abc_Obj_t * Abc_ExactBuildNode( word * pTruth, int nVars, int * pArrTimeProfile,
assert( *p == 2 ); /* binary gate */
++p;
/* invert truth table if we are last gate and inverted */
if ( i + 1 == pSol[ABC_EXACT_SOL_NGATES] && Abc_LitIsCompl( *( p + 2 ) ) )
for ( j = 0; j < 4; ++j )
pGateTruth[j] = ( pGateTruth[j] == '0' ) ? '1' : '0';
pSopCover = Abc_SopFromTruthBin( pGateTruth );
pObj = Abc_NtkCreateNode( pNtk );
pObj->pData = Abc_SopRegister( (Mem_Flex_t*)pNtk->pManFunc, pSopCover );
......@@ -1479,10 +1529,10 @@ Abc_Obj_t * Abc_ExactBuildNode( word * pTruth, int nVars, int * pArrTimeProfile,
}
/* output */
if ( Abc_LitIsCompl( *p ) )
pObj = Abc_NtkCreateNodeInv( pNtk, (Abc_Obj_t *)Vec_PtrEntry( pGates, nVars + Abc_Lit2Var( *p ) ) );
else
pObj = (Abc_Obj_t *)Vec_PtrEntry( pGates, nVars + Abc_Lit2Var( *p ) );
//if ( Abc_LitIsCompl( *p ) )
// pObj = Abc_NtkCreateNodeInv( pNtk, (Abc_Obj_t *)Vec_PtrEntry( pGates, nVars + Abc_Lit2Var( *p ) ) );
//else
pObj = (Abc_Obj_t *)Vec_PtrEntry( pGates, nVars + Abc_Lit2Var( *p ) );
Vec_PtrFree( pGates );
......
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