diff options
author | Alan Mishchenko <alanmi@berkeley.edu> | 2013-10-02 22:58:23 -0700 |
---|---|---|
committer | Alan Mishchenko <alanmi@berkeley.edu> | 2013-10-02 22:58:23 -0700 |
commit | cfa7be1a07e3102195b2395f379f50e556dbf4e3 (patch) | |
tree | a53bddabc1d9554eae9d03cb6f6363c5edd2d478 /src | |
parent | 38e577f5dfeb30379c0f97c246b4cc9428ba3db3 (diff) | |
download | abc-cfa7be1a07e3102195b2395f379f50e556dbf4e3.tar.gz abc-cfa7be1a07e3102195b2395f379f50e556dbf4e3.tar.bz2 abc-cfa7be1a07e3102195b2395f379f50e556dbf4e3.zip |
Integrating synthesis into the new BMC engine.
Diffstat (limited to 'src')
-rw-r--r-- | src/aig/gia/giaBalance.c | 54 | ||||
-rw-r--r-- | src/base/abci/abc.c | 9 | ||||
-rw-r--r-- | src/opt/dau/dau.h | 2 | ||||
-rw-r--r-- | src/opt/dau/dauGia.c | 19 | ||||
-rw-r--r-- | src/sat/bmc/bmc.h | 1 | ||||
-rw-r--r-- | src/sat/bmc/bmcBmcAnd.c | 7 |
6 files changed, 78 insertions, 14 deletions
diff --git a/src/aig/gia/giaBalance.c b/src/aig/gia/giaBalance.c index cdf36e7a..5855fc3d 100644 --- a/src/aig/gia/giaBalance.c +++ b/src/aig/gia/giaBalance.c @@ -36,13 +36,14 @@ struct Dam_Man_t_ { Gia_Man_t * pGia; // user's AIG Vec_Int_t * vNod2Set; // node ID into fanin set - Vec_Int_t * vDiv2Nod; // div ID into fanin set - Vec_Int_t * vSetStore; // stored multisets - Vec_Int_t * vNodStore; // stored divisors + Vec_Int_t * vDiv2Nod; // div ID into root node set + Vec_Int_t * vSetStore; // fanin set storage + Vec_Int_t * vNodStore; // root node set storage Vec_Flt_t * vCounts; // occur counts Vec_Int_t * vNodLevR; // node reverse level Vec_Int_t * vDivLevR; // divisor reverse level - Vec_Que_t * vQue; // pairs by count + Vec_Int_t * vVisit; // visited MUXes + Vec_Que_t * vQue; // pairs by their weight Hash_IntMan_t * vHash; // pair hash table abctime clkStart; // starting the clock int nLevelMax; // maximum level @@ -386,11 +387,13 @@ Dam_Man_t * Dam_ManAlloc( Gia_Man_t * pGia ) Dam_Man_t * p; p = ABC_CALLOC( Dam_Man_t, 1 ); p->clkStart = Abc_Clock(); + p->vVisit = Vec_IntAlloc( 1000 ); p->pGia = pGia; return p; } void Dam_ManFree( Dam_Man_t * p ) { + Vec_IntFreeP( &p->vVisit ); Vec_IntFreeP( &p->vDivLevR ); Vec_IntFreeP( &p->vNodLevR ); Vec_IntFreeP( &p->vNod2Set ); @@ -425,6 +428,10 @@ void Dam_ManCollectSets_rec( Dam_Man_t * p, int Id ) return; if ( Gia_ObjIsMux(p->pGia, pObj) ) { + if ( pObj->fMark0 ) + return; + pObj->fMark0 = 1; + Vec_IntPush( p->vVisit, Id ); Dam_ManCollectSets_rec( p, Gia_ObjFaninId0(pObj, Id) ); Dam_ManCollectSets_rec( p, Gia_ObjFaninId1(pObj, Id) ); Dam_ManCollectSets_rec( p, Gia_ObjFaninId2(p->pGia, Id) ); @@ -451,9 +458,12 @@ void Dam_ManCollectSets( Dam_Man_t * p ) p->vNod2Set = Vec_IntStart( Gia_ManObjNum(p->pGia) ); p->vSetStore = Vec_IntAlloc( Gia_ManObjNum(p->pGia) ); Vec_IntPush( p->vSetStore, -1 ); + Vec_IntClear( p->vVisit ); Gia_ManForEachCo( p->pGia, pObj, i ) Dam_ManCollectSets_rec( p, Gia_ObjFaninId0p(p->pGia, pObj) ); ABC_FREE( p->pGia->pRefs ); + Gia_ManForEachObjVec( p->vVisit, p->pGia, pObj, i ) + pObj->fMark0 = 0; } /**Function************************************************************* @@ -900,7 +910,7 @@ void Dam_ManUpdate( Dam_Man_t * p, int iDiv ) SeeAlso [] ***********************************************************************/ -Gia_Man_t * Dam_ManMultiExtractInt( Gia_Man_t * pGia, int nNewNodesMax, int fVerbose, int fVeryVerbose ) +Gia_Man_t * Dam_ManAreaBalanceInt( Gia_Man_t * pGia, int nNewNodesMax, int fVerbose, int fVeryVerbose ) { Gia_Man_t * pNew; Dam_Man_t * p; @@ -935,14 +945,14 @@ Gia_Man_t * Gia_ManAreaBalance( Gia_Man_t * p, int fSimpleAnd, int nNewNodesMax, { Gia_Man_t * pNew0, * pNew, * pNew1, * pNew2; // get the starting manager - pNew0 = Gia_ManHasMapping(p) ? (Gia_Man_t *)Dsm_ManDeriveGia(p) : p; + pNew0 = Gia_ManHasMapping(p) ? (Gia_Man_t *)Dsm_ManDeriveGia(p, 0) : p; if ( fVerbose ) Gia_ManPrintStats( pNew0, NULL ); // derive internal manager pNew = fSimpleAnd ? Gia_ManDup( pNew0 ) : Gia_ManDupMuxes( pNew0 ); if ( fVerbose ) Gia_ManPrintStats( pNew, NULL ); if ( pNew0 != p ) Gia_ManStop( pNew0 ); // perform the operation - pNew1 = Dam_ManMultiExtractInt( pNew, nNewNodesMax, fVerbose, fVeryVerbose ); + pNew1 = Dam_ManAreaBalanceInt( pNew, nNewNodesMax, fVerbose, fVeryVerbose ); if ( fVerbose ) Gia_ManPrintStats( pNew1, NULL ); Gia_ManStop( pNew ); // derive the final result @@ -952,6 +962,36 @@ Gia_Man_t * Gia_ManAreaBalance( Gia_Man_t * p, int fSimpleAnd, int nNewNodesMax, return pNew2; } +/**Function************************************************************* + + Synopsis [Synthesis script.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Gia_Man_t * Dam_ManAigSyn( Gia_Man_t * p, int fVerbose, int fVeryVerbose ) +{ + Gia_Man_t * pNew, * pTemp; + Jf_Par_t Pars, * pPars = &Pars; + Jf_ManSetDefaultPars( pPars ); + // perform balancing + pNew = Gia_ManAreaBalance( p, 0, ABC_INFINITY, fVeryVerbose, 0 ); + if ( fVerbose ) Gia_ManPrintStats( pNew, NULL ); + // perform mapping + pNew = Jf_ManPerformMapping( pTemp = pNew, pPars ); + if ( fVerbose ) Gia_ManPrintStats( pNew, NULL ); +// Gia_ManStop( pTemp ); + // perform balancing + pNew = Gia_ManAreaBalance( pTemp = pNew, 0, ABC_INFINITY, fVeryVerbose, 0 ); + if ( fVerbose ) Gia_ManPrintStats( pNew, NULL ); + Gia_ManStop( pTemp ); + return pNew; +} + //////////////////////////////////////////////////////////////////////// /// END OF FILE /// //////////////////////////////////////////////////////////////////////// diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c index c7a1c268..0e1c9b84 100644 --- a/src/base/abci/abc.c +++ b/src/base/abci/abc.c @@ -32163,6 +32163,7 @@ int Abc_CommandAbc9Bmc( Abc_Frame_t * pAbc, int argc, char ** argv ) pPars->nConfLimit = 0; // maximum number of conflicts at a node pPars->fLoadCnf = 0; // dynamic CNF loading pPars->fDumpFrames = 0; // dump unrolled timeframes + pPars->fUseSynth = 0; // use synthesis pPars->fVerbose = 0; // verbose pPars->fVeryVerbose = 0; // very verbose pPars->fNotVerbose = 0; // skip line-by-line print-out @@ -32170,7 +32171,7 @@ int Abc_CommandAbc9Bmc( Abc_Frame_t * pAbc, int argc, char ** argv ) pPars->nFailOuts = 0; // the number of failed outputs pPars->nDropOuts = 0; // the number of dropped outputs Extra_UtilGetoptReset(); - while ( ( c = Extra_UtilGetopt( argc, argv, "SFAcdvwh" ) ) != EOF ) + while ( ( c = Extra_UtilGetopt( argc, argv, "SFAcdsvwh" ) ) != EOF ) { switch ( c ) { @@ -32213,6 +32214,9 @@ int Abc_CommandAbc9Bmc( Abc_Frame_t * pAbc, int argc, char ** argv ) case 'd': pPars->fDumpFrames ^= 1; break; + case 's': + pPars->fUseSynth ^= 1; + break; case 'v': pPars->fVerbose ^= 1; break; @@ -32236,13 +32240,14 @@ int Abc_CommandAbc9Bmc( Abc_Frame_t * pAbc, int argc, char ** argv ) return 0; usage: - Abc_Print( -2, "usage: &bmc [-SFA num] [-cdvwh]\n" ); + Abc_Print( -2, "usage: &bmc [-SFA num] [-cdsvwh]\n" ); Abc_Print( -2, "\t performs bounded model checking\n" ); Abc_Print( -2, "\t-S num : the starting timeframe [default = %d]\n", pPars->nStart ); Abc_Print( -2, "\t-F num : the maximum number of timeframes [default = %d]\n", pPars->nFramesMax ); Abc_Print( -2, "\t-A num : the number of additional frames to unroll [default = %d]\n", pPars->nFramesAdd ); Abc_Print( -2, "\t-c : toggle dynamic CNF loading [default = %s]\n", pPars->fLoadCnf? "yes": "no" ); Abc_Print( -2, "\t-d : toggle dumping unfolded timeframes [default = %s]\n", pPars->fDumpFrames? "yes": "no" ); + Abc_Print( -2, "\t-s : toggle synthesizing unrolled timeframes [default = %s]\n", pPars->fUseSynth? "yes": "no" ); Abc_Print( -2, "\t-v : toggle printing verbose information [default = %s]\n", pPars->fVerbose? "yes": "no" ); Abc_Print( -2, "\t-w : toggle printing information about unfolding [default = %s]\n", pPars->fVeryVerbose? "yes": "no" ); Abc_Print( -2, "\t-h : print the command usage\n"); diff --git a/src/opt/dau/dau.h b/src/opt/dau/dau.h index a928fecf..92641b71 100644 --- a/src/opt/dau/dau.h +++ b/src/opt/dau/dau.h @@ -89,7 +89,7 @@ extern int Dau_DsdCheck1Step( word * pTruth, int nVarsInit ); /*=== dauGia.c ==========================================================*/ extern int Dsm_ManTruthToGia( void * p, word * pTruth, Vec_Int_t * vLeaves, Vec_Int_t * vCover ); -extern void * Dsm_ManDeriveGia( void * p ); +extern void * Dsm_ManDeriveGia( void * p, int fUseMuxes ); /*=== dauMerge.c ==========================================================*/ extern void Dau_DsdRemoveBraces( char * pDsd, int * pMatches ); diff --git a/src/opt/dau/dauGia.c b/src/opt/dau/dauGia.c index a714f622..2712effc 100644 --- a/src/opt/dau/dauGia.c +++ b/src/opt/dau/dauGia.c @@ -68,7 +68,10 @@ int Dau_DsdToGiaCompose_rec( Gia_Man_t * pGia, word Func, int * pFanins, int nVa return Dau_DsdToGiaCompose_rec( pGia, Func, pFanins, nVars ); t0 = Dau_DsdToGiaCompose_rec( pGia, Abc_Tt6Cofactor0(Func, nVars), pFanins, nVars ); t1 = Dau_DsdToGiaCompose_rec( pGia, Abc_Tt6Cofactor1(Func, nVars), pFanins, nVars ); - return Gia_ManHashMux( pGia, pFanins[nVars], t1, t0 ); + if ( pGia->pMuxes ) + return Gia_ManHashMuxReal( pGia, pFanins[nVars], t1, t0 ); + else + return Gia_ManHashMux( pGia, pFanins[nVars], t1, t0 ); } /**Function************************************************************* @@ -110,7 +113,10 @@ int Dau_DsdToGia_rec( Gia_Man_t * pGia, char * pStr, char ** p, int * pMatches, for ( (*p)++; *p < q; (*p)++ ) { Lit = Dau_DsdToGia_rec( pGia, pStr, p, pMatches, pLits, vCover ); - Res = Gia_ManHashXor( pGia, Res, Lit ); + if ( pGia->pMuxes ) + Res = Gia_ManHashXorReal( pGia, Res, Lit ); + else + Res = Gia_ManHashXor( pGia, Res, Lit ); } assert( *p == q ); return Abc_LitNotCond( Res, fCompl ); @@ -156,7 +162,10 @@ int Dau_DsdToGia_rec( Gia_Man_t * pGia, char * pStr, char ** p, int * pMatches, assert( **p == '{' && *q == '}' ); *p = q; } - Res = Gia_ManHashMux( pGia, Temp[0], Temp[1], Temp[2] ); + if ( pGia->pMuxes ) + Res = Gia_ManHashMuxReal( pGia, Temp[0], Temp[1], Temp[2] ); + else + Res = Gia_ManHashMux( pGia, Temp[0], Temp[1], Temp[2] ); return Abc_LitNotCond( Res, fCompl ); } if ( (**p >= 'A' && **p <= 'F') || (**p >= '0' && **p <= '9') ) @@ -250,7 +259,7 @@ void Dsm_ManReportStats() SeeAlso [] ***********************************************************************/ -void * Dsm_ManDeriveGia( void * pGia ) +void * Dsm_ManDeriveGia( void * pGia, int fUseMuxes ) { Gia_Man_t * p = (Gia_Man_t *)pGia; Gia_Man_t * pNew, * pTemp; @@ -263,6 +272,8 @@ void * Dsm_ManDeriveGia( void * pGia ) pNew = Gia_ManStart( Gia_ManObjNum(p) ); pNew->pName = Abc_UtilStrsav( p->pName ); pNew->pSpec = Abc_UtilStrsav( p->pSpec ); + if ( fUseMuxes ) + pNew->pMuxes = ABC_CALLOC( unsigned, pNew->nObjsAlloc ); // map primary inputs Gia_ManFillValue(p); Gia_ManConst0(p)->Value = 0; diff --git a/src/sat/bmc/bmc.h b/src/sat/bmc/bmc.h index 072040c5..65c24e93 100644 --- a/src/sat/bmc/bmc.h +++ b/src/sat/bmc/bmc.h @@ -82,6 +82,7 @@ struct Bmc_AndPar_t_ int nConfLimit; // maximum number of conflicts at a node int fLoadCnf; // dynamic CNF loading int fDumpFrames; // dump unrolled timeframes + int fUseSynth; // use synthesis int fVerbose; // verbose int fVeryVerbose; // very verbose int fNotVerbose; // skip line-by-line print-out diff --git a/src/sat/bmc/bmcBmcAnd.c b/src/sat/bmc/bmcBmcAnd.c index 1f203373..964ba54e 100644 --- a/src/sat/bmc/bmcBmcAnd.c +++ b/src/sat/bmc/bmcBmcAnd.c @@ -769,11 +769,18 @@ Abc_Cex_t * Gia_ManBmcCexGen( Bmc_Mna_t * pMan, Gia_Man_t * p, int iOut ) ***********************************************************************/ int Gia_ManBmcPerform( Gia_Man_t * pGia, Bmc_AndPar_t * pPars ) { + extern Gia_Man_t * Dam_ManAigSyn( Gia_Man_t * p, int fVerbose, int fVeryVerbose ); Bmc_Mna_t * p; int nFramesMax, f, i=0, Lit, status, RetValue = -2; abctime clk = Abc_Clock(); p = Bmc_MnaAlloc(); p->pFrames = Gia_ManBmcUnroll( pGia, pPars->nFramesMax, pPars->nFramesAdd, pPars->fVeryVerbose, &p->vPiMap ); + if ( pPars->fUseSynth ) + { + Gia_Man_t * pTemp = p->pFrames; + p->pFrames = Dam_ManAigSyn( pTemp, pPars->fVerbose, 0 ); + Gia_ManStop( pTemp ); + } nFramesMax = Gia_ManPoNum(p->pFrames) / Gia_ManPoNum(pGia); if ( pPars->fVerbose ) { |