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/sat/bmc/bmcBmcAnd.c | |
| 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/sat/bmc/bmcBmcAnd.c')
| -rw-r--r-- | src/sat/bmc/bmcBmcAnd.c | 7 |
1 files changed, 7 insertions, 0 deletions
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 ) { |