From 8ec44da3fbdba0d6fd4ee0eb74cc8e7648b78ece Mon Sep 17 00:00:00 2001 From: Mathias Soeken Date: Sun, 21 Aug 2016 18:13:57 +0200 Subject: More logging in exact synthesis. --- src/base/abci/abcExact.c | 166 +++++++++++++++++++++++++++++++---------------- 1 file changed, 110 insertions(+), 56 deletions(-) (limited to 'src') diff --git a/src/base/abci/abcExact.c b/src/base/abci/abcExact.c index 05c06051..db346835 100644 --- a/src/base/abci/abcExact.c +++ b/src/base/abci/abcExact.c @@ -25,7 +25,6 @@ #include "base/abc/abc.h" #include "aig/gia/gia.h" -#include "bool/kit/kit.h" #include "misc/util/utilTruth.h" #include "misc/vec/vecInt.h" #include "misc/vec/vecPtr.h" @@ -39,17 +38,6 @@ ABC_NAMESPACE_IMPL_START /// DECLARATIONS /// //////////////////////////////////////////////////////////////////////// -static word s_Truths8[32] = { - ABC_CONST(0xAAAAAAAAAAAAAAAA), ABC_CONST(0xAAAAAAAAAAAAAAAA), ABC_CONST(0xAAAAAAAAAAAAAAAA), ABC_CONST(0xAAAAAAAAAAAAAAAA), - ABC_CONST(0xCCCCCCCCCCCCCCCC), ABC_CONST(0xCCCCCCCCCCCCCCCC), ABC_CONST(0xCCCCCCCCCCCCCCCC), ABC_CONST(0xCCCCCCCCCCCCCCCC), - ABC_CONST(0xF0F0F0F0F0F0F0F0), ABC_CONST(0xF0F0F0F0F0F0F0F0), ABC_CONST(0xF0F0F0F0F0F0F0F0), ABC_CONST(0xF0F0F0F0F0F0F0F0), - ABC_CONST(0xFF00FF00FF00FF00), ABC_CONST(0xFF00FF00FF00FF00), ABC_CONST(0xFF00FF00FF00FF00), ABC_CONST(0xFF00FF00FF00FF00), - ABC_CONST(0xFFFF0000FFFF0000), ABC_CONST(0xFFFF0000FFFF0000), ABC_CONST(0xFFFF0000FFFF0000), ABC_CONST(0xFFFF0000FFFF0000), - ABC_CONST(0xFFFFFFFF00000000), ABC_CONST(0xFFFFFFFF00000000), ABC_CONST(0xFFFFFFFF00000000), ABC_CONST(0xFFFFFFFF00000000), - ABC_CONST(0x0000000000000000), ABC_CONST(0xFFFFFFFFFFFFFFFF), ABC_CONST(0x0000000000000000), ABC_CONST(0xFFFFFFFFFFFFFFFF), - ABC_CONST(0x0000000000000000), ABC_CONST(0x0000000000000000), ABC_CONST(0xFFFFFFFFFFFFFFFF), ABC_CONST(0xFFFFFFFFFFFFFFFF) -}; - #define ABC_EXACT_SOL_NVARS 0 #define ABC_EXACT_SOL_NFUNC 1 #define ABC_EXACT_SOL_NGATES 2 @@ -93,7 +81,13 @@ struct Ses_Man_t_ abctime timeSat; /* SAT runtime */ abctime timeSatSat; /* SAT runtime (sat instance) */ abctime timeSatUnsat; /* SAT runtime (unsat instance) */ + abctime timeSatUndef; /* SAT runtime (undef instance) */ + abctime timeInstance; /* creating instance runtime */ abctime timeTotal; /* all runtime */ + + int nSatCalls; /* number of SAT calls */ + int nUnsatCalls; /* number of UNSAT calls */ + int nUndefCalls; /* number of UNDEF calls */ }; /*********************************************************************** @@ -151,6 +145,18 @@ struct Ses_Store_t_ unsigned long pSynthesizedRL[9]; /* -> per cut size */ unsigned long nCacheHits; /* number of cache hits */ unsigned long pCacheHits[9]; /* -> per cut size */ + + unsigned long nSatCalls; /* number of total SAT calls */ + unsigned long nUnsatCalls; /* number of total UNSAT calls */ + unsigned long nUndefCalls; /* number of total UNDEF calls */ + + abctime timeExact; /* Exact synthesis runtime */ + abctime timeSat; /* SAT runtime */ + abctime timeSatSat; /* SAT runtime (sat instance) */ + abctime timeSatUnsat; /* SAT runtime (unsat instance) */ + abctime timeSatUndef; /* SAT runtime (undef instance) */ + abctime timeInstance; /* creating instance runtime */ + abctime timeTotal; /* all runtime */ }; static Ses_Store_t * s_pSesStore = NULL; @@ -183,14 +189,6 @@ static int Abc_NormalizeArrivalTimes( int * pArrTimeProfile, int nVars, int * ma return delta; } -static inline void Abc_UnnormalizeArrivalTimes( int * pArrTimeProfile, int nVars, int nDelta ) -{ - int l; - - for ( l = 0; l < nVars; ++l ) - pArrTimeProfile[l] += nDelta; -} - static inline Ses_Store_t * Ses_StoreAlloc( int nBTLimit, int fMakeAIG, int fVerbose ) { Ses_Store_t * pStore = ABC_CALLOC( Ses_Store_t, 1 ); @@ -623,7 +621,7 @@ static inline void Ses_ManCreateMainClause( Ses_Man_t * pSes, int t, int i, int if ( j < pSes->nSpecVars ) { - if ( Abc_TtGetBit( s_Truths8 + ( j << 2 ), t + 1 ) != b ) /* 1 in clause, we can omit the clause */ + if ( ( ( ( t + 1 ) & ( 1 << j ) ) ? 1 : 0 ) != b ) return; } else @@ -631,7 +629,7 @@ static inline void Ses_ManCreateMainClause( Ses_Man_t * pSes, int t, int i, int if ( k < pSes->nSpecVars ) { - if ( Abc_TtGetBit( s_Truths8 + ( k << 2 ), t + 1 ) != c ) /* 1 in clause, we can omit the clause */ + if ( ( ( ( t + 1 ) & ( 1 << k ) ) ? 1 : 0 ) != c ) return; } else @@ -883,16 +881,20 @@ static inline int Ses_ManSolve( Ses_Man_t * pSes ) if ( status == l_True ) { + pSes->nSatCalls++; pSes->timeSatSat += timeDelta; return 1; } else if ( status == l_False ) { + pSes->nUnsatCalls++; pSes->timeSatUnsat += timeDelta; return 0; } else { + pSes->nUndefCalls++; + pSes->timeSatUndef += timeDelta; if ( pSes->fSatVerbose ) { printf( "resource limit reached\n" ); @@ -1185,10 +1187,12 @@ static Gia_Man_t * Ses_ManExtractGia( char const * pSol ) static void Ses_ManPrintRuntime( Ses_Man_t * pSes ) { printf( "Runtime breakdown:\n" ); - ABC_PRTP( "Sat ", pSes->timeSat, pSes->timeTotal ); - ABC_PRTP( " Sat ", pSes->timeSatSat, pSes->timeTotal ); - ABC_PRTP( " Unsat", pSes->timeSatUnsat, pSes->timeTotal ); - ABC_PRTP( "ALL ", pSes->timeTotal, pSes->timeTotal ); + ABC_PRTP( "Sat ", pSes->timeSat, pSes->timeTotal ); + ABC_PRTP( " Sat ", pSes->timeSatSat, pSes->timeTotal ); + ABC_PRTP( " Unsat ", pSes->timeSatUnsat, pSes->timeTotal ); + ABC_PRTP( " Undef ", pSes->timeSatUndef, pSes->timeTotal ); + ABC_PRTP( "Instance", pSes->timeInstance, pSes->timeTotal ); + ABC_PRTP( "ALL ", pSes->timeTotal, pSes->timeTotal ); } static inline void Ses_ManPrintFuncs( Ses_Man_t * pSes ) @@ -1255,7 +1259,8 @@ static inline void Ses_ManPrintVars( Ses_Man_t * pSes ) ***********************************************************************/ static int Ses_ManFindMinimumSize( Ses_Man_t * pSes ) { - int nGates = 0; + int nGates = 0, f; + abctime timeStart; /* store whether call was unsuccessful due to resource limit and not due to impossible constraint */ pSes->fHitResLimit = 0; @@ -1280,8 +1285,11 @@ static int Ses_ManFindMinimumSize( Ses_Man_t * pSes ) return 0; } + timeStart = Abc_Clock(); Ses_ManCreateVars( pSes, nGates ); - if ( !Ses_ManCreateClauses( pSes ) ) + f = Ses_ManCreateClauses( pSes ); + pSes->timeInstance += ( Abc_Clock() - timeStart ); + if ( !f ) continue; /* proven UNSAT while creating clauses */ switch ( Ses_ManSolve( pSes ) ) @@ -1575,17 +1583,33 @@ void Abc_ExactStats() printf( "number of entries : %d\n", s_pSesStore->nEntriesCount ); printf( "number of valid entries : %d\n", s_pSesStore->nValidEntriesCount ); printf( "number of invalid entries : %d\n", s_pSesStore->nEntriesCount - s_pSesStore->nValidEntriesCount ); + printf( "-------------------------------------------------------------------------------------------------------------------------------\n" ); + printf( "number of SAT calls : %lu\n", s_pSesStore->nSatCalls ); + printf( "number of UNSAT calls : %lu\n", s_pSesStore->nUnsatCalls ); + printf( "number of UNDEF calls : %lu\n", s_pSesStore->nUndefCalls ); + + printf( "-------------------------------------------------------------------------------------------------------------------------------\n" ); + printf( "Runtime breakdown:\n" ); + ABC_PRTP( "Exact ", s_pSesStore->timeExact, s_pSesStore->timeTotal ); + ABC_PRTP( " Sat ", s_pSesStore->timeSat, s_pSesStore->timeTotal ); + ABC_PRTP( " Sat ", s_pSesStore->timeSatSat, s_pSesStore->timeTotal ); + ABC_PRTP( " Unsat ", s_pSesStore->timeSatUnsat, s_pSesStore->timeTotal ); + ABC_PRTP( " Undef ", s_pSesStore->timeSatUndef, s_pSesStore->timeTotal ); + ABC_PRTP( " Instance", s_pSesStore->timeInstance, s_pSesStore->timeTotal ); + ABC_PRTP( "Other ", s_pSesStore->timeTotal - s_pSesStore->timeExact, s_pSesStore->timeTotal ); + ABC_PRTP( "ALL ", s_pSesStore->timeTotal, s_pSesStore->timeTotal ); } // 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; + int i, nMaxArrival, l; Ses_Man_t * pSes = NULL; char * pSol = NULL, * p; + int pNormalArrTime[8]; int Delay = ABC_INFINITY, nMaxDepth; - abctime timeStart; + abctime timeStart = Abc_Clock(), timeStartExact; /* some checks */ if ( nVars < 0 || nVars > 8 ) @@ -1604,6 +1628,7 @@ int Abc_ExactDelayCost( word * pTruth, int nVars, int * pArrTimeProfile, char * s_pSesStore->pSynthesizedTrivial[0]++; *Cost = 0; + s_pSesStore->timeTotal += ( Abc_Clock() - timeStart ); return 0; } @@ -1614,6 +1639,7 @@ int Abc_ExactDelayCost( word * pTruth, int nVars, int * pArrTimeProfile, char * *Cost = 0; pPerm[0] = (char)0; + s_pSesStore->timeTotal += ( Abc_Clock() - timeStart ); return pArrTimeProfile[0]; } @@ -1625,7 +1651,10 @@ int Abc_ExactDelayCost( word * pTruth, int nVars, int * pArrTimeProfile, char * printf( "\n" ); } - nDelta = Abc_NormalizeArrivalTimes( pArrTimeProfile, nVars, &nMaxArrival ); + for ( l = 0; l < nVars; ++l ) + pNormalArrTime[l] = pArrTimeProfile[l]; + + Abc_NormalizeArrivalTimes( pNormalArrTime, nVars, &nMaxArrival ); if ( s_pSesStore->fVeryVerbose ) { @@ -1633,13 +1662,13 @@ int Abc_ExactDelayCost( word * pTruth, int nVars, int * pArrTimeProfile, char * Abc_TtPrintHexRev( stdout, pTruth, nVars ); printf( " with arrival times" ); for ( l = 0; l < nVars; ++l ) - printf( " %d", pArrTimeProfile[l] ); - printf( " at level %d (nDelta = %d)\n", AigLevel, nDelta ); + printf( " %d", pNormalArrTime[l] ); + printf( " at level %d\n", AigLevel ); } *Cost = ABC_INFINITY; - if ( Ses_StoreGetEntry( s_pSesStore, pTruth, nVars, pArrTimeProfile, &pSol ) ) + if ( Ses_StoreGetEntry( s_pSesStore, pTruth, nVars, pNormalArrTime, &pSol ) ) { if ( s_pSesStore->fVeryVerbose ) printf( " truth table already in store\n" ); @@ -1649,16 +1678,16 @@ int Abc_ExactDelayCost( word * pTruth, int nVars, int * pArrTimeProfile, char * } else { - nMaxDepth = pArrTimeProfile[0]; + nMaxDepth = pNormalArrTime[0]; for ( i = 1; i < nVars; ++i ) - nMaxDepth = Abc_MaxInt( nMaxDepth, pArrTimeProfile[i] ); + nMaxDepth = Abc_MaxInt( nMaxDepth, pNormalArrTime[i] ); nMaxDepth += nVars + 1; if ( AigLevel != -1 ) nMaxDepth = Abc_MinInt( AigLevel, nMaxDepth + nVars + 1 ); - timeStart = Abc_Clock(); + timeStartExact = Abc_Clock(); - pSes = Ses_ManAlloc( pTruth, nVars, 1 /* nSpecFunc */, nMaxDepth, pArrTimeProfile, s_pSesStore->fMakeAIG, s_pSesStore->nBTLimit, s_pSesStore->fVerbose ); + pSes = Ses_ManAlloc( pTruth, nVars, 1 /* nSpecFunc */, nMaxDepth, pNormalArrTime, s_pSesStore->fMakeAIG, s_pSesStore->nBTLimit, s_pSesStore->fVerbose ); pSes->fVeryVerbose = s_pSesStore->fVeryVerbose; while ( pSes->nMaxDepth ) /* there is improvement */ @@ -1686,6 +1715,9 @@ int Abc_ExactDelayCost( word * pTruth, int nVars, int * pArrTimeProfile, char * } } + pSes->timeTotal = Abc_Clock() - timeStartExact; + + /* statistics */ if ( pSol ) { if ( pSes->fHitResLimit ) @@ -1713,13 +1745,22 @@ int Abc_ExactDelayCost( word * pTruth, int nVars, int * pArrTimeProfile, char * } } - pSes->timeTotal = Abc_Clock() - timeStart; + s_pSesStore->nSatCalls += pSes->nSatCalls; + s_pSesStore->nUnsatCalls += pSes->nUnsatCalls; + s_pSesStore->nUndefCalls += pSes->nUndefCalls; + + s_pSesStore->timeSat += pSes->timeSat; + s_pSesStore->timeSatSat += pSes->timeSatSat; + s_pSesStore->timeSatUnsat += pSes->timeSatUnsat; + s_pSesStore->timeSatUndef += pSes->timeSatUndef; + s_pSesStore->timeInstance += pSes->timeInstance; + s_pSesStore->timeExact += pSes->timeTotal; /* cleanup */ Ses_ManClean( pSes ); /* store solution */ - Ses_StoreAddEntry( s_pSesStore, pTruth, nVars, pArrTimeProfile, pSol ); + Ses_StoreAddEntry( s_pSesStore, pTruth, nVars, pNormalArrTime, pSol ); } if ( pSol ) @@ -1740,45 +1781,57 @@ int Abc_ExactDelayCost( word * pTruth, int nVars, int * pArrTimeProfile, char * 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 ( Delay != Delay2 ) + //{ + // printf( "^--- BUG!\n" ); + // assert( 0 ); + //} + + s_pSesStore->timeTotal += ( Abc_Clock() - timeStart ); + return Delay2; } - - Abc_UnnormalizeArrivalTimes( pArrTimeProfile, nVars, nDelta ); - - if ( !pSol ) + else { assert( *Cost == ABC_INFINITY ); - } - return pSol ? nDelta + Delay : ABC_INFINITY; + s_pSesStore->timeTotal += ( Abc_Clock() - timeStart ); + return ABC_INFINITY; + } } // this procedure returns a new node whose output in terms of the given fanins // 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 = NULL; - int i, j, nDelta, nMaxArrival; + int i, j, nMaxArrival; + int pNormalArrTime[8]; char const * p; Abc_Obj_t * pObj; Vec_Ptr_t * pGates; char pGateTruth[5]; char * pSopCover; + abctime timeStart = Abc_Clock(); if ( nVars == 0 ) + { + s_pSesStore->timeTotal += ( Abc_Clock() - timeStart ); return (pTruth[0] & 1) ? Abc_NtkCreateNodeConst1(pNtk) : Abc_NtkCreateNodeConst0(pNtk); + } if ( nVars == 1 ) + { + s_pSesStore->timeTotal += ( Abc_Clock() - timeStart ); return (pTruth[0] & 1) ? Abc_NtkCreateNodeInv(pNtk, pFanins[0]) : Abc_NtkCreateNodeBuf(pNtk, pFanins[0]); + } - nDelta = Abc_NormalizeArrivalTimes( pArrTimeProfile, nVars, &nMaxArrival ); - Ses_StoreGetEntry( s_pSesStore, pTruth, nVars, pArrTimeProfile, &pSol ); - Abc_UnnormalizeArrivalTimes( pArrTimeProfile, nVars, nDelta ); + for ( i = 0; i < nVars; ++i ) + pNormalArrTime[i] = pArrTimeProfile[i]; + Abc_NormalizeArrivalTimes( pNormalArrTime, nVars, &nMaxArrival ); + Ses_StoreGetEntry( s_pSesStore, pTruth, nVars, pNormalArrTime, &pSol ); if ( !pSol ) + { + s_pSesStore->timeTotal += ( Abc_Clock() - timeStart ); return NULL; + } assert( pSol[ABC_EXACT_SOL_NVARS] == nVars ); assert( pSol[ABC_EXACT_SOL_NFUNC] == 1 ); @@ -1827,6 +1880,7 @@ Abc_Obj_t * Abc_ExactBuildNode( word * pTruth, int nVars, int * pArrTimeProfile, Vec_PtrFree( pGates ); + s_pSesStore->timeTotal += ( Abc_Clock() - timeStart ); return pObj; } -- cgit v1.2.3