From 805eb96d6d1be9542fd9af90125df190f796703f Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Wed, 2 Oct 2013 23:03:17 -0700 Subject: Integrating synthesis into the new BMC engine. --- src/sat/bmc/bmcBmcAnd.c | 14 ++++++++------ 1 file changed, 8 insertions(+), 6 deletions(-) (limited to 'src/sat') diff --git a/src/sat/bmc/bmcBmcAnd.c b/src/sat/bmc/bmcBmcAnd.c index 964ba54e..8cdd162d 100644 --- a/src/sat/bmc/bmcBmcAnd.c +++ b/src/sat/bmc/bmcBmcAnd.c @@ -775,12 +775,6 @@ int Gia_ManBmcPerform( Gia_Man_t * pGia, Bmc_AndPar_t * pPars ) 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 ) { @@ -789,6 +783,14 @@ int Gia_ManBmcPerform( Gia_Man_t * pGia, Bmc_AndPar_t * pPars ) } if ( pPars->fVerbose ) Gia_ManPrintStats( p->pFrames, NULL ); + if ( pPars->fUseSynth ) + { + Gia_Man_t * pTemp = p->pFrames; + p->pFrames = Dam_ManAigSyn( pTemp, pPars->fVerbose, 0 ); + Gia_ManStop( pTemp ); + if ( pPars->fVerbose ) + Gia_ManPrintStats( p->pFrames, NULL ); + } if ( pPars->fDumpFrames ) { Gia_AigerWrite( p->pFrames, "frames.aig", 0, 0 ); -- cgit v1.2.3