From 95d2ab9c17e94daa1bc53a254f4533eac1e49b79 Mon Sep 17 00:00:00 2001 From: Mathias Soeken Date: Mon, 8 Aug 2016 12:59:21 +0200 Subject: Improvements in exact synthesis. --- src/base/abci/abc.c | 14 +++-- src/base/abci/abcExact.c | 135 +++++++++++++++++++++++++++-------------------- 2 files changed, 86 insertions(+), 63 deletions(-) (limited to 'src/base/abci') diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c index 31f3a275..471e6eef 100644 --- a/src/base/abci/abc.c +++ b/src/base/abci/abc.c @@ -7417,13 +7417,13 @@ usage: int Abc_CommandBmsStart( Abc_Frame_t * pAbc, int argc, char ** argv ) { extern int Abc_ExactIsRunning(); - extern void Abc_ExactStart( int nBTLimit, int fMakeAIG, int fVerbose, const char *pFilename ); + extern void Abc_ExactStart( int nBTLimit, int fMakeAIG, int fVerbose, int fVeryVerbose, const char *pFilename ); - int c, fMakeAIG = 0, fVerbose = 0, nBTLimit = 10000; + int c, fMakeAIG = 0, fVerbose = 0, fVeryVerbose = 0, nBTLimit = 100; char * pFilename = NULL; Extra_UtilGetoptReset(); - while ( ( c = Extra_UtilGetopt( argc, argv, "Cavh" ) ) != EOF ) + while ( ( c = Extra_UtilGetopt( argc, argv, "Cavwh" ) ) != EOF ) { switch ( c ) { @@ -7442,6 +7442,9 @@ int Abc_CommandBmsStart( Abc_Frame_t * pAbc, int argc, char ** argv ) case 'v': fVerbose ^= 1; break; + case 'w': + fVeryVerbose ^= 1; + break; case 'h': goto usage; default: @@ -7460,16 +7463,17 @@ int Abc_CommandBmsStart( Abc_Frame_t * pAbc, int argc, char ** argv ) return 1; } - Abc_ExactStart( nBTLimit, fMakeAIG, fVerbose, pFilename ); + Abc_ExactStart( nBTLimit, fMakeAIG, fVerbose, fVeryVerbose, pFilename ); return 0; usage: - Abc_Print( -2, "usage: bms_start [-C ] [-avh] []\n" ); + Abc_Print( -2, "usage: bms_start [-C ] [-avwh] []\n" ); Abc_Print( -2, "\t starts BMS manager for recording optimum networks\n" ); Abc_Print( -2, "\t if is specified, store entries are read from that file\n" ); Abc_Print( -2, "\t-C : 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-v : toggle verbose printout [default = %s]\n", fVerbose ? "yes" : "no" ); + Abc_Print( -2, "\t-w : toggle very verbose printout [default = %s]\n", fVeryVerbose ? "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" ); diff --git a/src/base/abci/abcExact.c b/src/base/abci/abcExact.c index 19b0188a..7d968b70 100644 --- a/src/base/abci/abcExact.c +++ b/src/base/abci/abcExact.c @@ -72,6 +72,8 @@ struct Ses_Man_t_ int fMakeAIG; /* create AIG instead of general network */ int fVerbose; /* be verbose */ int fVeryVerbose; /* be very verbose */ + int fExtractVerbose; /* be verbose about solution extraction */ + int fSatVerbose; /* be verbose about SAT solving */ int nGates; /* number of gates */ @@ -126,8 +128,10 @@ struct Ses_Store_t_ { int fMakeAIG; /* create AIG instead of general network */ int fVerbose; /* be verbose */ + int fVeryVerbose; /* be very verbose */ int nBTLimit; /* conflict limit */ int nEntriesCount; /* number of entries */ + int nValidEntriesCount; /* number of entries with network */ Ses_TruthEntry_t * pEntries[SES_STORE_TABLE_SIZE]; /* hash table for truth table entries */ unsigned long nCutCount; @@ -266,7 +270,7 @@ static inline void Ses_StoreTimesCopy( int * pTimesDest, int * pTimesSrc, int nV pTimesDest[i] = pTimesSrc[i]; } -// pArrTimeProfile is not normalized +// pArrTimeProfile is normalized // returns 1 if and only if a new TimesEntry has been created int Ses_StoreAddEntry( Ses_Store_t * pStore, word * pTruth, int nVars, int * pArrTimeProfile, char * pSol ) { @@ -317,6 +321,8 @@ int Ses_StoreAddEntry( Ses_Store_t * pStore, word * pTruth, int nVars, int * pAr /* item has been added */ fAdded = 1; pStore->nEntriesCount++; + if ( pSol ) + pStore->nValidEntriesCount++; } else /* item was already present */ @@ -325,9 +331,9 @@ int Ses_StoreAddEntry( Ses_Store_t * pStore, word * pTruth, int nVars, int * pAr return fAdded; } -// pArrTimeProfile is not normalized -// returns 0 if no solution was found -char * Ses_StoreGetEntry( Ses_Store_t * pStore, word * pTruth, int nVars, int * pArrTimeProfile ) +// pArrTimeProfile is normalized +// returns 1 if entry was in store, pSol may still be 0 if it couldn't be computed +int Ses_StoreGetEntry( Ses_Store_t * pStore, word * pTruth, int nVars, int * pArrTimeProfile, char ** pSol ) { int key; Ses_TruthEntry_t * pTEntry; @@ -363,7 +369,8 @@ char * Ses_StoreGetEntry( Ses_Store_t * pStore, word * pTruth, int nVars, int * if ( !pTiEntry ) return 0; - return pTiEntry->pNetwork; + *pSol = pTiEntry->pNetwork; + return 1; } static void Ses_StoreWrite( Ses_Store_t * pStore, const char * pFilename ) @@ -380,7 +387,7 @@ static void Ses_StoreWrite( Ses_Store_t * pStore, const char * pFilename ) return; } - fwrite( &pStore->nEntriesCount, sizeof( int ), 1, pFile ); + fwrite( &pStore->nValidEntriesCount, sizeof( int ), 1, pFile ); for ( i = 0; i < SES_STORE_TABLE_SIZE; ++i ) if ( pStore->pEntries[i] ) @@ -392,10 +399,13 @@ static void Ses_StoreWrite( Ses_Store_t * pStore, const char * pFilename ) pTiEntry = pTEntry->head; while ( pTiEntry ) { - fwrite( pTEntry->pTruth, sizeof( word ), 4, pFile ); - fwrite( &pTEntry->nVars, sizeof( int ), 1, pFile ); - fwrite( pTiEntry->pArrTimeProfile, sizeof( int ), 8, pFile ); - fwrite( pTiEntry->pNetwork, sizeof( char ), 3 + 4 * pTiEntry->pNetwork[ABC_EXACT_SOL_NGATES] + 2 + pTiEntry->pNetwork[ABC_EXACT_SOL_NVARS], pFile ); + if ( pTiEntry->pNetwork ) + { + fwrite( pTEntry->pTruth, sizeof( word ), 4, pFile ); + fwrite( &pTEntry->nVars, sizeof( int ), 1, pFile ); + fwrite( pTiEntry->pArrTimeProfile, sizeof( int ), 8, pFile ); + fwrite( pTiEntry->pNetwork, sizeof( char ), 3 + 4 * pTiEntry->pNetwork[ABC_EXACT_SOL_NGATES] + 2 + pTiEntry->pNetwork[ABC_EXACT_SOL_NVARS], pFile ); + } pTiEntry = pTiEntry->next; } pTEntry = pTEntry->next; @@ -560,7 +570,7 @@ static void Ses_ManCreateVars( Ses_Man_t * pSes, int nGates ) { int i; - if ( pSes->fVerbose ) + if ( pSes->fSatVerbose ) { printf( "create variables for network with %d functions over %d variables and %d gates\n", pSes->nSpecFunc, pSes->nSpecVars, nGates ); } @@ -846,7 +856,7 @@ static inline int Ses_ManSolve( Ses_Man_t * pSes ) int status; abctime timeStart, timeDelta; - if ( pSes->fVeryVerbose ) + if ( pSes->fSatVerbose ) { printf( "solve SAT instance with %d clauses and %d variables\n", sat_solver_nclauses( pSes->pSat ), sat_solver_nvars( pSes->pSat ) ); } @@ -869,7 +879,7 @@ static inline int Ses_ManSolve( Ses_Man_t * pSes ) } else { - if ( pSes->fVerbose ) + if ( pSes->fSatVerbose ) { printf( "resource limit reached\n" ); } @@ -923,21 +933,21 @@ static char * Ses_ManExtractSolution( Ses_Man_t * pSes ) *p++ = nOp; *p++ = 2; - if ( pSes->fVeryVerbose ) + if ( pSes->fExtractVerbose ) printf( "add gate %d with operation %d", pSes->nSpecVars + i, nOp ); for ( k = 0; k < pSes->nSpecVars + i; ++k ) for ( j = 0; j < k; ++j ) if ( sat_solver_var_value( pSes->pSat, Ses_ManSelectVar( pSes, i, j, k ) ) ) { - if ( pSes->fVeryVerbose ) + if ( pSes->fExtractVerbose ) printf( " and operands %d and %d", j, k ); *p++ = j; *p++ = k; break; } - if ( pSes->fVeryVerbose ) + if ( pSes->fExtractVerbose ) { if ( pSes->nMaxDepth > 0 ) { @@ -986,12 +996,12 @@ static char * Ses_ManExtractSolution( Ses_Man_t * pSes ) for ( l = 0; l < pSes->nSpecVars; ++l ) d = Abc_MaxInt( d, pSes->pArrTimeProfile[l] + pPerm[i * pSes->nSpecVars + l] ); *p++ = d; - if ( pSes->fVeryVerbose ) + if ( pSes->fExtractVerbose ) printf( "output %d points to %d and has normalized delay %d (nArrTimeDelta = %d)\n", h, i, d, pSes->nArrTimeDelta ); for ( l = 0; l < pSes->nSpecVars; ++l ) { d = ( pSes->nMaxDepth != -1 ) ? pPerm[i * pSes->nSpecVars + l] : 0; - if ( pSes->fVeryVerbose ) + if ( pSes->fExtractVerbose ) printf( " pin-to-pin arrival time from input %d is %d (pArrTimeProfile = %d)\n", l, d, pSes->pArrTimeProfile[l] ); *p++ = d; } @@ -1449,11 +1459,12 @@ int Abc_ExactInputNum() return 8; } // start exact store manager -void Abc_ExactStart( int nBTLimit, int fMakeAIG, int fVerbose, const char * pFilename ) +void Abc_ExactStart( int nBTLimit, int fMakeAIG, int fVerbose, int fVeryVerbose, const char * pFilename ) { if ( !s_pSesStore ) { s_pSesStore = Ses_StoreAlloc( nBTLimit, fMakeAIG, fVerbose ); + s_pSesStore->fVeryVerbose = fVeryVerbose; if ( pFilename ) Ses_StoreRead( s_pSesStore, pFilename ); } @@ -1489,13 +1500,14 @@ void Abc_ExactStats() printf( " total = %lu\n", s_pSesStore->nCutCount ); printf( "cache hits : %lu\n", s_pSesStore->nCacheHit ); printf( "number of entries : %d\n", s_pSesStore->nEntriesCount ); + printf( "number of valid entries : %d\n", s_pSesStore->nValidEntriesCount ); } // 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, nDelta, nMaxArrival, l, fExists = 0; + int i, nDelta, nMaxArrival, l; Ses_Man_t * pSes = NULL; char * pSol = NULL, * p; int Delay = ABC_INFINITY, nMaxDepth; @@ -1523,60 +1535,74 @@ int Abc_ExactDelayCost( word * pTruth, int nVars, int * pArrTimeProfile, char * nDelta = Abc_NormalizeArrivalTimes( pArrTimeProfile, nVars, &nMaxArrival ); - if ( s_pSesStore->fVerbose ) + 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", pArrTimeProfile[l] ); - printf( "\n" ); + printf( " at level %d\n", AigLevel ); } /* statistics */ s_pSesStore->nCutCount++; s_pSesStore->pCutCount[nVars]++; - pSol = Ses_StoreGetEntry( s_pSesStore, pTruth, nVars, pArrTimeProfile ); - if ( pSol ) + *Cost = ABC_INFINITY; + + if ( Ses_StoreGetEntry( s_pSesStore, pTruth, nVars, pArrTimeProfile, &pSol ) ) { - if ( s_pSesStore->fVerbose ) + if ( s_pSesStore->fVeryVerbose ) printf( " truth table already in store\n" ); 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 ); + nMaxDepth += nVars + 1; + //nMaxDepth = Abc_MinInt( AigLevel, nMaxDepth + nVars + 1 ); timeStart = Abc_Clock(); - *Cost = ABC_INFINITY; - - pSes = Ses_ManAlloc( pTruth, nVars, 1 /* fSpecFunc */, nMaxDepth, pArrTimeProfile, s_pSesStore->fMakeAIG, s_pSesStore->fVerbose ); + pSes = Ses_ManAlloc( pTruth, nVars, 1 /* nSpecFunc */, nMaxDepth, pArrTimeProfile, s_pSesStore->fMakeAIG, s_pSesStore->fVerbose ); pSes->nBTLimit = s_pSesStore->nBTLimit; - pSes->fVeryVerbose = 0; + pSes->fVeryVerbose = s_pSesStore->fVeryVerbose; - while ( 1 ) /* there is improvement */ + while ( pSes->nMaxDepth ) /* there is improvement */ { + if ( s_pSesStore->fVeryVerbose ) + { + printf( " try to compute network starting with depth %d ", pSes->nMaxDepth ); + fflush( stdout ); + } + if ( Ses_ManFindMinimumSize( pSes ) ) { + if ( s_pSesStore->fVeryVerbose ) + printf( " FOUND\n" ); if ( pSol ) ABC_FREE( pSol ); pSol = Ses_ManExtractSolution( pSes ); pSes->nMaxDepth--; } else + { + if ( s_pSesStore->fVeryVerbose ) + printf( " NOT FOUND\n" ); break; + } } pSes->timeTotal = Abc_Clock() - timeStart; /* cleanup */ Ses_ManClean( pSes ); + + /* store solution */ + Ses_StoreAddEntry( s_pSesStore, pTruth, nVars, pArrTimeProfile, pSol ); } if ( pSol ) @@ -1586,31 +1612,24 @@ int Abc_ExactDelayCost( word * pTruth, int nVars, int * pArrTimeProfile, char * Delay = *p++; for ( l = 0; l < nVars; ++l ) pPerm[l] = *p++; - - /* store solution */ - if ( !fExists ) - Ses_StoreAddEntry( s_pSesStore, pTruth, nVars, pArrTimeProfile, pSol ); } - //for ( l = 0; l < nVars; ++l ) - // printf( "pArrTimeProfile[%d] = %d\n", l, pArrTimeProfile[l] ); - - if ( pSol ) - { - int Delay2 = 0; - for ( l = 0; l < nVars; ++l ) - { - //printf( "%d ", pPerm[l] ); - Delay2 = Abc_MaxInt( Delay2, pArrTimeProfile[l] + pPerm[l] ); - } - //printf( " output arrival = %d recomputed = %d\n", Delay, Delay2 ); - if ( Delay != Delay2 ) - { - printf( "^--- BUG!\n" ); - assert( 0 ); - } - //Delay = Delay2; - } + /* if ( pSol ) */ + /* { */ + /* int Delay2 = 0; */ + /* for ( l = 0; l < nVars; ++l ) */ + /* { */ + /* //printf( "%d ", pPerm[l] ); */ + /* Delay2 = Abc_MaxInt( Delay2, pArrTimeProfile[l] + pPerm[l] ); */ + /* } */ + /* //printf( " output arrival = %d recomputed = %d\n", Delay, Delay2 ); */ + /* if ( Delay != Delay2 ) */ + /* { */ + /* printf( "^--- BUG!\n" ); */ + /* assert( 0 ); */ + /* } */ + /* //Delay = Delay2; */ + /* } */ Abc_UnnormalizeArrivalTimes( pArrTimeProfile, nVars, nDelta ); @@ -1620,7 +1639,7 @@ int Abc_ExactDelayCost( word * pTruth, int nVars, int * pArrTimeProfile, char * // has the smallest possible arrival time (in agreement with the above Abc_ExactDelayCost) Abc_Obj_t * Abc_ExactBuildNode( word * pTruth, int nVars, int * pArrTimeProfile, Abc_Obj_t ** pFanins, Abc_Ntk_t * pNtk ) { - char * pSol; + char * pSol = NULL; int i, j, nDelta, nMaxArrival; char const * p; Abc_Obj_t * pObj; @@ -1634,7 +1653,7 @@ Abc_Obj_t * Abc_ExactBuildNode( word * pTruth, int nVars, int * pArrTimeProfile, return (pTruth[0] & 1) ? Abc_NtkCreateNodeInv(pNtk, pFanins[0]) : Abc_NtkCreateNodeBuf(pNtk, pFanins[0]); nDelta = Abc_NormalizeArrivalTimes( pArrTimeProfile, nVars, &nMaxArrival ); - pSol = Ses_StoreGetEntry( s_pSesStore, pTruth, nVars, pArrTimeProfile ); + Ses_StoreGetEntry( s_pSesStore, pTruth, nVars, pArrTimeProfile, &pSol ); Abc_UnnormalizeArrivalTimes( pArrTimeProfile, nVars, nDelta ); if ( !pSol ) return NULL; @@ -1711,7 +1730,7 @@ void Abc_ExactStoreTest( int fVerbose ) } Abc_NodeFreeNames( vNames ); - Abc_ExactStart( 10000, 1, fVerbose, NULL ); + Abc_ExactStart( 10000, 1, fVerbose, 0, NULL ); assert( !Abc_ExactBuildNode( pTruth, 4, pArrTimeProfile, pFanins, pNtk ) ); -- cgit v1.2.3