diff options
Diffstat (limited to 'src/base/abci')
| -rw-r--r-- | src/base/abci/abc.c | 125 | ||||
| -rw-r--r-- | src/base/abci/abcExact.c | 126 |
2 files changed, 209 insertions, 42 deletions
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c index d49db050..e4e78d08 100644 --- a/src/base/abci/abc.c +++ b/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; } } diff --git a/src/base/abci/abcExact.c b/src/base/abci/abcExact.c index 847c2465..c9a4def4 100644 --- a/src/base/abci/abcExact.c +++ b/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 ); |