mirror of https://github.com/YosysHQ/abc.git
Improvements to BMS.
This commit is contained in:
Mathias Soeken
parent
ea3836ea5d
commit
fcf3335041
|
|
@ -53,6 +53,14 @@ static word s_Truths8[32] = {
|
|||
#define ABC_EXACT_SOL_NFUNC 1
|
||||
#define ABC_EXACT_SOL_NGATES 2
|
||||
|
||||
#define ANSI_COLOR_RED "\x1b[31m"
|
||||
#define ANSI_COLOR_GREEN "\x1b[32m"
|
||||
#define ANSI_COLOR_YELLOW "\x1b[33m"
|
||||
#define ANSI_COLOR_BLUE "\x1b[34m"
|
||||
#define ANSI_COLOR_MAGENTA "\x1b[35m"
|
||||
#define ANSI_COLOR_CYAN "\x1b[36m"
|
||||
#define ANSI_COLOR_RESET "\x1b[0m"
|
||||
|
||||
typedef struct Ses_Man_t_ Ses_Man_t;
|
||||
struct Ses_Man_t_
|
||||
{
|
||||
|
|
@ -76,9 +84,12 @@ struct Ses_Man_t_
|
|||
int fVeryVerbose; /* be very verbose */
|
||||
int fExtractVerbose; /* be verbose about solution extraction */
|
||||
int fSatVerbose; /* be verbose about SAT solving */
|
||||
int fReasonVerbose; /* be verbose about give-up reasons */
|
||||
|
||||
int nGates; /* number of gates */
|
||||
int nStartGates; /* number of gates to start search (-1), i.e., to start from 1 gate, one needs to specify 0 */
|
||||
int fDecStructure; /* set to 1 or higher if nSpecFunc = 1 and f = x_i OP g(X \ {x_i}), otherwise 0 (determined when solving) */
|
||||
int pDecVars; /* mask of variables that can be decomposed at top-level */
|
||||
|
||||
int nSimVars; /* number of simulation vars x(i, t) */
|
||||
int nOutputVars; /* number of output variables g(h, i) */
|
||||
|
|
@ -311,7 +322,7 @@ static inline void Ses_StorePrintEntry( Ses_TruthEntry_t * pEntry, Ses_TimesEntr
|
|||
printf( "\n" );
|
||||
}
|
||||
|
||||
static inline void Ses_StorePrintDebugEntry( Ses_Store_t * pStore, word * pTruth, int nVars, int * pNormalArrTime, int nMaxDepth )
|
||||
static inline void Ses_StorePrintDebugEntry( Ses_Store_t * pStore, word * pTruth, int nVars, int * pNormalArrTime, int nMaxDepth, char * pSol )
|
||||
{
|
||||
int l;
|
||||
|
||||
|
|
@ -322,7 +333,11 @@ static inline void Ses_StorePrintDebugEntry( Ses_Store_t * pStore, word * pTruth
|
|||
fprintf( pStore->pDebugEntries, "%c%d", ( l == 0 ? ' ' : ',' ), pNormalArrTime[l] );
|
||||
fprintf( pStore->pDebugEntries, " " );
|
||||
Abc_TtPrintHexRev( pStore->pDebugEntries, pTruth, nVars );
|
||||
fprintf( pStore->pDebugEntries, "\"\n" );
|
||||
fprintf( pStore->pDebugEntries, "\" # " );
|
||||
|
||||
if ( !pSol )
|
||||
fprintf( pStore->pDebugEntries, "no " );
|
||||
fprintf( pStore->pDebugEntries, "solution found before\n" );
|
||||
}
|
||||
|
||||
static void Abc_ExactNormalizeArrivalTimesForNetwork( int nVars, int * pArrTimeProfile, char * pSol )
|
||||
|
|
@ -688,6 +703,33 @@ static void Ses_StoreRead( Ses_Store_t * pStore, const char * pFilename, int fSy
|
|||
printf( "read %lu entries from file\n", nEntries );
|
||||
}
|
||||
|
||||
// computes top decomposition of variables wrt. to AND and OR
|
||||
static inline void Ses_ManComputeTopDec( Ses_Man_t * pSes )
|
||||
{
|
||||
int l, i, mask = ~0;
|
||||
word * pVar;
|
||||
int fAnd, fAndC, fOr, fOrC;
|
||||
|
||||
if ( pSes->nSpecVars < 6u )
|
||||
mask = Abc_Tt6Mask( 1u << pSes->nSpecVars );
|
||||
|
||||
for ( l = 0; l < pSes->nSpecVars; ++l )
|
||||
{
|
||||
pVar = &s_Truths8[l << 2];
|
||||
fAnd = fAndC = fOr = fOrC = 1;
|
||||
|
||||
for ( i = 0; i < pSes->nSpecWords; ++i )
|
||||
{
|
||||
fAnd &= ( pVar[i] & pSes->pSpec[i] & mask ) != ( pSes->pSpec[i] & mask );
|
||||
fAndC &= ( ~pVar[i] & pSes->pSpec[i] & mask ) != ( pSes->pSpec[i] & mask );
|
||||
fOr &= ( pVar[i] & pSes->pSpec[i] & mask ) != ( pVar[i] & mask );
|
||||
fOrC &= ( ~pVar[i] & pSes->pSpec[i] & mask ) != ( ~pVar[i] & mask );
|
||||
}
|
||||
|
||||
pSes->pDecVars |= ( fAnd | fAndC | fOr | fOrC ) << l;
|
||||
}
|
||||
}
|
||||
|
||||
static inline Ses_Man_t * Ses_ManAlloc( word * pTruth, int nVars, int nFunc, int nMaxDepth, int * pArrTimeProfile, int fMakeAIG, int nBTLimit, int fVerbose )
|
||||
{
|
||||
int h, i;
|
||||
|
|
@ -720,6 +762,9 @@ static inline Ses_Man_t * Ses_ManAlloc( word * pTruth, int nVars, int nFunc, int
|
|||
p->fExtractVerbose = 0;
|
||||
p->fSatVerbose = 0;
|
||||
|
||||
if ( p->nSpecFunc == 1 )
|
||||
Ses_ManComputeTopDec( p );
|
||||
|
||||
return p;
|
||||
}
|
||||
|
||||
|
|
@ -876,7 +921,7 @@ static int Ses_ManCreateClauses( Ses_Man_t * pSes )
|
|||
|
||||
int h, i, j, k, t, ii, jj, kk, p, q;
|
||||
int pLits[3];
|
||||
Vec_Int_t * vLits = Vec_IntAlloc( 0u );
|
||||
Vec_Int_t * vLits = NULL;
|
||||
|
||||
for ( t = 0; t < pSes->nRows; ++t )
|
||||
for ( i = 0; i < pSes->nGates; ++i )
|
||||
|
|
@ -895,12 +940,14 @@ static int Ses_ManCreateClauses( Ses_Man_t * pSes )
|
|||
}
|
||||
|
||||
/* output clauses */
|
||||
for ( h = 0; h < pSes->nSpecFunc; ++h )
|
||||
{
|
||||
pLits[0] = Abc_Var2Lit( Ses_ManOutputVar( pSes, h, i ), 1 );
|
||||
pLits[1] = Abc_Var2Lit( Ses_ManSimVar( pSes, i, t ), 1 - Abc_TtGetBit( &pSes->pSpec[h << 2], t + 1 ) );
|
||||
sat_solver_addclause( pSes->pSat, pLits, pLits + 2 );
|
||||
}
|
||||
if ( pSes->nSpecFunc != 1 )
|
||||
for ( h = 0; h < pSes->nSpecFunc; ++h )
|
||||
{
|
||||
pLits[0] = Abc_Var2Lit( Ses_ManOutputVar( pSes, h, i ), 1 );
|
||||
pLits[1] = Abc_Var2Lit( Ses_ManSimVar( pSes, i, t ), 1 - Abc_TtGetBit( &pSes->pSpec[h << 2], t + 1 ) );
|
||||
if ( !sat_solver_addclause( pSes->pSat, pLits, pLits + 2 ) )
|
||||
return 0;
|
||||
}
|
||||
}
|
||||
|
||||
/* if there is only one output, we know it must point to the last gate */
|
||||
|
|
@ -921,9 +968,20 @@ static int Ses_ManCreateClauses( Ses_Man_t * pSes )
|
|||
Vec_IntFree( vLits );
|
||||
return 0;
|
||||
}
|
||||
|
||||
for ( t = 0; t < pSes->nRows; ++t )
|
||||
{
|
||||
pLits[0] = Abc_Var2Lit( Ses_ManSimVar( pSes, pSes->nGates - 1, t ), 1 - Abc_TtGetBit( pSes->pSpec, t + 1 ) );
|
||||
if ( !sat_solver_addclause( pSes->pSat, pLits, pLits + 1 ) )
|
||||
return 0;
|
||||
}
|
||||
|
||||
vLits = Vec_IntAlloc( 0u );
|
||||
}
|
||||
else
|
||||
{
|
||||
vLits = Vec_IntAlloc( 0u );
|
||||
|
||||
/* some output is selected */
|
||||
for ( h = 0; h < pSes->nSpecFunc; ++h )
|
||||
{
|
||||
|
|
@ -1154,6 +1212,9 @@ static inline int Ses_ManSolve( Ses_Man_t * pSes )
|
|||
status = sat_solver_solve( pSes->pSat, NULL, NULL, pSes->nBTLimit, 0, 0, 0 );
|
||||
timeDelta = Abc_Clock() - timeStart;
|
||||
|
||||
if ( pSes->fSatVerbose )
|
||||
Sat_SolverPrintStats( stdout, pSes->pSat );
|
||||
|
||||
pSes->timeSat += timeDelta;
|
||||
|
||||
if ( status == l_True )
|
||||
|
|
@ -1547,7 +1608,7 @@ static int Ses_CheckDepthConsistency( Ses_Man_t * pSes )
|
|||
{
|
||||
if ( pSes->pArrTimeProfile[l] >= pSes->nMaxDepth )
|
||||
{
|
||||
if ( pSes->fVeryVerbose )
|
||||
if ( pSes->fReasonVerbose )
|
||||
printf( "give up due to impossible arrival time (depth = %d, input = %d, arrival time = %d)", pSes->nMaxDepth, l, pSes->pArrTimeProfile[l] );
|
||||
return 0;
|
||||
}
|
||||
|
|
@ -1555,7 +1616,7 @@ static int Ses_CheckDepthConsistency( Ses_Man_t * pSes )
|
|||
{
|
||||
if ( ( pSes->fDecStructure == 1 && pSes->nSpecVars > 2 ) || pSes->fDecStructure == 2 )
|
||||
{
|
||||
if ( pSes->fVeryVerbose )
|
||||
if ( pSes->fReasonVerbose )
|
||||
printf( "give up due to impossible decomposition (depth = %d, input = %d, arrival time = %d)", pSes->nMaxDepth, l, pSes->pArrTimeProfile[l] );
|
||||
return 0;
|
||||
}
|
||||
|
|
@ -1566,16 +1627,12 @@ static int Ses_CheckDepthConsistency( Ses_Man_t * pSes )
|
|||
mask = Abc_Tt6Mask( 1u << pSes->nSpecVars );
|
||||
|
||||
/* A subset B <=> A and B = A */
|
||||
for ( i = 0; i < pSes->nSpecWords; ++i )
|
||||
if ( ( ( s_Truths8[(l << 2) + i] & pSes->pSpec[i] & mask ) != ( pSes->pSpec[i] & mask ) ) &&
|
||||
( ( ~( s_Truths8[(l << 2) + i] ) & pSes->pSpec[i] & mask ) != ( pSes->pSpec[i] & mask ) ) &&
|
||||
( ( ( s_Truths8[(l << 2) + i] | pSes->pSpec[i] ) & mask ) != ( pSes->pSpec[i] & mask ) ) &&
|
||||
( ( ( ~( s_Truths8[(l << 2) + i] ) | pSes->pSpec[i] ) & mask ) != ( pSes->pSpec[i] & mask ) ) )
|
||||
{
|
||||
if ( pSes->fVeryVerbose )
|
||||
printf( "give up due to impossible decomposition (depth = %d, input = %d, arrival time = %d)", pSes->nMaxDepth, l, pSes->pArrTimeProfile[l] );
|
||||
return 0;
|
||||
}
|
||||
if ( !( ( pSes->pDecVars >> l ) & 1 ) )
|
||||
{
|
||||
if ( pSes->fReasonVerbose )
|
||||
printf( "give up due to impossible decomposition (depth = %d, input = %d, arrival time = %d)", pSes->nMaxDepth, l, pSes->pArrTimeProfile[l] );
|
||||
return 0;
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
|
|
@ -1590,7 +1647,7 @@ static int Ses_CheckDepthConsistency( Ses_Man_t * pSes )
|
|||
if ( pSes->pArrTimeProfile[l] + 2 == pSes->nMaxDepth )
|
||||
if ( ++i > fMaxGatesLevel2 )
|
||||
{
|
||||
if ( pSes->fVeryVerbose )
|
||||
if ( pSes->fReasonVerbose )
|
||||
printf( "give up due to impossible decomposition at second level (depth = %d, input = %d, arrival time = %d)", pSes->nMaxDepth, l, pSes->pArrTimeProfile[l] );
|
||||
return 0;
|
||||
}
|
||||
|
|
@ -1603,7 +1660,7 @@ static int Ses_CheckDepthConsistency( Ses_Man_t * pSes )
|
|||
if ( pSes->pArrTimeProfile[l] + 3 == pSes->nMaxDepth )
|
||||
if ( ++i > 1 )
|
||||
{
|
||||
if ( pSes->fVeryVerbose )
|
||||
if ( pSes->fReasonVerbose )
|
||||
printf( "give up due to impossible decomposition at third level (depth = %d, input = %d, arrival time = %d)", pSes->nMaxDepth, l, pSes->pArrTimeProfile[l] );
|
||||
return 0;
|
||||
}
|
||||
|
|
@ -1618,14 +1675,14 @@ static int Ses_CheckGatesConsistency( Ses_Man_t * pSes, int nGates )
|
|||
/* give up if number of gates is impossible for given depth */
|
||||
if ( pSes->nMaxDepth != -1 && nGates >= (1 << pSes->nMaxDepth ) )
|
||||
{
|
||||
if ( pSes->fVeryVerbose )
|
||||
if ( pSes->fReasonVerbose )
|
||||
printf( "give up due to impossible depth (depth = %d, gates = %d)", pSes->nMaxDepth, nGates );
|
||||
return 0;
|
||||
}
|
||||
|
||||
if ( pSes->fDecStructure && nGates >= ( 1 << ( pSes->nMaxDepth - 1 ) ) + 1 )
|
||||
{
|
||||
if ( pSes->fVeryVerbose )
|
||||
if ( pSes->fReasonVerbose )
|
||||
printf( "give up due to impossible depth in AND-dec structure (depth = %d, gates = %d)", pSes->nMaxDepth, nGates );
|
||||
return 0;
|
||||
}
|
||||
|
|
@ -1633,7 +1690,7 @@ static int Ses_CheckGatesConsistency( Ses_Man_t * pSes, int nGates )
|
|||
/* give up if number of gates gets practically too large */
|
||||
if ( nGates >= ( 1 << pSes->nSpecVars ) )
|
||||
{
|
||||
if ( pSes->fVeryVerbose )
|
||||
if ( pSes->fReasonVerbose )
|
||||
printf( "give up due to impossible number of gates" );
|
||||
return 0;
|
||||
}
|
||||
|
|
@ -1678,7 +1735,7 @@ static void Ses_AdjustDepthAndArrivalTimes( Ses_Man_t * pSes, int nGates )
|
|||
|
||||
static int Ses_ManFindMinimumSize( Ses_Man_t * pSes )
|
||||
{
|
||||
int nGates = 0, f, fRes, fSat;
|
||||
int nGates = pSes->nStartGates, f, fRes, fSat;
|
||||
abctime timeStart;
|
||||
|
||||
/* store whether call was unsuccessful due to resource limit and not due to impossible constraint */
|
||||
|
|
@ -2094,41 +2151,32 @@ int Abc_ExactDelayCost( word * pTruth, int nVars, int * pArrTimeProfile, char *
|
|||
return pArrTimeProfile[0];
|
||||
}
|
||||
|
||||
if ( s_pSesStore->fVeryVerbose )
|
||||
{
|
||||
printf( "arrival times input:" );
|
||||
for ( l = 0; l < nVars; ++l )
|
||||
printf( " %d", pArrTimeProfile[l] );
|
||||
printf( "\n" );
|
||||
}
|
||||
|
||||
for ( l = 0; l < nVars; ++l )
|
||||
pNormalArrTime[l] = pArrTimeProfile[l];
|
||||
|
||||
nDelta = Abc_NormalizeArrivalTimes( pNormalArrTime, nVars, &nMaxArrival );
|
||||
|
||||
if ( s_pSesStore->fVeryVerbose )
|
||||
{
|
||||
printf( "compute delay for nontrivial truth table " );
|
||||
Abc_TtPrintHexRev( stdout, pTruth, nVars );
|
||||
printf( " with arrival times" );
|
||||
for ( l = 0; l < nVars; ++l )
|
||||
printf( " %d", pNormalArrTime[l] );
|
||||
printf( " at level %d\n", AigLevel );
|
||||
}
|
||||
|
||||
*Cost = ABC_INFINITY;
|
||||
|
||||
if ( Ses_StoreGetEntry( s_pSesStore, pTruth, nVars, pNormalArrTime, &pSol ) )
|
||||
{
|
||||
if ( s_pSesStore->fVeryVerbose )
|
||||
printf( " truth table already in store\n" );
|
||||
|
||||
s_pSesStore->nCacheHits++;
|
||||
s_pSesStore->pCacheHits[nVars]++;
|
||||
}
|
||||
else
|
||||
{
|
||||
if ( s_pSesStore->fVeryVerbose )
|
||||
{
|
||||
printf( ANSI_COLOR_CYAN );
|
||||
Abc_TtPrintHexRev( stdout, pTruth, nVars );
|
||||
printf( ANSI_COLOR_RESET );
|
||||
printf( " [%d", pNormalArrTime[0] );
|
||||
for ( l = 1; l < nVars; ++l )
|
||||
printf( " %d", pNormalArrTime[l] );
|
||||
printf( "]@%d:", AigLevel );
|
||||
fflush( stdout );
|
||||
}
|
||||
|
||||
nMaxDepth = pNormalArrTime[0];
|
||||
for ( i = 1; i < nVars; ++i )
|
||||
nMaxDepth = Abc_MaxInt( nMaxDepth, pNormalArrTime[i] );
|
||||
|
|
@ -2141,19 +2189,23 @@ int Abc_ExactDelayCost( word * pTruth, int nVars, int * pArrTimeProfile, char *
|
|||
pSes = Ses_ManAlloc( pTruth, nVars, 1 /* nSpecFunc */, nMaxDepth, pNormalArrTime, s_pSesStore->fMakeAIG, s_pSesStore->nBTLimit, s_pSesStore->fVerbose );
|
||||
pSes->fVeryVerbose = s_pSesStore->fVeryVerbose;
|
||||
pSes->pSat = s_pSesStore->pSat;
|
||||
pSes->nStartGates = nVars - 2;
|
||||
|
||||
while ( pSes->nMaxDepth ) /* there is improvement */
|
||||
{
|
||||
if ( s_pSesStore->fVeryVerbose )
|
||||
{
|
||||
printf( " try to compute network starting with depth %d ", pSes->nMaxDepth );
|
||||
printf( " %d", pSes->nMaxDepth );
|
||||
fflush( stdout );
|
||||
}
|
||||
|
||||
if ( Ses_ManFindMinimumSize( pSes ) )
|
||||
{
|
||||
if ( s_pSesStore->fVeryVerbose )
|
||||
printf( " FOUND\n" );
|
||||
{
|
||||
if ( pSes->nMaxDepth >= 10 ) printf( "\b" );
|
||||
printf( "\b" ANSI_COLOR_GREEN "%d" ANSI_COLOR_RESET, pSes->nMaxDepth );
|
||||
}
|
||||
if ( pSol )
|
||||
ABC_FREE( pSol );
|
||||
pSol = Ses_ManExtractSolution( pSes );
|
||||
|
|
@ -2162,14 +2214,20 @@ int Abc_ExactDelayCost( word * pTruth, int nVars, int * pArrTimeProfile, char *
|
|||
else
|
||||
{
|
||||
if ( s_pSesStore->fVeryVerbose )
|
||||
printf( " NOT FOUND (%d)\n", pSes->fHitResLimit );
|
||||
{
|
||||
if ( pSes->nMaxDepth >= 10 ) printf( "\b" );
|
||||
printf( "\b%s%d" ANSI_COLOR_RESET, pSes->fHitResLimit ? ANSI_COLOR_RED : ANSI_COLOR_YELLOW, pSes->nMaxDepth );
|
||||
}
|
||||
break;
|
||||
}
|
||||
}
|
||||
|
||||
if ( s_pSesStore->fVeryVerbose )
|
||||
printf( "\n" );
|
||||
|
||||
/* log unsuccessful case for debugging */
|
||||
if ( s_pSesStore->pDebugEntries && pSes->fHitResLimit )
|
||||
Ses_StorePrintDebugEntry( s_pSesStore, pTruth, nVars, pNormalArrTime, pSes->nMaxDepth );
|
||||
Ses_StorePrintDebugEntry( s_pSesStore, pTruth, nVars, pNormalArrTime, pSes->nMaxDepth, pSol );
|
||||
|
||||
pSes->timeTotal = Abc_Clock() - timeStartExact;
|
||||
|
||||
|
|
|
|||
Loading…
Reference in New Issue