From 33c6d01291433cb3cb6560856280dd3a9cb8fb58 Mon Sep 17 00:00:00 2001 From: Mathias Soeken Date: Tue, 2 Aug 2016 13:24:21 +0200 Subject: Tests and bug fixes for exact store manager. --- src/base/abci/abc.c | 4 ++- src/base/abci/abcExact.c | 76 ++++++++++++++++++++++++++++++------------------ 2 files changed, 50 insertions(+), 30 deletions(-) (limited to 'src') diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c index 6138013e..d49db050 100644 --- a/src/base/abci/abc.c +++ b/src/base/abci/abc.c @@ -7325,10 +7325,12 @@ int Abc_CommandExact( Abc_Frame_t * pAbc, int argc, char ** argv ) if ( fTest ) { - extern void Abc_ExactTest(); + extern void Abc_ExactTest( int fVerbose ); + extern void Abc_ExactStoreTest( int fVerbose ); printf( "run test suite, ignore all other settings\n" ); Abc_ExactTest( fVerbose ); + Abc_ExactStoreTest( fVerbose ); return 0; } diff --git a/src/base/abci/abcExact.c b/src/base/abci/abcExact.c index ae5e9944..94325f4a 100644 --- a/src/base/abci/abcExact.c +++ b/src/base/abci/abcExact.c @@ -120,6 +120,8 @@ struct Ses_TruthEntry_t_ typedef struct Ses_Store_t_ Ses_Store_t; 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 */ }; @@ -153,9 +155,11 @@ static int Abc_NormalizeArrivalTimes( int * pArrTimeProfile, int nVars, int * ma return delta; } -static inline Ses_Store_t * Ses_StoreAlloc() +static inline Ses_Store_t * Ses_StoreAlloc( int nBTLimit, int fVerbose ) { Ses_Store_t * pStore = ABC_CALLOC( Ses_Store_t, 1 ); + pStore->fVerbose = fVerbose; + pStore->nBTLimit = nBTLimit; memset( pStore->pEntries, 0, SES_STORE_TABLE_SIZE ); return pStore; @@ -823,25 +827,30 @@ static char * Ses_ManExtractSolution( Ses_Man_t * pSes ) *p++ = nOp; *p++ = 2; + if ( pSes->fVeryVerbose ) + 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 ) + printf( " and operands %d and %d", j, k ); *p++ = j; *p++ = k; break; } - /* if ( pSes->fVeryVerbose ) */ - /* { */ - /* if ( pSes->nMaxDepth > 0 ) */ - /* { */ - /* printf( " and depth vector " ); */ - /* for ( j = 0; j <= pSes->nArrTimeMax + i; ++j ) */ - /* printf( "%d", sat_solver_var_value( pSes->pSat, Ses_ManDepthVar( pSes, i, j ) ) ); */ - /* } */ - /* printf( "\n" ); */ - /* } */ + if ( pSes->fVeryVerbose ) + { + if ( pSes->nMaxDepth > 0 ) + { + printf( " and depth vector " ); + for ( j = 0; j <= pSes->nArrTimeMax + i; ++j ) + printf( "%d", sat_solver_var_value( pSes->pSat, Ses_ManDepthVar( pSes, i, j ) ) ); + } + printf( "\n" ); + } } /* pin-to-pin delay */ @@ -852,18 +861,18 @@ static char * Ses_ManExtractSolution( Ses_Man_t * pSes ) { /* since all gates are binary for now */ j = pSol[3 + i * 4 + 2]; - k = pSol[3 + i * 4 + 2]; + k = pSol[3 + i * 4 + 3]; for ( l = 0; l < pSes->nSpecVars; ++l ) { /* pin-to-pin delay to input l of child nodes */ - aj = j < pSes->nGates ? 0 : pPerm[j * pSes->nSpecVars + l]; - ak = k < pSes->nGates ? 0 : pPerm[k * pSes->nSpecVars + l]; + aj = j < pSes->nSpecVars ? 0 : pPerm[(j - pSes->nSpecVars) * pSes->nSpecVars + l]; + ak = k < pSes->nSpecVars ? 0 : pPerm[(k - pSes->nSpecVars) * pSes->nSpecVars + l]; if ( aj == 0 && ak == 0 ) - pPerm[i * pSes->nSpecVars + l] = 0; + pPerm[i * pSes->nSpecVars + l] = ( l == j || l == k ) ? 1 : 0; else - pPerm[i * pSes->nSpecVars + l] = ( ( aj > ak ) ? aj : ak ) + 1; + pPerm[i * pSes->nSpecVars + l] = Abc_MaxInt( aj, ak ) + 1; } } } @@ -879,10 +888,15 @@ static char * Ses_ManExtractSolution( Ses_Man_t * pSes ) while ( d < pSes->nArrTimeMax + i && sat_solver_var_value( pSes->pSat, Ses_ManDepthVar( pSes, i, d ) ) ) ++d; *p++ = d + pSes->nArrTimeDelta; - for ( l = 0; l < pSes->nSpecVars; ++l ) - *p++ = ( pSes->nMaxDepth != -1 ) ? pPerm[i * pSes->nSpecVars + l] : 0; if ( pSes->fVeryVerbose ) printf( "output %d points to %d and has normalized delay %d\n", h, i, d ); + for ( l = 0; l < pSes->nSpecVars; ++l ) + { + d = ( pSes->nMaxDepth != -1 ) ? pPerm[i * pSes->nSpecVars + l] : 0; + if ( pSes->fVeryVerbose ) + printf( " pin-to-pin arrival time from input %d is %d\n", l, d ); + *p++ = d; + } } /* pin-to-pin delays */ @@ -1336,10 +1350,10 @@ int Abc_ExactInputNum() return 8; } // start exact store manager -void Abc_ExactStart() +void Abc_ExactStart( int nBTLimit, int fVerbose ) { if ( !s_pSesStore ) - s_pSesStore = Ses_StoreAlloc(); + s_pSesStore = Ses_StoreAlloc( nBTLimit, fVerbose ); else printf( "exact store manager already started\n" ); } @@ -1367,17 +1381,15 @@ int Abc_ExactDelayCost( word * pTruth, int nVars, int * pArrTimeProfile, char * nMaxDepth = pArrTimeProfile[0]; for ( i = 1; i < nVars; ++i ) - if ( pArrTimeProfile[i] > nMaxDepth ) - nMaxDepth = pArrTimeProfile[i]; - nMaxDepth += nVars + 1; - if ( AigLevel < nMaxDepth ) - nMaxDepth = AigLevel; + nMaxDepth = Abc_MaxInt( nMaxDepth, pArrTimeProfile[i] ); + nMaxDepth = Abc_MinInt( AigLevel, nMaxDepth + nVars + 1 ); timeStart = Abc_Clock(); *Cost = ABC_INFINITY; - pSes = Ses_ManAlloc( pTruth, nVars, 1 /* fSpecFunc */, nMaxDepth, pArrTimeProfile, 1 /* fMakeAIG */, 0 ); + pSes = Ses_ManAlloc( pTruth, nVars, 1 /* fSpecFunc */, nMaxDepth, pArrTimeProfile, 1 /* fMakeAIG */, s_pSesStore->fVerbose ); + pSes->nBTLimit = s_pSesStore->nBTLimit; while ( 1 ) /* there is improvement */ { @@ -1396,7 +1408,7 @@ int Abc_ExactDelayCost( word * pTruth, int nVars, int * pArrTimeProfile, char * if ( pSol ) { *Cost = pSol[ABC_EXACT_SOL_NGATES]; - p = pSol + 3 + 4 * ABC_EXACT_SOL_NGATES + 1; + p = pSol + 3 + 4 * pSol[ABC_EXACT_SOL_NGATES] + 1; Delay = *p++; for ( l = 0; l < nVars; ++l ) pPerm[l] = *p++; @@ -1501,11 +1513,17 @@ void Abc_ExactStoreTest( int fVerbose ) } Abc_NodeFreeNames( vNames ); - Abc_ExactStart(); + Abc_ExactStart( 10000, fVerbose ); assert( !Abc_ExactBuildNode( pTruth, 4, pArrTimeProfile, pFanins ) ); - printf( "%d\n", Abc_ExactDelayCost( pTruth, 4, pArrTimeProfile, pPerm, &Cost, 12 ) ); + assert( Abc_ExactDelayCost( pTruth, 4, pArrTimeProfile, pPerm, &Cost, 12 ) == 1 ); + + assert( Abc_ExactBuildNode( pTruth, 4, pArrTimeProfile, pFanins ) ); + + (*pArrTimeProfile)++; + assert( !Abc_ExactBuildNode( pTruth, 4, pArrTimeProfile, pFanins ) ); + (*pArrTimeProfile)--; Abc_ExactStop(); } -- cgit v1.2.3