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 <noreply@anthropic.com>

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;

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 );

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;

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" );
 }