From 2c9827cb15a1e71441dfd7cd7633537b33036487 Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Fri, 29 Jun 2012 13:50:01 -0700 Subject: Bug fix in &gla. --- src/aig/gia/giaAbsGla.c | 10 ++++++++++ 1 file changed, 10 insertions(+) (limited to 'src/aig/gia') 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 ) -- cgit v1.2.3