diff options
| -rw-r--r-- | src/aig/gia/gia.h | 6 | ||||
| -rw-r--r-- | src/misc/tim/tim.c | 5 | ||||
| -rw-r--r-- | src/proof/cec/cecCec.c | 6 |
3 files changed, 11 insertions, 6 deletions
diff --git a/src/aig/gia/gia.h b/src/aig/gia/gia.h index 1d7bf625..376488bd 100644 --- a/src/aig/gia/gia.h +++ b/src/aig/gia/gia.h @@ -439,6 +439,8 @@ static inline int Gia_ManAppendCi( Gia_Man_t * p ) static inline int Gia_ManAppendAnd( Gia_Man_t * p, int iLit0, int iLit1 ) { Gia_Obj_t * pObj = Gia_ManAppendObj( p ); + assert( iLit0 >= 0 && Abc_Lit2Var(iLit0) < Gia_ManObjNum(p) ); + assert( iLit1 >= 0 && Abc_Lit2Var(iLit1) < Gia_ManObjNum(p) ); assert( iLit0 != iLit1 ); if ( iLit0 < iLit1 ) { @@ -463,7 +465,9 @@ static inline int Gia_ManAppendAnd( Gia_Man_t * p, int iLit0, int iLit1 ) } static inline int Gia_ManAppendCo( Gia_Man_t * p, int iLit0 ) { - Gia_Obj_t * pObj = Gia_ManAppendObj( p ); + Gia_Obj_t * pObj; + assert( iLit0 >= 0 && Abc_Lit2Var(iLit0) < Gia_ManObjNum(p) ); + pObj = Gia_ManAppendObj( p ); pObj->fTerm = 1; pObj->iDiff0 = Gia_ObjId(p, pObj) - Abc_Lit2Var(iLit0); pObj->fCompl0 = Abc_LitIsCompl(iLit0); diff --git a/src/misc/tim/tim.c b/src/misc/tim/tim.c index fe5f214d..9056d261 100644 --- a/src/misc/tim/tim.c +++ b/src/misc/tim/tim.c @@ -582,6 +582,7 @@ void Tim_ManCreateBoxFirst( Tim_Man_t * p, int firstIn, int nIns, int firstOut, { Tim_Box_t * pBox; int i; +// printf( "Creating %d x %d box with first inputs (%d and %d).\n", nIns, nOuts, firstIn, firstOut ); pBox = (Tim_Box_t *)Mem_FlexEntryFetch( p->pMemObj, sizeof(Tim_Box_t) + sizeof(int) * (nIns+nOuts) ); memset( pBox, 0, sizeof(Tim_Box_t) ); @@ -847,7 +848,7 @@ float Tim_ManGetCoRequired( Tim_Man_t * p, int iCo ) if ( p->fUseTravId ) Tim_ManBoxForEachOutput( p, pBox, pObj, i ) if ( pObj->TravId != p->nTravIds ) - printf( "Tim_ManGetCoRequired(): Output required times of the box are not up to date!\n" ); + printf( "Tim_ManGetCoRequired(): Output required times of output %d the box %d are not up to date!\n", i, pBox->iBox ); // compute the required times for each input of the box (POs) Tim_ManBoxForEachInput( p, pBox, pObjRes, i ) { @@ -855,7 +856,7 @@ float Tim_ManGetCoRequired( Tim_Man_t * p, int iCo ) Tim_ManBoxForEachOutput( p, pBox, pObj, k ) { pDelays = pBox->pDelayTable + k * pBox->nInputs; - DelayBest = Abc_MinInt( DelayBest, pObj->timeReq - pDelays[i] ); + DelayBest = Abc_MinFloat( DelayBest, pObj->timeReq - pDelays[i] ); } pObjRes->timeReq = DelayBest; pObjRes->TravId = p->nTravIds; diff --git a/src/proof/cec/cecCec.c b/src/proof/cec/cecCec.c index aa36a28e..b9b3e1f1 100644 --- a/src/proof/cec/cecCec.c +++ b/src/proof/cec/cecCec.c @@ -143,7 +143,7 @@ int Cec_ManHandleSpecialCases( Gia_Man_t * p, Cec_ParCec_t * pPars ) // (for example, when they have the same driver but complemented) if ( Gia_ObjPhase(pObj1) != Gia_ObjPhase(pObj2) ) { - Abc_Print( 1, "Networks are NOT EQUIVALENT. Outputs %d trivially differ. ", i/2 ); + Abc_Print( 1, "Networks are NOT EQUIVALENT. Outputs %d trivially differ (different phase). ", i/2 ); Abc_PrintTime( 1, "Time", clock() - clk ); pPars->iOutFail = i/2; Cec_ManTransformPattern( p, i/2, NULL ); @@ -155,7 +155,7 @@ int Cec_ManHandleSpecialCases( Gia_Man_t * p, Cec_ParCec_t * pPars ) // drivers are different PIs if ( Gia_ObjIsPi(p, pDri1) && Gia_ObjIsPi(p, pDri2) && pDri1 != pDri2 ) { - Abc_Print( 1, "Networks are NOT EQUIVALENT. Outputs %d trivially differ. ", i/2 ); + Abc_Print( 1, "Networks are NOT EQUIVALENT. Outputs %d trivially differ (different PIs). ", i/2 ); Abc_PrintTime( 1, "Time", clock() - clk ); pPars->iOutFail = i/2; Cec_ManTransformPattern( p, i/2, NULL ); @@ -168,7 +168,7 @@ int Cec_ManHandleSpecialCases( Gia_Man_t * p, Cec_ParCec_t * pPars ) if ( (Gia_ObjIsPi(p, pDri1) && Gia_ObjIsConst0(pDri2)) || (Gia_ObjIsPi(p, pDri2) && Gia_ObjIsConst0(pDri1)) ) { - Abc_Print( 1, "Networks are NOT EQUIVALENT. Outputs %d trivially differ. ", i/2 ); + Abc_Print( 1, "Networks are NOT EQUIVALENT. Outputs %d trivially differ (PI vs. constant). ", i/2 ); Abc_PrintTime( 1, "Time", clock() - clk ); pPars->iOutFail = i/2; Cec_ManTransformPattern( p, i/2, NULL ); |