diff options
| author | Alan Mishchenko <alanmi@berkeley.edu> | 2013-10-02 23:03:17 -0700 |
|---|---|---|
| committer | Alan Mishchenko <alanmi@berkeley.edu> | 2013-10-02 23:03:17 -0700 |
| commit | 805eb96d6d1be9542fd9af90125df190f796703f (patch) | |
| tree | 2758682a5e0cd6f19dfd198318b6aa7234ab18e4 | |
| parent | cfa7be1a07e3102195b2395f379f50e556dbf4e3 (diff) | |
| download | abc-805eb96d6d1be9542fd9af90125df190f796703f.tar.gz abc-805eb96d6d1be9542fd9af90125df190f796703f.tar.bz2 abc-805eb96d6d1be9542fd9af90125df190f796703f.zip | |
Integrating synthesis into the new BMC engine.
| -rw-r--r-- | src/map/if/ifDec07.c | 2 | ||||
| -rw-r--r-- | src/map/mio/mioParse.c | 7 | ||||
| -rw-r--r-- | src/sat/bmc/bmcBmcAnd.c | 14 |
3 files changed, 12 insertions, 11 deletions
diff --git a/src/map/if/ifDec07.c b/src/map/if/ifDec07.c index b5f4d324..1bbc93fb 100644 --- a/src/map/if/ifDec07.c +++ b/src/map/if/ifDec07.c @@ -713,7 +713,7 @@ word If_Dec5Perform( word t, int fDerive ) { int Pla2Var[7], Var2Pla[7]; int i, j, v; - word t0 = t; +// word t0 = t; word c0, c1, c00, c01, c10, c11; for ( i = 0; i < 5; i++ ) { diff --git a/src/map/mio/mioParse.c b/src/map/mio/mioParse.c index cac21596..6d7740a2 100644 --- a/src/map/mio/mioParse.c +++ b/src/map/mio/mioParse.c @@ -429,7 +429,7 @@ void Mio_ParseFormulaTruthTest( char * pFormInit, char ** ppVarNames, int nVars int Mio_ParseCheckName( Mio_Gate_t * pGate, char ** ppStr ) { Mio_Pin_t * pPin; - int i, iBest; + int i, iBest = -1; // find the longest pin name that matches substring char * pNameBest = NULL; for ( pPin = Mio_GateReadPins(pGate), i = 0; pPin; pPin = Mio_PinReadNext(pPin), i++ ) @@ -437,9 +437,8 @@ int Mio_ParseCheckName( Mio_Gate_t * pGate, char ** ppStr ) if ( pNameBest == NULL || strlen(pNameBest) < strlen(Mio_PinReadName(pPin)) ) pNameBest = Mio_PinReadName(pPin), iBest = i; // if pin is not found, return -1 - if ( pNameBest == NULL ) - return -1; - *ppStr += strlen(pNameBest) - 1; + if ( pNameBest ) + *ppStr += strlen(pNameBest) - 1; return iBest; } int Mio_ParseCheckFormula( Mio_Gate_t * pGate, char * pForm ) 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 ); |