diff options
| author | Alan Mishchenko <alanmi@berkeley.edu> | 2013-10-02 23:17:59 -0700 |
|---|---|---|
| committer | Alan Mishchenko <alanmi@berkeley.edu> | 2013-10-02 23:17:59 -0700 |
| commit | 6014c4b11ec25aaa23dc72101c548857ab4e7367 (patch) | |
| tree | 69dbbb163f54aaf22fe77fbf5340d61f2bbc4678 /src | |
| parent | 805eb96d6d1be9542fd9af90125df190f796703f (diff) | |
| download | abc-6014c4b11ec25aaa23dc72101c548857ab4e7367.tar.gz abc-6014c4b11ec25aaa23dc72101c548857ab4e7367.tar.bz2 abc-6014c4b11ec25aaa23dc72101c548857ab4e7367.zip | |
Integrating synthesis into the new BMC engine.
Diffstat (limited to 'src')
| -rw-r--r-- | src/aig/gia/giaBalance.c | 1 | ||||
| -rw-r--r-- | src/sat/bmc/bmcBmcAnd.c | 6 |
2 files changed, 3 insertions, 4 deletions
diff --git a/src/aig/gia/giaBalance.c b/src/aig/gia/giaBalance.c index 5855fc3d..12659149 100644 --- a/src/aig/gia/giaBalance.c +++ b/src/aig/gia/giaBalance.c @@ -978,6 +978,7 @@ 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 ); + if ( fVerbose ) Gia_ManPrintStats( p, NULL ); // perform balancing pNew = Gia_ManAreaBalance( p, 0, ABC_INFINITY, fVeryVerbose, 0 ); if ( fVerbose ) Gia_ManPrintStats( pNew, NULL ); diff --git a/src/sat/bmc/bmcBmcAnd.c b/src/sat/bmc/bmcBmcAnd.c index 8cdd162d..38d19a61 100644 --- a/src/sat/bmc/bmcBmcAnd.c +++ b/src/sat/bmc/bmcBmcAnd.c @@ -781,16 +781,14 @@ int Gia_ManBmcPerform( Gia_Man_t * pGia, Bmc_AndPar_t * pPars ) printf( "Unfolding for %d frames with first non-trivial PO %d. ", nFramesMax, Gia_ManBmcFindFirst(p->pFrames) ); Abc_PrintTime( 1, "Time", Abc_Clock() - clk ); } - 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 ); } + else if ( pPars->fVerbose ) + Gia_ManPrintStats( p->pFrames, NULL ); if ( pPars->fDumpFrames ) { Gia_AigerWrite( p->pFrames, "frames.aig", 0, 0 ); |