Supporting edges in delay-optimization in &satlut.

src/aig/gia/gia.h

@@ -1447,6 +1447,7 @@ extern int                 Gia_ManBoxCoNum( Gia_Man_t * p );
 extern int                 Gia_ManClockDomainNum( Gia_Man_t * p );
 extern int                 Gia_ManIsSeqWithBoxes( Gia_Man_t * p );
 extern int                 Gia_ManIsNormalized( Gia_Man_t * p );
+extern Vec_Int_t *         Gia_ManOrderWithBoxes( Gia_Man_t * p );
 extern Gia_Man_t *         Gia_ManDupNormalize( Gia_Man_t * p );
 extern Gia_Man_t *         Gia_ManDupUnnormalize( Gia_Man_t * p );
 extern Gia_Man_t *         Gia_ManDupUnshuffleInputs( Gia_Man_t * p );

src/aig/gia/giaEdge.c

@@ -19,6 +19,7 @@
 ***********************************************************************/
 
 #include "gia.h"
+#include "misc/tim/tim.h"
 
 ABC_NAMESPACE_IMPL_START
 
@@ -196,11 +197,77 @@ int Gia_ManEvalEdgeDelay( Gia_Man_t * p )
     Vec_IntFreeP( &p->vEdgeDelay );
     p->vEdgeDelay = Vec_IntStart( Gia_ManObjNum(p) );
     if ( Gia_ManHasMapping(p) )
-        Gia_ManForEachLut( p, iLut )
-            Vec_IntWriteEntry( p->vEdgeDelay, iLut, Gia_ObjEvalEdgeDelay(p, iLut, p->vEdgeDelay) );
+    {
+        if ( p->pManTime != NULL && Tim_ManBoxNum((Tim_Man_t*)p->pManTime) )
+        {
+            Gia_Obj_t * pObj; 
+            Vec_Int_t * vNodes = Gia_ManOrderWithBoxes( p );
+            Tim_ManIncrementTravId( (Tim_Man_t*)p->pManTime );
+            Gia_ManForEachObjVec( vNodes, p, pObj, k )
+            {
+                iLut = Gia_ObjId( p, pObj );
+                if ( Gia_ObjIsAnd(pObj) )
+                {
+                    if ( Gia_ObjIsLut(p, iLut) )
+                        Vec_IntWriteEntry( p->vEdgeDelay, iLut, Gia_ObjEvalEdgeDelay(p, iLut, p->vEdgeDelay) );
+                }
+                else if ( Gia_ObjIsCi(pObj) )
+                {
+                    int arrTime = Tim_ManGetCiArrival( (Tim_Man_t*)p->pManTime, Gia_ObjCioId(pObj) );
+                    Vec_IntWriteEntry( p->vEdgeDelay,  iLut, arrTime );
+                }
+                else if ( Gia_ObjIsCo(pObj) )
+                {
+                    int arrTime = Vec_IntEntry( p->vEdgeDelay, Gia_ObjFaninId0(pObj, iLut) );
+                    Tim_ManSetCoArrival( (Tim_Man_t*)p->pManTime, Gia_ObjCioId(pObj), arrTime );
+                }
+                else if ( !Gia_ObjIsConst0(pObj) ) 
+                    assert( 0 );
+            }
+            Vec_IntFree( vNodes );
+        }
+        else
+        {
+            Gia_ManForEachLut( p, iLut )
+                Vec_IntWriteEntry( p->vEdgeDelay, iLut, Gia_ObjEvalEdgeDelay(p, iLut, p->vEdgeDelay) );
+        }
+    }
     else if ( Gia_ManHasMapping2(p) )
-        Gia_ManForEachLut2( p, iLut )
-            Vec_IntWriteEntry( p->vEdgeDelay, iLut, Gia_ObjEvalEdgeDelay(p, iLut, p->vEdgeDelay) );
+    {
+        if ( p->pManTime != NULL && Tim_ManBoxNum((Tim_Man_t*)p->pManTime) )
+        {
+            Gia_Obj_t * pObj; 
+            Vec_Int_t * vNodes = Gia_ManOrderWithBoxes( p );
+            Tim_ManIncrementTravId( (Tim_Man_t*)p->pManTime );
+            Gia_ManForEachObjVec( vNodes, p, pObj, k )
+            {
+                iLut = Gia_ObjId( p, pObj );
+                if ( Gia_ObjIsAnd(pObj) )
+                {
+                    if ( Gia_ObjIsLut2(p, iLut) )
+                        Vec_IntWriteEntry( p->vEdgeDelay, iLut, Gia_ObjEvalEdgeDelay(p, iLut, p->vEdgeDelay) );
+                }
+                else if ( Gia_ObjIsCi(pObj) )
+                {
+                    int arrTime = Tim_ManGetCiArrival( (Tim_Man_t*)p->pManTime, Gia_ObjCioId(pObj) );
+                    Vec_IntWriteEntry( p->vEdgeDelay,  iLut, arrTime );
+                }
+                else if ( Gia_ObjIsCo(pObj) )
+                {
+                    int arrTime = Vec_IntEntry( p->vEdgeDelay, Gia_ObjFaninId0(pObj, iLut) );
+                    Tim_ManSetCoArrival( (Tim_Man_t*)p->pManTime, Gia_ObjCioId(pObj), arrTime );
+                }
+                else if ( !Gia_ObjIsConst0(pObj) ) 
+                    assert( 0 );
+            }
+            Vec_IntFree( vNodes );
+        }
+        else
+        {
+            Gia_ManForEachLut2( p, iLut )
+                Vec_IntWriteEntry( p->vEdgeDelay, iLut, Gia_ObjEvalEdgeDelay(p, iLut, p->vEdgeDelay) );
+        }
+    }
     else assert( 0 );
     Gia_ManForEachCoDriverId( p, iLut, k )
         DelayMax = Abc_MaxInt( DelayMax, Vec_IntEntry(p->vEdgeDelay, iLut) );
@@ -310,11 +377,77 @@ int Gia_ManComputeEdgeDelay( Gia_Man_t * p )
     p->vEdge2 = Vec_IntStart( Gia_ManObjNum(p) );
     p->vEdgeDelay = Vec_IntStart( Gia_ManObjNum(p) );
     if ( Gia_ManHasMapping(p) )
-        Gia_ManForEachLut( p, iLut )
-            Gia_ObjComputeEdgeDelay( p, iLut, p->vEdgeDelay, p->vEdge1, p->vEdge2 );
+    {
+        if ( p->pManTime != NULL && Tim_ManBoxNum((Tim_Man_t*)p->pManTime) )
+        {
+            Gia_Obj_t * pObj; 
+            Vec_Int_t * vNodes = Gia_ManOrderWithBoxes( p );
+            Tim_ManIncrementTravId( (Tim_Man_t*)p->pManTime );
+            Gia_ManForEachObjVec( vNodes, p, pObj, k )
+            {
+                iLut = Gia_ObjId( p, pObj );
+                if ( Gia_ObjIsAnd(pObj) )
+                {
+                    if ( Gia_ObjIsLut(p, iLut) )
+                        Gia_ObjComputeEdgeDelay( p, iLut, p->vEdgeDelay, p->vEdge1, p->vEdge2 );
+                }
+                else if ( Gia_ObjIsCi(pObj) )
+                {
+                    int arrTime = Tim_ManGetCiArrival( (Tim_Man_t*)p->pManTime, Gia_ObjCioId(pObj) );
+                    Vec_IntWriteEntry( p->vEdgeDelay,  iLut, arrTime );
+                }
+                else if ( Gia_ObjIsCo(pObj) )
+                {
+                    int arrTime = Vec_IntEntry( p->vEdgeDelay, Gia_ObjFaninId0(pObj, iLut) );
+                    Tim_ManSetCoArrival( (Tim_Man_t*)p->pManTime, Gia_ObjCioId(pObj), arrTime );
+                }
+                else if ( !Gia_ObjIsConst0(pObj) ) 
+                    assert( 0 );
+            }
+            Vec_IntFree( vNodes );
+        }
+        else
+        {
+            Gia_ManForEachLut( p, iLut )
+                Gia_ObjComputeEdgeDelay( p, iLut, p->vEdgeDelay, p->vEdge1, p->vEdge2 );
+        }
+    }
     else if ( Gia_ManHasMapping2(p) )
-        Gia_ManForEachLut2( p, iLut )
-            Gia_ObjComputeEdgeDelay( p, iLut, p->vEdgeDelay, p->vEdge1, p->vEdge2 );
+    {
+        if ( p->pManTime != NULL && Tim_ManBoxNum((Tim_Man_t*)p->pManTime) )
+        {
+            Gia_Obj_t * pObj; 
+            Vec_Int_t * vNodes = Gia_ManOrderWithBoxes( p );
+            Tim_ManIncrementTravId( (Tim_Man_t*)p->pManTime );
+            Gia_ManForEachObjVec( vNodes, p, pObj, k )
+            {
+                iLut = Gia_ObjId( p, pObj );
+                if ( Gia_ObjIsAnd(pObj) )
+                {
+                    if ( Gia_ObjIsLut2(p, iLut) )
+                        Gia_ObjComputeEdgeDelay( p, iLut, p->vEdgeDelay, p->vEdge1, p->vEdge2 );
+                }
+                else if ( Gia_ObjIsCi(pObj) )
+                {
+                    int arrTime = Tim_ManGetCiArrival( (Tim_Man_t*)p->pManTime, Gia_ObjCioId(pObj) );
+                    Vec_IntWriteEntry( p->vEdgeDelay,  iLut, arrTime );
+                }
+                else if ( Gia_ObjIsCo(pObj) )
+                {
+                    int arrTime = Vec_IntEntry( p->vEdgeDelay, Gia_ObjFaninId0(pObj, iLut) );
+                    Tim_ManSetCoArrival( (Tim_Man_t*)p->pManTime, Gia_ObjCioId(pObj), arrTime );
+                }
+                else if ( !Gia_ObjIsConst0(pObj) ) 
+                    assert( 0 );
+            }
+            Vec_IntFree( vNodes );
+        }
+        else
+        {
+            Gia_ManForEachLut2( p, iLut )
+                Gia_ObjComputeEdgeDelay( p, iLut, p->vEdgeDelay, p->vEdge1, p->vEdge2 );
+        }
+    }
     else assert( 0 );
     Gia_ManForEachCoDriverId( p, iLut, k )
         DelayMax = Abc_MaxInt( DelayMax, Vec_IntEntry(p->vEdgeDelay, iLut) );
@@ -414,10 +547,11 @@ int Gia_ObjComputeEdgeDelay2( Gia_Man_t * p, int iObj, Vec_Int_t * vDelay, Vec_I
 }
 int Gia_ManComputeEdgeDelay2( Gia_Man_t * p )
 {
-    int k, iLut, DelayMax = 0, EdgeCount = 0;
+    int k, iLut, DelayMax = 0;
     Vec_Int_t * vFanMax1 = Vec_IntStart( Gia_ManObjNum(p) );
     Vec_Int_t * vFanMax2 = Vec_IntStart( Gia_ManObjNum(p) );
     Vec_Int_t * vCountMax = Vec_IntStart( Gia_ManObjNum(p) );
+    assert( p->pManTime == NULL );
     Vec_IntFreeP( &p->vEdgeDelay );
     Vec_IntFreeP( &p->vEdge1 );
     Vec_IntFreeP( &p->vEdge2 );

src/aig/gia/giaSatLut.c

@@ -19,6 +19,7 @@
 ***********************************************************************/
 
 #include "gia.h"
+#include "misc/tim/tim.h"
 #include "sat/bsat/satStore.h"
 #include "misc/util/utilNam.h"
 #include "map/scl/sclCon.h"
@@ -303,27 +304,101 @@ int Sbl_ManCreateTiming( Sbl_Man_t * p, int DelayStart )
     int DelayMax = DelayStart, Delay, iLut, iFan, k;
     // compute arrival times
     Vec_IntFill( p->vArrs,  Gia_ManObjNum(p->pGia), 0 );
-    Gia_ManForEachLut2( p->pGia, iLut )
+    if ( p->pGia->pManTime != NULL && Tim_ManBoxNum((Tim_Man_t*)p->pGia->pManTime) )
     {
-        vFanins = Gia_ObjLutFanins2(p->pGia, iLut);
-        Delay = Sbl_ManComputeDelay( p, iLut, vFanins );
-        Vec_IntWriteEntry( p->vArrs,  iLut, Delay );
-        DelayMax = Abc_MaxInt( DelayMax, Delay );
+        Gia_Obj_t * pObj; 
+        Vec_Int_t * vNodes = Gia_ManOrderWithBoxes( p->pGia );
+        Tim_ManIncrementTravId( (Tim_Man_t*)p->pGia->pManTime );
+        Gia_ManForEachObjVec( vNodes, p->pGia, pObj, k )
+        {
+            iLut = Gia_ObjId( p->pGia, pObj );
+            if ( Gia_ObjIsAnd(pObj) )
+            {
+                if ( Gia_ObjIsLut2(p->pGia, iLut) )
+                {
+                    vFanins = Gia_ObjLutFanins2(p->pGia, iLut);
+                    Delay = Sbl_ManComputeDelay( p, iLut, vFanins );
+                    Vec_IntWriteEntry( p->vArrs,  iLut, Delay );
+                    DelayMax = Abc_MaxInt( DelayMax, Delay );
+                }
+            }
+            else if ( Gia_ObjIsCi(pObj) )
+            {
+                int arrTime = Tim_ManGetCiArrival( (Tim_Man_t*)p->pGia->pManTime, Gia_ObjCioId(pObj) );
+                Vec_IntWriteEntry( p->vArrs,  iLut, arrTime );
+            }
+            else if ( Gia_ObjIsCo(pObj) )
+            {
+                int arrTime = Vec_IntEntry( p->vArrs, Gia_ObjFaninId0(pObj, iLut) );
+                Tim_ManSetCoArrival( (Tim_Man_t*)p->pGia->pManTime, Gia_ObjCioId(pObj), arrTime );
+            }
+            else if ( !Gia_ObjIsConst0(pObj) ) 
+                assert( 0 );
+        }
+        Vec_IntFree( vNodes );
+    }
+    else
+    {
+        Gia_ManForEachLut2( p->pGia, iLut )
+        {
+            vFanins = Gia_ObjLutFanins2(p->pGia, iLut);
+            Delay = Sbl_ManComputeDelay( p, iLut, vFanins );
+            Vec_IntWriteEntry( p->vArrs,  iLut, Delay );
+            DelayMax = Abc_MaxInt( DelayMax, Delay );
+        }
     }
     // compute required times
     Vec_IntFill( p->vReqs, Gia_ManObjNum(p->pGia), ABC_INFINITY );
     Gia_ManForEachCoDriverId( p->pGia, iLut, k )
         Vec_IntDowndateEntry( p->vReqs, iLut, DelayMax );
-    Gia_ManForEachLut2Reverse( p->pGia, iLut )
+    if ( p->pGia->pManTime != NULL && Tim_ManBoxNum((Tim_Man_t*)p->pGia->pManTime) )
     {
-        Delay = Vec_IntEntry(p->vReqs, iLut) - 1;
-        vFanins = Gia_ObjLutFanins2(p->pGia, iLut);
-        Vec_IntForEachEntry( vFanins, iFan, k )
-            Vec_IntDowndateEntry( p->vReqs, iFan, Delay );
+        Gia_Obj_t * pObj; 
+        Vec_Int_t * vNodes = Gia_ManOrderWithBoxes( p->pGia );
+        Tim_ManIncrementTravId( (Tim_Man_t*)p->pGia->pManTime );
+        Tim_ManInitPoRequiredAll( (Tim_Man_t*)p->pGia->pManTime, DelayMax );
+        Gia_ManForEachObjVecReverse( vNodes, p->pGia, pObj, k )
+        {
+            iLut = Gia_ObjId( p->pGia, pObj );
+            if ( Gia_ObjIsAnd(pObj) )
+            {
+                if ( Gia_ObjIsLut2(p->pGia, iLut) )
+                {
+                    Delay = Vec_IntEntry(p->vReqs, iLut) - 1;
+                    vFanins = Gia_ObjLutFanins2(p->pGia, iLut);
+                    Vec_IntForEachEntry( vFanins, iFan, k )
+                        Vec_IntDowndateEntry( p->vReqs, iFan, Delay );
+                }
+            }
+            else if ( Gia_ObjIsCi(pObj) )
+            {
+                int reqTime = Vec_IntEntry( p->vReqs, iLut );
+                Tim_ManSetCiRequired( (Tim_Man_t*)p->pGia->pManTime, Gia_ObjCioId(pObj), reqTime );
+            }
+            else if ( Gia_ObjIsCo(pObj) )
+            {
+                int reqTime = Tim_ManGetCoRequired( (Tim_Man_t*)p->pGia->pManTime, Gia_ObjCioId(pObj) );
+                Vec_IntWriteEntry( p->vReqs, Gia_ObjFaninId0(pObj, iLut), reqTime );
+            }
+            else if ( !Gia_ObjIsConst0(pObj) ) 
+                assert( 0 );
+        }
+        Vec_IntFree( vNodes );
+    }
+    else
+    {
+        Gia_ManForEachLut2Reverse( p->pGia, iLut )
+        {
+            Delay = Vec_IntEntry(p->vReqs, iLut) - 1;
+            vFanins = Gia_ObjLutFanins2(p->pGia, iLut);
+            Vec_IntForEachEntry( vFanins, iFan, k )
+                Vec_IntDowndateEntry( p->vReqs, iFan, Delay );
+        }
     }
     return DelayMax;
 }
 
+
 /**Function*************************************************************
 
   Synopsis    [Given mapping in p->vSolCur, check if mapping meets delay.]
@@ -379,7 +454,7 @@ int Sbl_ManEvaluateMapping( Sbl_Man_t * p, int DelayGlo )
 {
     abctime clk = Abc_Clock();
     Vec_Int_t * vFanins;
-    int i, iLut, iAnd, Delay, Required;
+    int i, iLut = -1, iAnd, Delay, Required;
     if ( p->pGia->vEdge1 )
         return Sbl_ManEvaluateMappingEdge( p, DelayGlo );
     Vec_IntClear( p->vPath );

src/aig/gia/giaSweep.c

@@ -421,6 +421,7 @@ void Gia_ManCheckIntegrityWithBoxes( Gia_Man_t * p )
     int i, nCountReg = 0, nCountCarry = 0;
     if ( p->pManTime == NULL )
         return;
+    ABC_FREE( p->pRefs );
     Gia_ManCreateRefs( p );
     for ( i = Gia_ManPoNum(p) - Gia_ManRegBoxNum(p); i < Gia_ManPoNum(p); i++ )
     {

src/base/abci/abc.c

@@ -34862,6 +34862,11 @@ int Abc_CommandAbc9Edge( Abc_Frame_t * pAbc, int argc, char ** argv )
         Abc_Print( 0, "Current AIG has mapping into %d-LUTs.\n", Gia_ManLutSizeMax(pAbc->pGia) );
         return 0;
     }
+    if ( pAbc->pGia->pManTime && fReverse )
+    {
+        Abc_Print( 0, "Reverse computation does not work when boxes are present.\n" );
+        return 0;
+    }
     if ( fReverse )
         DelayMax = Gia_ManComputeEdgeDelay2( pAbc->pGia );
     else