From 3b5036a1e1175a05c307b50393c2f1667490fd5a Mon Sep 17 00:00:00 2001 From: Jonathan Greene Date: Sat, 21 Feb 2026 16:54:27 -0800 Subject: [PATCH] Fix required time handling for unconstrained POs, infinity arithmetic, and absDup cosmetic - Tim_ManInitPoRequiredAll: only overwrite PO required times when ALL are unconstrained; preserve user-specified constraints - Gia_ObjPropagateRequired: propagate infinity unchanged through LUTs - Tim_ManGetCoRequired: guard against infinity minus delay arithmetic - Gia_ManDelayTraceLut: handle infinite required times in slack computation; allow negative slack to report timing violations - Tim_ManCreate: fix required-time loading to address actual POs via Tim_ManForEachPo instead of p->pCos[] (wrong for designs with boxes) - Tim_ManGetArrTimes/Tim_ManGetReqTimes: fix loop-exit detection using boolean flag instead of comparing iterator index against PO/PI count - Gia_ManPrintFlopClasses: use Gia_ManRegBoxNum instead of Gia_ManRegNum Co-Authored-By: Claude Opus 4.6 --- src/aig/gia/giaSpeedup.c | 11 ++++++++--- src/misc/tim/timMan.c | 41 +++++++++++++++++++++++++--------------- src/misc/tim/timTime.c | 7 ++++++- src/proof/abs/absDup.c | 4 ++-- 4 files changed, 42 insertions(+), 21 deletions(-) diff --git a/src/aig/gia/giaSpeedup.c b/src/aig/gia/giaSpeedup.c index aa39c9bcd..4212c8966 100644 --- a/src/aig/gia/giaSpeedup.c +++ b/src/aig/gia/giaSpeedup.c @@ -209,6 +209,9 @@ float Gia_ObjPropagateRequired( Gia_Man_t * p, int iObj, int fUseSorting ) float tRequired = 0.0; // Suppress "might be used uninitialized" float * pDelays; assert( Gia_ObjIsLut(p, iObj) ); + // Infinity propagates unchanged + if ( Gia_ObjTimeRequired( p, iObj ) >= TIM_ETERNITY ) + return TIM_ETERNITY; if ( pLutLib == NULL && pCellLib == NULL ) { tRequired = Gia_ObjTimeRequired( p, iObj) - (float)1.0; @@ -407,9 +410,11 @@ float Gia_ManDelayTraceLut( Gia_Man_t * p ) } // set slack for this object - tSlack = Gia_ObjTimeRequired(p, iObj) - Gia_ObjTimeArrival(p, iObj); - assert( tSlack + 0.01 > 0.0 ); - Gia_ObjSetTimeSlack( p, iObj, tSlack < 0.0 ? 0.0 : tSlack ); + if ( Gia_ObjTimeRequired(p, iObj) >= TIM_ETERNITY ) + tSlack = TIM_ETERNITY; + else + tSlack = Gia_ObjTimeRequired(p, iObj) - Gia_ObjTimeArrival(p, iObj); + Gia_ObjSetTimeSlack( p, iObj, tSlack ); } Vec_IntFree( vObjs ); return tArrival; diff --git a/src/misc/tim/timMan.c b/src/misc/tim/timMan.c index 274dc0c0e..59eac5a0d 100644 --- a/src/misc/tim/timMan.c +++ b/src/misc/tim/timMan.c @@ -591,19 +591,16 @@ void Tim_ManCreate( Tim_Man_t * p, void * pLib, Vec_Flt_t * vInArrs, Vec_Flt_t * { // Handle special case when timing is only for POs (without boxes/flops) // This happens when old files provide timing for actual design POs only - if ( Vec_FltSize(vOutReqs) < Tim_ManPoNum(p) ) + if ( Vec_FltSize(vOutReqs) <= Tim_ManPoNum(p) ) { - // Special case: timing for actual POs only (less than Tim_ManPoNum when boxes exist) - for ( i = 0; i < Vec_FltSize(vOutReqs); i++ ) - p->pCos[i].timeReq = Vec_FltEntry(vOutReqs, i); - } - else if ( Vec_FltSize(vOutReqs) == Tim_ManPoNum(p) ) - { - // Original case: timing for POs + // Timing for POs (may be partial — omitted entries stay at TIM_ETERNITY) k = 0; Tim_ManForEachPo( p, pObj, i ) + { + if ( k >= Vec_FltSize(vOutReqs) ) + break; pObj->timeReq = Vec_FltEntry(vOutReqs, k++); - assert( k == Tim_ManPoNum(p) ); + } } else { @@ -633,20 +630,27 @@ float * Tim_ManGetArrTimes( Tim_Man_t * p, int nRegs ) float * pTimes; Tim_Obj_t * pObj; int i; + int fFoundTiming = 0; // Check if any PIs have non-zero arrival times Tim_ManForEachPi( p, pObj, i ) if ( pObj->timeArr != 0.0 ) + { + fFoundTiming = 1; break; - if ( i == Tim_ManPiNum(p) && nRegs > 0 ) + } + if ( !fFoundTiming && nRegs > 0 ) { // Check if any flops have non-zero arrival times for ( i = Tim_ManCiNum(p) - nRegs; i < Tim_ManCiNum(p); i++ ) if ( p->pCis[i].timeArr != 0.0 ) + { + fFoundTiming = 1; break; - if ( i == Tim_ManCiNum(p) ) + } + if ( !fFoundTiming ) return NULL; // No timing info at all } - else if ( i == Tim_ManPiNum(p) ) + else if ( !fFoundTiming ) return NULL; // Allocate array for PIs + Flops (compact format, no box outputs) pTimes = ABC_FALLOC( float, Tim_ManPiNum(p) + nRegs ); @@ -663,20 +667,27 @@ float * Tim_ManGetReqTimes( Tim_Man_t * p, int nRegs ) float * pTimes; Tim_Obj_t * pObj; int i, k = 0; + int fFoundConstraint = 0; // Check if any POs have non-infinity required times Tim_ManForEachPo( p, pObj, i ) if ( pObj->timeReq != TIM_ETERNITY ) + { + fFoundConstraint = 1; break; - if ( i == Tim_ManPoNum(p) && nRegs > 0 ) + } + if ( !fFoundConstraint && nRegs > 0 ) { // Check if any flops have non-infinity required times for ( i = Tim_ManCoNum(p) - nRegs; i < Tim_ManCoNum(p); i++ ) if ( p->pCos[i].timeReq != TIM_ETERNITY ) + { + fFoundConstraint = 1; break; - if ( i == Tim_ManCoNum(p) ) + } + if ( !fFoundConstraint ) return NULL; // No timing info at all } - else if ( i == Tim_ManPoNum(p) ) + else if ( !fFoundConstraint ) return NULL; // Allocate array for POs + Flops (compact format, no box inputs) pTimes = ABC_FALLOC( float, Tim_ManPoNum(p) + nRegs ); diff --git a/src/misc/tim/timTime.c b/src/misc/tim/timTime.c index 578eead31..cc0aa5ffd 100644 --- a/src/misc/tim/timTime.c +++ b/src/misc/tim/timTime.c @@ -98,6 +98,11 @@ void Tim_ManInitPoRequiredAll( Tim_Man_t * p, float Delay ) { Tim_Obj_t * pObj; int i; + // If any PO or flop-input CO is constrained, leave all unchanged + Tim_ManForEachPo( p, pObj, i ) + if ( pObj->timeReq < TIM_ETERNITY ) + return; + // All unconstrained — set to max arrival time Tim_ManForEachPo( p, pObj, i ) Tim_ManSetCoRequired( p, i, Delay ); } @@ -249,7 +254,7 @@ float Tim_ManGetCoRequired( Tim_Man_t * p, int iCo ) Tim_ManBoxForEachOutput( p, pBox, pObj, k ) { pDelays = pTable + 3 + k * pBox->nInputs; - if ( pDelays[i] != -ABC_INFINITY ) + if ( pDelays[i] != -ABC_INFINITY && pObj->timeReq < TIM_ETERNITY ) DelayBest = Abc_MinFloat( DelayBest, pObj->timeReq - pDelays[i] ); } pObjRes->timeReq = DelayBest; diff --git a/src/proof/abs/absDup.c b/src/proof/abs/absDup.c index 942155753..8bd3b537a 100644 --- a/src/proof/abs/absDup.c +++ b/src/proof/abs/absDup.c @@ -303,7 +303,7 @@ void Gia_ManPrintFlopClasses( Gia_Man_t * p ) int Counter0, Counter1; if ( p->vFlopClasses == NULL ) return; - if ( Vec_IntSize(p->vFlopClasses) != Gia_ManRegNum(p) ) + if ( Vec_IntSize(p->vFlopClasses) != Gia_ManRegBoxNum(p) ) { printf( "Gia_ManPrintFlopClasses(): The number of flop map entries differs from the number of flops.\n" ); return; @@ -312,7 +312,7 @@ void Gia_ManPrintFlopClasses( Gia_Man_t * p ) Counter1 = Vec_IntCountEntry( p->vFlopClasses, 1 ); printf( "Flop-level abstraction: Excluded FFs = %d Included FFs = %d (%.2f %%) ", Counter0, Counter1, 100.0*Counter1/(Counter0 + Counter1 + 1) ); - if ( Counter0 + Counter1 < Gia_ManRegNum(p) ) + if ( Counter0 + Counter1 < Gia_ManRegBoxNum(p) ) printf( "and there are other FF classes..." ); printf( "\n" ); }