diff options
| author | Alan Mishchenko <alanmi@berkeley.edu> | 2012-06-29 13:50:01 -0700 |
|---|---|---|
| committer | Alan Mishchenko <alanmi@berkeley.edu> | 2012-06-29 13:50:01 -0700 |
| commit | 2c9827cb15a1e71441dfd7cd7633537b33036487 (patch) | |
| tree | 1985d4830f5abf64a52a272687348334a771e7d4 | |
| parent | 7e9ccf7a2328fa3599197c7db51a46b26e1fbb51 (diff) | |
| download | abc-2c9827cb15a1e71441dfd7cd7633537b33036487.tar.gz abc-2c9827cb15a1e71441dfd7cd7633537b33036487.tar.bz2 abc-2c9827cb15a1e71441dfd7cd7633537b33036487.zip | |
Bug fix in &gla.
| -rw-r--r-- | src/aig/gia/giaAbsGla.c | 10 |
1 files changed, 10 insertions, 0 deletions
diff --git a/src/aig/gia/giaAbsGla.c b/src/aig/gia/giaAbsGla.c index bf889892..18ef8942 100644 --- a/src/aig/gia/giaAbsGla.c +++ b/src/aig/gia/giaAbsGla.c @@ -672,6 +672,8 @@ int Gla_ManGetOutLit( Gla_Man_t * p, int f ) Gla_Obj_t * pFanin = Gla_ManObj( p, p->pObjRoot->Fanins[0] ); int iSat = Vec_IntEntry( &pFanin->vFrames, f ); assert( iSat > 0 ); + if ( f == 0 && pFanin->fRo && !p->pObjRoot->fCompl0 ) + return -1; return Abc_Var2Lit( iSat, p->pObjRoot->fCompl0 ); } Vec_Int_t * Gla_ManUnsatCore( Gla_Man_t * p, int f, Vec_Int_t * vCla2Obj, sat_solver2 * pSat, int nConfMax, int fVerbose, int * piRetValue, int * pnConfls ) @@ -682,6 +684,14 @@ Vec_Int_t * Gla_ManUnsatCore( Gla_Man_t * p, int f, Vec_Int_t * vCla2Obj, sat_so int i, Entry, RetValue, clk = clock(); if ( piRetValue ) *piRetValue = 1; + // consider special case when PO points to the flop + // this leads to immediate conflict in the first timeframe + if ( iLit == -1 ) + { + vCore = Vec_IntAlloc( 1 ); + Vec_IntPush( vCore, p->pObjRoot->Fanins[0] ); + return vCore; + } // solve the problem RetValue = sat_solver2_solve( pSat, &iLit, &iLit+1, (ABC_INT64_T)nConfMax, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0 ); if ( pnConfls ) |