diff options
author | Alan Mishchenko <alanmi@berkeley.edu> | 2014-09-18 11:46:14 -0700 |
---|---|---|
committer | Alan Mishchenko <alanmi@berkeley.edu> | 2014-09-18 11:46:14 -0700 |
commit | 043cfcd775d067eadc400b7af40347e170a3774b (patch) | |
tree | 1647cd5ad61b95dd391a2c523e383a87e35d14ef | |
parent | 023e92c4700283d4de6e60c5b5054c2d2452b98f (diff) | |
download | abc-043cfcd775d067eadc400b7af40347e170a3774b.tar.gz abc-043cfcd775d067eadc400b7af40347e170a3774b.tar.bz2 abc-043cfcd775d067eadc400b7af40347e170a3774b.zip |
Concurrency for Boolean matching.
-rw-r--r-- | src/aig/gia/giaKf.c | 12 | ||||
-rw-r--r-- | src/base/abci/abc.c | 56 | ||||
-rw-r--r-- | src/base/cmd/cmdStarter.c | 2 | ||||
-rw-r--r-- | src/base/wlc/wlcReadVer.c | 2 | ||||
-rw-r--r-- | src/map/if/if.h | 2 | ||||
-rw-r--r-- | src/map/if/ifDsd.c | 222 | ||||
-rw-r--r-- | src/map/if/ifTest.c | 12 | ||||
-rw-r--r-- | src/map/if/ifTune.c | 74 | ||||
-rw-r--r-- | src/proof/abs/absPth.c | 2 | ||||
-rw-r--r-- | src/proof/cec/cecSplit.c | 12 |
10 files changed, 331 insertions, 65 deletions
diff --git a/src/aig/gia/giaKf.c b/src/aig/gia/giaKf.c index 083bf95c..caa88bfc 100644 --- a/src/aig/gia/giaKf.c +++ b/src/aig/gia/giaKf.c @@ -21,7 +21,7 @@ #include "gia.h" #include "misc/vec/vecSet.h" -//#ifdef ABC_USE_PTHREADS +#ifdef ABC_USE_PTHREADS #ifdef _WIN32 #include "../lib/pthread.h" @@ -30,7 +30,7 @@ #include <unistd.h> #endif -//#endif +#endif ABC_NAMESPACE_IMPL_START @@ -38,6 +38,13 @@ ABC_NAMESPACE_IMPL_START /// DECLARATIONS /// //////////////////////////////////////////////////////////////////////// +#ifndef ABC_USE_PTHREADS + +void Kf_ManSetDefaultPars( Jf_Par_t * pPars ) {} +Gia_Man_t * Kf_ManPerformMapping( Gia_Man_t * pGia, Jf_Par_t * pPars ) { return NULL; } + +#else // pthreads are used + #define KF_LEAF_MAX 16 #define KF_CUT_MAX 32 #define KF_PROC_MAX 32 @@ -1328,6 +1335,7 @@ Gia_Man_t * Kf_ManPerformMapping( Gia_Man_t * pGia, Jf_Par_t * pPars ) /// END OF FILE /// //////////////////////////////////////////////////////////////////////// +#endif // pthreads are used ABC_NAMESPACE_IMPL_END diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c index 091b3b88..c39eea0a 100644 --- a/src/base/abci/abc.c +++ b/src/base/abci/abc.c @@ -15489,7 +15489,14 @@ int Abc_CommandIf( Abc_Frame_t * pAbc, int argc, char ** argv ) return 0; } if ( p == NULL ) + { + if ( LutSize > DAU_MAX_VAR || pPars->nLutSize > DAU_MAX_VAR ) + { + printf( "Size of required DSD manager (%d) exceeds the precompiled limit (%d) (change parameter DAU_MAX_VAR).\n", LutSize, DAU_MAX_VAR ); + return 0; + } Abc_FrameSetManDsd( If_DsdManAlloc(pPars->nLutSize, LutSize) ); + } } if ( pPars->fUserRecLib ) @@ -15913,7 +15920,7 @@ int Abc_CommandDsdFree( Abc_Frame_t * pAbc, int argc, char ** argv ) { if ( !Abc_FrameReadManDsd2() ) { - Abc_Print( 1, "The DSD manager is not started.\n" ); + Abc_Print( -1, "The DSD manager is not started.\n" ); return 0; } Abc_FrameSetManDsd2( NULL ); @@ -15922,7 +15929,7 @@ int Abc_CommandDsdFree( Abc_Frame_t * pAbc, int argc, char ** argv ) { if ( !Abc_FrameReadManDsd() ) { - Abc_Print( 1, "The DSD manager is not started.\n" ); + Abc_Print( -1, "The DSD manager is not started.\n" ); return 0; } Abc_FrameSetManDsd( NULL ); @@ -16000,7 +16007,7 @@ int Abc_CommandDsdPs( Abc_Frame_t * pAbc, int argc, char ** argv ) { if ( !Abc_FrameReadManDsd2() ) { - Abc_Print( 1, "The DSD manager is not started.\n" ); + Abc_Print( -1, "The DSD manager is not started.\n" ); return 0; } If_DsdManPrint( (If_DsdMan_t *)Abc_FrameReadManDsd2(), NULL, Number, Support, fOccurs, fTtDump, fVerbose ); @@ -16009,7 +16016,7 @@ int Abc_CommandDsdPs( Abc_Frame_t * pAbc, int argc, char ** argv ) { if ( !Abc_FrameReadManDsd() ) { - Abc_Print( 1, "The DSD manager is not started.\n" ); + Abc_Print( -1, "The DSD manager is not started.\n" ); return 0; } If_DsdManPrint( (If_DsdMan_t *)Abc_FrameReadManDsd(), NULL, Number, Support, fOccurs, fTtDump, fVerbose ); @@ -16043,10 +16050,10 @@ usage: int Abc_CommandDsdTune( Abc_Frame_t * pAbc, int argc, char ** argv ) { char * pStruct = NULL; - int c, fVerbose = 0, fFast = 0, fAdd = 0, fSpec = 0, LutSize = 0, nConfls = 10000; + int c, fVerbose = 0, fFast = 0, fAdd = 0, fSpec = 0, LutSize = 0, nConfls = 10000, nProcs = 1; If_DsdMan_t * pDsdMan = (If_DsdMan_t *)Abc_FrameReadManDsd(); Extra_UtilGetoptReset(); - while ( ( c = Extra_UtilGetopt( argc, argv, "KCSfasvh" ) ) != EOF ) + while ( ( c = Extra_UtilGetopt( argc, argv, "KCPSfasvh" ) ) != EOF ) { switch ( c ) { @@ -16070,6 +16077,15 @@ int Abc_CommandDsdTune( Abc_Frame_t * pAbc, int argc, char ** argv ) nConfls = atoi(argv[globalUtilOptind]); globalUtilOptind++; break; + case 'P': + if ( globalUtilOptind >= argc ) + { + Abc_Print( -1, "Command line switch \"-P\" should be followed by a floating point number.\n" ); + goto usage; + } + nProcs = atoi(argv[globalUtilOptind]); + globalUtilOptind++; + break; case 'S': if ( globalUtilOptind >= argc ) { @@ -16099,20 +16115,21 @@ int Abc_CommandDsdTune( Abc_Frame_t * pAbc, int argc, char ** argv ) } if ( !Abc_FrameReadManDsd() ) { - Abc_Print( 1, "The DSD manager is not started.\n" ); + Abc_Print( -1, "The DSD manager is not started.\n" ); return 0; } if ( pStruct ) - Id_DsdManTuneStr( pDsdMan, pStruct, nConfls, fVerbose ); + Id_DsdManTuneStr( pDsdMan, pStruct, nConfls, nProcs, fVerbose ); else If_DsdManTune( pDsdMan, LutSize, fFast, fAdd, fSpec, fVerbose ); return 0; usage: - Abc_Print( -2, "usage: dsd_tune [-KC num] [-fasvh] [-S str]\n" ); + Abc_Print( -2, "usage: dsd_tune [-KCP num] [-fasvh] [-S str]\n" ); Abc_Print( -2, "\t tunes DSD manager for the given LUT size\n" ); Abc_Print( -2, "\t-K num : LUT size used for tuning [default = %d]\n", LutSize ); Abc_Print( -2, "\t-C num : the maximum number of conflicts [default = %d]\n", nConfls ); + Abc_Print( -2, "\t-P num : the maximum number of processes [default = %d]\n", nProcs ); Abc_Print( -2, "\t-f : toggles using fast check [default = %s]\n", fFast? "yes": "no" ); Abc_Print( -2, "\t-a : toggles adding tuning to the current one [default = %s]\n", fAdd? "yes": "no" ); Abc_Print( -2, "\t-s : toggles using specialized check [default = %s]\n", fSpec? "yes": "no" ); @@ -16153,7 +16170,7 @@ int Abc_CommandDsdMerge( Abc_Frame_t * pAbc, int argc, char ** argv ) } if ( !Abc_FrameReadManDsd() ) { - Abc_Print( 1, "The DSD manager is not started.\n" ); + Abc_Print( -1, "The DSD manager is not started.\n" ); return 0; } pArgvNew = argv + globalUtilOptind; @@ -16223,7 +16240,7 @@ int Abc_CommandDsdClean( Abc_Frame_t * pAbc, int argc, char ** argv ) } if ( !Abc_FrameReadManDsd() ) { - Abc_Print( 1, "The DSD manager is not started.\n" ); + Abc_Print( -1, "The DSD manager is not started.\n" ); return 0; } If_DsdManClean( (If_DsdMan_t *)Abc_FrameReadManDsd(), fVerbose ); @@ -30804,6 +30821,16 @@ int Abc_CommandAbc9Dsdb( Abc_Frame_t * pAbc, int argc, char ** argv ) Abc_Print( -1, "Abc_CommandAbc9Dsdb(): There is no AIG.\n" ); return 1; } + if ( nLutSize > DAU_MAX_VAR ) + { + printf( "Abc_CommandAbc9Dsdb(): Size of the required DSD manager (%d) exceeds the precompiled limit (%d) (change parameter DAU_MAX_VAR).\n", nLutSize, DAU_MAX_VAR ); + return 0; + } + if ( Abc_FrameReadManDsd2() && nLutSize > If_DsdManVarNum(Abc_FrameReadManDsd2()) ) + { + printf( "Abc_CommandAbc9Dsdb(): Incompatible size of the DSD manager (run \"dsd_free -b\").\n" ); + return 0; + } if ( nLevelMax || nTimeWindow ) pTemp = Gia_ManPerformDsdBalanceWin( pAbc->pGia, nLevelMax, nTimeWindow, nLutSize, nCutNum, nRelaxRatio, fVerbose ); else @@ -31329,7 +31356,14 @@ int Abc_CommandAbc9If( Abc_Frame_t * pAbc, int argc, char ** argv ) return 0; } if ( p == NULL ) + { + if ( LutSize > DAU_MAX_VAR || pPars->nLutSize > DAU_MAX_VAR ) + { + printf( "Size of required DSD manager (%d) exceeds the precompiled limit (%d) (change parameter DAU_MAX_VAR).\n", LutSize, DAU_MAX_VAR ); + return 0; + } Abc_FrameSetManDsd( If_DsdManAlloc(pPars->nLutSize, LutSize) ); + } } if ( pPars->fUserRecLib ) diff --git a/src/base/cmd/cmdStarter.c b/src/base/cmd/cmdStarter.c index 16810baa..47cdd9ed 100644 --- a/src/base/cmd/cmdStarter.c +++ b/src/base/cmd/cmdStarter.c @@ -248,7 +248,7 @@ void Cmd_RunStarter( char * pFileName, char * pBinary, char * pCommand, int nCor fflush( stdout ); } -#endif +#endif // pthreads are used //////////////////////////////////////////////////////////////////////// /// END OF FILE /// diff --git a/src/base/wlc/wlcReadVer.c b/src/base/wlc/wlcReadVer.c index 34197e1b..32375ac0 100644 --- a/src/base/wlc/wlcReadVer.c +++ b/src/base/wlc/wlcReadVer.c @@ -134,7 +134,7 @@ int Wlc_PrsWriteErrorMessage( Wlc_Prs_t * p, char * pCur, const char * format, . break; sprintf( p->sError, "%s (line %d): %s\n", p->pFileName, iLine+1, pMessage ); } - free( pMessage ); + ABC_FREE( pMessage ); return 0; } void Wlc_PrsPrintErrorMessage( Wlc_Prs_t * p ) diff --git a/src/map/if/if.h b/src/map/if/if.h index 0f217d20..1d5dec16 100644 --- a/src/map/if/if.h +++ b/src/map/if/if.h @@ -539,7 +539,7 @@ extern If_DsdMan_t * If_DsdManAlloc( int nVars, int nLutSize ); extern void If_DsdManAllocIsops( If_DsdMan_t * p, int nLutSize ); extern void If_DsdManPrint( If_DsdMan_t * p, char * pFileName, int Number, int Support, int fOccurs, int fTtDump, int fVerbose ); extern void If_DsdManTune( If_DsdMan_t * p, int LutSize, int fFast, int fAdd, int fSpec, int fVerbose ); -extern void Id_DsdManTuneStr( If_DsdMan_t * p, char * pStruct, int nConfls, int fVerbose ); +extern void Id_DsdManTuneStr( If_DsdMan_t * p, char * pStruct, int nConfls, int nProcs, int fVerbose ); extern void If_DsdManFree( If_DsdMan_t * p, int fVerbose ); extern void If_DsdManSave( If_DsdMan_t * p, char * pFileName ); extern If_DsdMan_t * If_DsdManLoad( char * pFileName ); diff --git a/src/map/if/ifDsd.c b/src/map/if/ifDsd.c index d6d0f801..a8224d63 100644 --- a/src/map/if/ifDsd.c +++ b/src/map/if/ifDsd.c @@ -26,6 +26,17 @@ #include "aig/gia/gia.h" #include "bool/kit/kit.h" +#ifdef ABC_USE_PTHREADS + +#ifdef _WIN32 +#include "../lib/pthread.h" +#else +#include <pthread.h> +#include <unistd.h> +#endif + +#endif + ABC_NAMESPACE_IMPL_START @@ -206,6 +217,7 @@ If_DsdMan_t * If_DsdManAlloc( int nVars, int LutSize ) { If_DsdMan_t * p; int v; char pFileName[10]; + assert( nVars <= DAU_MAX_VAR ); sprintf( pFileName, "%02d.dsd", nVars ); p = ABC_CALLOC( If_DsdMan_t, 1 ); p->pStore = Abc_UtilStrsav( pFileName ); @@ -1213,10 +1225,9 @@ void If_DsdManComputeTruth_rec( If_DsdMan_t * p, int iDsd, word * pRes, unsigned assert( 0 ); } -word * If_DsdManComputeTruth( If_DsdMan_t * p, int iDsd, unsigned char * pPermLits ) +void If_DsdManComputeTruthPtr( If_DsdMan_t * p, int iDsd, unsigned char * pPermLits, word * pRes ) { int nSupp = 0; - word * pRes = p->pTtElems[DAU_MAX_VAR]; If_DsdObj_t * pObj = If_DsdVecObj( &p->vObjs, Abc_Lit2Var(iDsd) ); if ( iDsd == 0 ) Abc_TtConst0( pRes, p->nWords ); @@ -1231,6 +1242,11 @@ word * If_DsdManComputeTruth( If_DsdMan_t * p, int iDsd, unsigned char * pPermLi else If_DsdManComputeTruth_rec( p, iDsd, pRes, pPermLits, &nSupp ); assert( nSupp == If_DsdVecLitSuppSize(&p->vObjs, iDsd) ); +} +word * If_DsdManComputeTruth( If_DsdMan_t * p, int iDsd, unsigned char * pPermLits ) +{ + word * pRes = p->pTtElems[DAU_MAX_VAR]; + If_DsdManComputeTruthPtr( p, iDsd, pPermLits, pRes ); return pRes; } @@ -2259,6 +2275,7 @@ extern Ifn_Ntk_t * Ifn_NtkParse( char * pStr ); extern int Ifn_NtkMatch( Ifn_Ntk_t * p, word * pTruth, int nVars, int nConfls, int fVerbose, int fVeryVerbose ); extern void Ifn_NtkPrint( Ifn_Ntk_t * p ); extern int Ifn_NtkLutSizeMax( Ifn_Ntk_t * p ); +extern int Ifn_NtkInputNum( Ifn_Ntk_t * p ); /**Function************************************************************* @@ -2271,7 +2288,7 @@ extern int Ifn_NtkLutSizeMax( Ifn_Ntk_t * p ); SeeAlso [] ***********************************************************************/ -void Id_DsdManTuneStr( If_DsdMan_t * p, char * pStruct, int nConfls, int fVerbose ) +void Id_DsdManTuneStr1( If_DsdMan_t * p, char * pStruct, int nConfls, int fVerbose ) { int fVeryVerbose = 0; ProgressBar * pProgress = NULL; @@ -2281,6 +2298,14 @@ void Id_DsdManTuneStr( If_DsdMan_t * p, char * pStruct, int nConfls, int fVerbos abctime clk = Abc_Clock(); // parse the structure Ifn_Ntk_t * pNtk = Ifn_NtkParse( pStruct ); + if ( If_DsdManVarNum(p) > Ifn_NtkInputNum(pNtk) ) + { + printf( "The support of DSD manager (%d) exceeds the support of the structure (%d).\n", If_DsdManVarNum(p), Ifn_NtkInputNum(pNtk) ); + ABC_FREE( pNtk ); + return; + } + if ( If_DsdManVarNum(p) < Ifn_NtkInputNum(pNtk) ) + printf( "Warning: The support of DSD manager (%d) is less than the support of the structure (%d).\n", If_DsdManVarNum(p), Ifn_NtkInputNum(pNtk) ); LutSize = Ifn_NtkLutSizeMax(pNtk); // print if ( fVerbose ) @@ -2316,8 +2341,199 @@ void Id_DsdManTuneStr( If_DsdMan_t * p, char * pStruct, int nConfls, int fVerbos Abc_PrintTime( 1, "Time", Abc_Clock() - clk ); if ( fVeryVerbose ) If_DsdManPrintDistrib( p ); + ABC_FREE( pNtk ); +} + + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +#ifndef ABC_USE_PTHREADS +void Id_DsdManTuneStr( If_DsdMan_t * p, char * pStruct, int nConfls, int nProcs, int fVerbose ) +{ + Id_DsdManTuneStr1( p, pStruct, nConfls, fVerbose ); +} +#else // pthreads are used + + +#define PAR_THR_MAX 100 +typedef struct Ifn_ThData_t_ +{ + Ifn_Ntk_t * pNtk; // network + word pTruth[DAU_MAX_WORD]; + int nVars; // support + int Id; // object + int nConfls; // conflicts + int Result; // result + int Status; // state + abctime clkUsed; // total runtime +} Ifn_ThData_t; +void * Ifn_WorkerThread( void * pArg ) +{ + Ifn_ThData_t * pThData = (Ifn_ThData_t *)pArg; + volatile int * pPlace = &pThData->Status; + abctime clk; + while ( 1 ) + { + while ( *pPlace == 0 ); + assert( pThData->Status == 1 ); + if ( pThData->Id == -1 ) + { + pthread_exit( NULL ); + assert( 0 ); + return NULL; + } + clk = Abc_Clock(); + pThData->Result = Ifn_NtkMatch( pThData->pNtk, pThData->pTruth, pThData->nVars, pThData->nConfls, 0, 0 ); + pThData->clkUsed += Abc_Clock() - clk; + pThData->Status = 0; +// printf( "Finished object %d\n", pThData->Id ); + } + assert( 0 ); + return NULL; +} +void Id_DsdManTuneStr( If_DsdMan_t * p, char * pStruct, int nConfls, int nProcs, int fVerbose ) +{ + int fVeryVerbose = 0; + ProgressBar * pProgress = NULL; + int i, k, nVars, LutSize; + abctime clk = Abc_Clock(); + Ifn_Ntk_t * pNtk; + If_DsdObj_t * pObj; + if ( nProcs == 1 ) + { + Id_DsdManTuneStr1( p, pStruct, nConfls, fVerbose ); + return; + } + if ( nProcs > PAR_THR_MAX ) + { + printf( "The number of processes (%d) exceeds the precompiled limit (%d).\n", nProcs, PAR_THR_MAX ); + return; + } + // parse the structure + pNtk = Ifn_NtkParse( pStruct ); + if ( pNtk == NULL ) + return; + if ( If_DsdManVarNum(p) > Ifn_NtkInputNum(pNtk) ) + { + printf( "The support of DSD manager (%d) exceeds the support of the structure (%d).\n", If_DsdManVarNum(p), Ifn_NtkInputNum(pNtk) ); + ABC_FREE( pNtk ); + return; + } + if ( If_DsdManVarNum(p) < Ifn_NtkInputNum(pNtk) ) + printf( "Warning: The support of DSD manager (%d) is less than the support of the structure (%d).\n", If_DsdManVarNum(p), Ifn_NtkInputNum(pNtk) ); + // check the largest LUT + LutSize = Ifn_NtkLutSizeMax(pNtk); + if ( fVerbose ) + { + printf( "Considering programmable cell: " ); + Ifn_NtkPrint( pNtk ); + printf( "Largest LUT size = %d.\n", LutSize ); + } + ABC_FREE( pNtk ); + // clean the attributes + If_DsdVecForEachObj( &p->vObjs, pObj, i ) + pObj->fMark = 0; + pProgress = Extra_ProgressBarStart( stdout, Vec_PtrSize(&p->vObjs) ); + + // perform concurrent solving + { + pthread_t WorkerThread[PAR_THR_MAX]; + Ifn_ThData_t ThData[PAR_THR_MAX]; + abctime clk, clkUsed = 0; + int status, fRunning = 1, iCurrentObj = 0; + // start the threads + for ( i = 0; i < nProcs; i++ ) + { + ThData[i].pNtk = Ifn_NtkParse( pStruct ); + ThData[i].nVars = -1; // support + ThData[i].Id = -1; // object + ThData[i].nConfls = nConfls; // conflicts + ThData[i].Result = -1; // result + ThData[i].Status = 0; // state + ThData[i].clkUsed = 0; // total runtime + status = pthread_create( WorkerThread + i, NULL, Ifn_WorkerThread, (void *)(ThData + i) ); assert( status == 0 ); + } + // run the threads + while ( fRunning || iCurrentObj < Vec_PtrSize(&p->vObjs) ) + { + for ( i = 0; i < nProcs; i++ ) + { + if ( ThData[i].Status ) + continue; + assert( ThData[i].Status == 0 ); + if ( ThData[i].Id >= 0 ) + { + //printf( "Closing obj %d with Thread %d:\n", ThData[i].Id, i ); + assert( ThData[i].Result == 0 || ThData[i].Result == 1 ); + if ( ThData[i].Result == 1 ) + If_DsdVecObjSetMark( &p->vObjs, ThData[i].Id ); + ThData[i].Id = -1; + ThData[i].Result = -1; + } + for ( k = iCurrentObj; k < Vec_PtrSize(&p->vObjs); k++ ) + { + if ( (k & 0x3FF) == 0 ) + Extra_ProgressBarUpdate( pProgress, k, NULL ); + pObj = If_DsdVecObj( &p->vObjs, k ); + nVars = If_DsdObjSuppSize(pObj); + if ( nVars <= LutSize ) + continue; + clk = Abc_Clock(); + If_DsdManComputeTruthPtr( p, Abc_Var2Lit(k, 0), NULL, ThData[i].pTruth ); + clkUsed += Abc_Clock() - clk; + ThData[i].nVars = nVars; + ThData[i].Id = k; + ThData[i].Result = -1; + ThData[i].Status = 1; + //printf( "Scheduling %d for Thread %d\n", ThData[i].Id, i ); + iCurrentObj = k+1; + break; + } + } + fRunning = 0; + for ( i = 0; i < nProcs; i++ ) + if ( ThData[i].Status == 1 || (ThData[i].Status == 0 && ThData[i].Id >= 0) ) + fRunning = 1; + //printf( "fRunning %d\n", fRunning ); + } + // stop the threads + for ( i = 0; i < nProcs; i++ ) + { + assert( ThData[i].Status == 0 ); + ThData[i].Id = -1; + ThData[i].Status = 1; + ABC_FREE( ThData[i].pNtk ); + } + if ( fVerbose ) + { + printf( "Main : " ); + Abc_PrintTime( 1, "Time", clkUsed ); + for ( i = 0; i < nProcs; i++ ) + { + printf( "Thread %d : ", i ); + Abc_PrintTime( 1, "Time", ThData[i].clkUsed ); + } + } + } + + Extra_ProgressBarStop( pProgress ); + printf( "Finished matching %d functions. ", Vec_PtrSize(&p->vObjs) ); + Abc_PrintTime( 1, "Time", Abc_Clock() - clk ); + if ( fVeryVerbose ) + If_DsdManPrintDistrib( p ); } +#endif // pthreads are used + //////////////////////////////////////////////////////////////////////// /// END OF FILE /// //////////////////////////////////////////////////////////////////////// diff --git a/src/map/if/ifTest.c b/src/map/if/ifTest.c index bbadaca2..fa9a6444 100644 --- a/src/map/if/ifTest.c +++ b/src/map/if/ifTest.c @@ -21,7 +21,7 @@ #include "if.h" #include "aig/gia/gia.h" -//#ifdef ABC_USE_PTHREADS +#ifdef ABC_USE_PTHREADS #ifdef _WIN32 #include "../lib/pthread.h" @@ -30,7 +30,7 @@ #include <unistd.h> #endif -//#endif +#endif ABC_NAMESPACE_IMPL_START @@ -38,6 +38,12 @@ ABC_NAMESPACE_IMPL_START /// DECLARATIONS /// //////////////////////////////////////////////////////////////////////// +#ifndef ABC_USE_PTHREADS + +// do nothing + +#else // pthreads are used + static inline word * Gia_ParTestObj( Gia_Man_t * p, int Id ) { return (word *)p->pData + Id * p->iData; } static inline void Gia_ParTestAlloc( Gia_Man_t * p, int nWords ) { assert( !p->pData ); p->pData = (unsigned *)ABC_ALLOC(word, Gia_ManObjNum(p) * nWords); p->iData = nWords; } static inline void Gia_ParTestFree( Gia_Man_t * p ) { ABC_FREE( p->pData ); p->iData = 0; } @@ -339,6 +345,8 @@ void Gia_ParTest( Gia_Man_t * p, int nWords, int nProcs ) /// END OF FILE /// //////////////////////////////////////////////////////////////////////// +#endif // pthreads are used + ABC_NAMESPACE_IMPL_END diff --git a/src/map/if/ifTune.c b/src/map/if/ifTune.c index 817b0a2e..7dc7f75f 100644 --- a/src/map/if/ifTune.c +++ b/src/map/if/ifTune.c @@ -166,6 +166,10 @@ int Ifn_NtkLutSizeMax( Ifn_Ntk_t * p ) LutSize = Abc_MaxInt( LutSize, (int)p->Nodes[i].nFanins ); return LutSize; } +int Ifn_NtkInputNum( Ifn_Ntk_t * p ) +{ + return p->nInps; +} /**Function************************************************************* @@ -240,18 +244,24 @@ int Ifn_ManStrCheck( char * pStr, int * pnInps, int * pnObjs ) *pnObjs = MaxDef; return 1; } -Ifn_Ntk_t * Ifn_NtkParse( char * pStr ) +int Ifn_ErrorMessage( const char * format, ... ) +{ + char * pMessage; + va_list args; + va_start( args, format ); + pMessage = vnsprintf( format, args ); + va_end( args ); + printf( "%s", pMessage ); + ABC_FREE( pMessage ); + return 0; +} +int Ifn_NtkParseInt( char * pStr, Ifn_Ntk_t * p ) { int i, k, n, f, nFans, iFan; - static Ifn_Ntk_t P, * p = &P; - memset( p, 0, sizeof(Ifn_Ntk_t) ); if ( !Ifn_ManStrCheck(pStr, &p->nInps, &p->nObjs) ) - return NULL; + return 0; if ( p->nInps > IFN_INS ) - { - printf( "The number of variables (%d) exceeds predefined limit (%d). Recompile with different value of IFN_INS.\n", p->nInps, IFN_INS ); - return NULL; - } + return Ifn_ErrorMessage( "The number of variables (%d) exceeds predefined limit (%d). Recompile with different value of IFN_INS.\n", p->nInps, IFN_INS ); assert( p->nInps > 1 && p->nInps < p->nObjs && p->nInps <= IFN_INS && p->nObjs < 2*IFN_INS ); for ( i = p->nInps; i < p->nObjs; i++ ) { @@ -260,10 +270,7 @@ Ifn_Ntk_t * Ifn_NtkParse( char * pStr ) if ( pStr[k] == 'a' + i && pStr[k+1] == '=' ) break; if ( pStr[k] == 0 ) - { - printf( "Cannot find definition of signal %c.\n", 'a' + i ); - return NULL; - } + return Ifn_ErrorMessage( "Cannot find definition of signal %c.\n", 'a' + i ); if ( pStr[k+2] == '(' ) p->Nodes[i].Type = IF_DSD_AND, Next = ')'; else if ( pStr[k+2] == '[' ) @@ -273,32 +280,20 @@ Ifn_Ntk_t * Ifn_NtkParse( char * pStr ) else if ( pStr[k+2] == '{' ) p->Nodes[i].Type = IF_DSD_PRIME, Next = '}'; else - { - printf( "Cannot find openning operation symbol in the defition of of signal %c.\n", 'a' + i ); - return NULL; - } + return Ifn_ErrorMessage( "Cannot find openning operation symbol in the defition of of signal %c.\n", 'a' + i ); for ( n = k + 3; pStr[n]; n++ ) if ( pStr[n] == Next ) break; if ( pStr[n] == 0 ) - { - printf( "Cannot find closing operation symbol in the defition of of signal %c.\n", 'a' + i ); - return NULL; - } + return Ifn_ErrorMessage( "Cannot find closing operation symbol in the defition of of signal %c.\n", 'a' + i ); nFans = n - k - 3; if ( nFans < 1 || nFans > 8 ) - { - printf( "Cannot find matching operation symbol in the defition of of signal %c.\n", 'a' + i ); - return NULL; - } + return Ifn_ErrorMessage( "Cannot find matching operation symbol in the defition of of signal %c.\n", 'a' + i ); for ( f = 0; f < nFans; f++ ) { iFan = pStr[k + 3 + f] - 'a'; if ( iFan < 0 || iFan >= i ) - { - printf( "Fanin number %d is signal %d is out of range.\n", f, 'a' + i ); - return NULL; - } + return Ifn_ErrorMessage( "Fanin number %d is signal %d is out of range.\n", f, 'a' + i ); p->Nodes[i].Fanins[f] = iFan; } p->Nodes[i].nFanins = nFans; @@ -316,19 +311,15 @@ Ifn_Ntk_t * Ifn_NtkParse( char * pStr ) } // if ( p->nConstr ) // printf( "Total constraints = %d\n", p->nConstr ); - -/* - // constraints - p->nConstr = 5; - p->pConstr[0] = (0 << 16) | 1; - - p->pConstr[1] = (2 << 16) | 3; - p->pConstr[2] = (3 << 16) | 4; - - p->pConstr[3] = (6 << 16) | 7; - p->pConstr[4] = (7 << 16) | 8; -*/ - return p; + return 1; +} +Ifn_Ntk_t * Ifn_NtkParse( char * pStr ) +{ + Ifn_Ntk_t * p = ABC_CALLOC( Ifn_Ntk_t, 1 ); + if ( Ifn_NtkParseInt( pStr, p ) ) + return p; + ABC_FREE( p ); + return NULL; } /**Function************************************************************* @@ -805,6 +796,7 @@ void Ifn_NtkRead() Dau_DsdPrintFromTruth( pTruth, nVars ); // get the given function RetValue = Ifn_NtkMatch( p, pTruth, nVars, 0, 1, 1 ); + ABC_FREE( p ); } //////////////////////////////////////////////////////////////////////// diff --git a/src/proof/abs/absPth.c b/src/proof/abs/absPth.c index bd3f2dcb..f04a20d1 100644 --- a/src/proof/abs/absPth.c +++ b/src/proof/abs/absPth.c @@ -194,7 +194,7 @@ int Gia_GlaProveCheck( int fVerbose ) return 1; } -#endif +#endif // pthreads are used //////////////////////////////////////////////////////////////////////// /// END OF FILE /// diff --git a/src/proof/cec/cecSplit.c b/src/proof/cec/cecSplit.c index e5e9a9a4..0984c234 100644 --- a/src/proof/cec/cecSplit.c +++ b/src/proof/cec/cecSplit.c @@ -26,7 +26,7 @@ #include "misc/util/utilTruth.h" //#include "bdd/cudd/cuddInt.h" -//#ifdef ABC_USE_PTHREADS +#ifdef ABC_USE_PTHREADS #ifdef _WIN32 #include "../lib/pthread.h" @@ -35,7 +35,7 @@ #include <unistd.h> #endif -//#endif +#endif ABC_NAMESPACE_IMPL_START @@ -44,6 +44,12 @@ ABC_NAMESPACE_IMPL_START /// DECLARATIONS /// //////////////////////////////////////////////////////////////////////// +#ifndef ABC_USE_PTHREADS + +int Cec_GiaSplitTest( Gia_Man_t * p, int nProcs, int nTimeOut, int nIterMax, int LookAhead, int fVerbose, int fVeryVerbose ) { return -1; } + +#else // pthreads are used + //////////////////////////////////////////////////////////////////////// /// FUNCTION DEFINITIONS /// //////////////////////////////////////////////////////////////////////// @@ -822,6 +828,8 @@ void Cec_GiaPrintCofStats2( Gia_Man_t * p ) } } +#endif // pthreads are used + //////////////////////////////////////////////////////////////////////// /// END OF FILE /// //////////////////////////////////////////////////////////////////////// |