Version abc80402

5 files changed, 38 insertions, 53 deletions

diff --git a/src/aig/mfx/mfxCore.c b/src/aig/mfx/mfxCore.c
index 4c8988cc..6e47c986 100644
--- a/src/aig/mfx/mfxCore.c
+++ b/src/aig/mfx/mfxCore.c
@@ -19,6 +19,7 @@
 ***********************************************************************/
 
 #include "mfxInt.h"
+#include "bar.h"
 
 ////////////////////////////////////////////////////////////////////////
 ///                        DECLARATIONS                              ///
@@ -83,8 +84,8 @@ p->timeWin += clock() - clk;
         return 1;
     // compute the divisors of the window
 clk = clock();
-//    p->vDivs  = Mfx_ComputeDivisors( p, pNode, Nwk_ObjRequired(pNode) - If_LutLibSlowestPinDelay(pNode->pMan->pLutLib) );
-    p->vDivs  = Mfx_ComputeDivisors( p, pNode, AIG_INFINITY );
+    p->vDivs  = Mfx_ComputeDivisors( p, pNode, Nwk_ObjRequired(pNode) - If_LutLibSlowestPinDelay(pNode->pMan->pLutLib) );
+//    p->vDivs  = Mfx_ComputeDivisors( p, pNode, AIG_INFINITY );
     p->nTotalDivs += Vec_PtrSize(p->vDivs);
 p->timeDiv += clock() - clk;
     // construct AIG for the window
@@ -192,10 +193,10 @@ p->timeSat += clock() - clk;
   SeeAlso     []
 
 ***********************************************************************/
-int Mfx_Perform( Nwk_Man_t * pNtk, Mfx_Par_t * pPars )
+int Mfx_Perform( Nwk_Man_t * pNtk, Mfx_Par_t * pPars, If_Lib_t * pLutLib )
 {
     Bdc_Par_t Pars = {0}, * pDecPars = &Pars;
-//    ProgressBar * pProgress;
+    Bar_Progress_t * pProgress;
     Mfx_Man_t * p;
     Tim_Man_t * pManTimeOld = NULL;
     Nwk_Obj_t * pObj;
@@ -223,23 +224,19 @@ int Mfx_Perform( Nwk_Man_t * pNtk, Mfx_Par_t * pPars )
             nFaninMax = MFX_FANIN_MAX;
         }
     }
-
-/*
-    // prepare timing information
-    if ( pNtk->pManTime )
+    if ( pLutLib && pLutLib->LutMax < nFaninMax )
     {
-        // compute levels
-        Nwk_ManLevel( pNtk );
-        // compute delay trace with white-boxes
-        Nwk_ManDelayTraceLut( pNtk, pNtk->pLutLib );
-        // save the general timing manager
-        pManTimeOld = pNtk->pManTime;
-        // derive an approximate timing manager without white-boxes
-        pNtk->pManTime = Tim_ManDupApprox( pNtk->pManTime );
+        printf( "The selected LUT library with max LUT size (%d) cannot be used to compute timing for network with %d-input nodes. Using unit-delay model.\n", pLutLib->LutMax, nFaninMax );
+        pLutLib = NULL;
     }
-    // compute delay trace with the given timing manager
-    Nwk_ManDelayTraceLut( pNtk, pNtk->pLutLib );
-*/
+    pNtk->pLutLib = pLutLib;
+
+    // compute levels
+    Nwk_ManLevel( pNtk );
+    assert( Nwk_ManVerifyLevel( pNtk ) );
+    // compute delay trace with white-boxes
+    Nwk_ManDelayTraceLut( pNtk );
+    assert( Nwk_ManVerifyTiming( pNtk ) );
 
     // start the manager
     p = Mfx_ManAlloc( pPars );
@@ -259,27 +256,27 @@ int Mfx_Perform( Nwk_Man_t * pNtk, Mfx_Par_t * pPars )
     p->nTotalEdgesBeg = nTotalEdgesBeg;
     if ( pPars->fResub )
     {
-//        pProgress = Extra_ProgressBarStart( stdout, Nwk_ObjNumMax(pNtk) );
+        pProgress = Bar_ProgressStart( stdout, Nwk_ManObjNumMax(pNtk) );
         Nwk_ManForEachNode( pNtk, pObj, i )
         {
             if ( p->pPars->nDepthMax && pObj->Level > p->pPars->nDepthMax )
                 continue;
             if ( Nwk_ObjFaninNum(pObj) < 2 || Nwk_ObjFaninNum(pObj) > nFaninMax )
                 continue;
-//            if ( !p->pPars->fVeryVerbose )
-//                Extra_ProgressBarUpdate( pProgress, i, NULL );
+            if ( !p->pPars->fVeryVerbose )
+                Bar_ProgressUpdate( pProgress, i, NULL );
             Mfx_Resub( p, pObj );
         }
-//        Extra_ProgressBarStop( pProgress );
+        Bar_ProgressStop( pProgress );
     }
     else
     {
-//        pProgress = Extra_ProgressBarStart( stdout, Nwk_NodeNum(pNtk) );
+        pProgress = Bar_ProgressStart( stdout, Nwk_ManNodeNum(pNtk) );
         vLevels = Nwk_ManLevelize( pNtk );
         Vec_VecForEachLevelStart( vLevels, vNodes, k, 1 )
         {
-//            if ( !p->pPars->fVeryVerbose )
-//                Extra_ProgressBarUpdate( pProgress, nNodes, NULL );
+            if ( !p->pPars->fVeryVerbose )
+                Bar_ProgressUpdate( pProgress, nNodes, NULL );
             p->nNodesGainedLevel = 0;
             p->nTotConfLevel = 0;
             p->nTimeOutsLevel = 0;
@@ -303,20 +300,15 @@ int Mfx_Perform( Nwk_Man_t * pNtk, Mfx_Par_t * pPars )
             PRT( "Time", clock() - clk2 );
             }
         }
-//        Extra_ProgressBarStop( pProgress );
+        Bar_ProgressStop( pProgress );
         Vec_VecFree( vLevels );
     }
     p->nTotalNodesEnd = Nwk_ManNodeNum(pNtk);
     p->nTotalEdgesEnd = Nwk_ManGetTotalFanins(pNtk);
-/*
-    // reset the timing manager
-    if ( pNtk->pManTime )
-    {
-        Tim_ManStop( pNtk->pManTime );
-        pNtk->pManTime = pManTimeOld;
-    }
-    Nwk_ManVerifyLevel( pNtk );
-*/
+
+    assert( Nwk_ManVerifyLevel( pNtk ) );
+    assert( Nwk_ManVerifyTiming( pNtk ) );
+
     // free the manager
     p->timeTotal = clock() - clk;
     Mfx_ManStop( p );
diff --git a/src/aig/mfx/mfxDiv.c b/src/aig/mfx/mfxDiv.c
index b7b76031..33f55ecb 100644
--- a/src/aig/mfx/mfxDiv.c
+++ b/src/aig/mfx/mfxDiv.c
@@ -88,17 +88,17 @@ Vec_Ptr_t * Abc_MfxWinMarkTfi( Nwk_Obj_t * pNode )
   SeeAlso     []
 
 ***********************************************************************/
-void Abc_MfxWinSweepLeafTfo_rec( Nwk_Obj_t * pObj, int nLevelLimit )
+void Abc_MfxWinSweepLeafTfo_rec( Nwk_Obj_t * pObj, float tArrivalMax )
 {
     Nwk_Obj_t * pFanout;
     int i;
-    if ( Nwk_ObjIsCo(pObj) || (int)pObj->Level > nLevelLimit )
+    if ( Nwk_ObjIsCo(pObj) || Nwk_ObjArrival(pObj) > tArrivalMax )
         return;
     if ( Nwk_ObjIsTravIdCurrent(pObj) )
         return;
     Nwk_ObjSetTravIdCurrent( pObj );
     Nwk_ObjForEachFanout( pObj, pFanout, i )
-        Abc_MfxWinSweepLeafTfo_rec( pFanout, nLevelLimit );
+        Abc_MfxWinSweepLeafTfo_rec( pFanout, tArrivalMax );
 }
 
 /**Function*************************************************************
@@ -187,7 +187,7 @@ int Abc_MfxWinVisitMffc( Nwk_Obj_t * pNode )
   SeeAlso     []
 
 ***********************************************************************/
-Vec_Ptr_t * Mfx_ComputeDivisors( Mfx_Man_t * p, Nwk_Obj_t * pNode, int nLevDivMax )
+Vec_Ptr_t * Mfx_ComputeDivisors( Mfx_Man_t * p, Nwk_Obj_t * pNode, float tArrivalMax )
 {
     Vec_Ptr_t * vCone, * vDivs;
     Nwk_Obj_t * pObj, * pFanout, * pFanin;
@@ -210,7 +210,7 @@ Vec_Ptr_t * Mfx_ComputeDivisors( Mfx_Man_t * p, Nwk_Obj_t * pNode, int nLevDivMa
     // (2) the MFFC of the node
     // (3) the node's fanins (these are treated as a special case)
     Nwk_ManIncrementTravId( pNode->pMan );
-    Abc_MfxWinSweepLeafTfo_rec( pNode, nLevDivMax );
+    Abc_MfxWinSweepLeafTfo_rec( pNode, tArrivalMax );
     Abc_MfxWinVisitMffc( pNode );
     Nwk_ObjForEachFanin( pNode, pObj, k )
         Nwk_ObjSetTravIdCurrent( pObj );
@@ -225,7 +225,7 @@ Vec_Ptr_t * Mfx_ComputeDivisors( Mfx_Man_t * p, Nwk_Obj_t * pNode, int nLevDivMa
     {
         if ( !Nwk_ObjIsTravIdPrevious(pObj) )
             continue;
-        if ( (int)pObj->Level > nLevDivMax )
+        if ( Nwk_ObjArrival(pObj) > tArrivalMax )
             continue;
         Vec_PtrPush( vDivs, pObj );
         if ( Vec_PtrSize(vDivs) >= p->pPars->nDivMax )
@@ -253,7 +253,7 @@ Vec_Ptr_t * Mfx_ComputeDivisors( Mfx_Man_t * p, Nwk_Obj_t * pNode, int nLevDivMa
             if ( !Nwk_ObjIsNode(pFanout) ) 
                 continue;
             // skip nodes with large level
-            if ( (int)pFanout->Level > nLevDivMax )
+            if ( Nwk_ObjArrival(pFanout) > tArrivalMax )
                 continue;
             // skip nodes whose fanins are not divisors
             Nwk_ObjForEachFanin( pFanout, pFanin, m )
diff --git a/src/aig/mfx/mfxInt.h b/src/aig/mfx/mfxInt.h
index 88792bf2..0693200d 100644
--- a/src/aig/mfx/mfxInt.h
+++ b/src/aig/mfx/mfxInt.h
@@ -125,7 +125,7 @@ struct Mfx_Man_t_
 ////////////////////////////////////////////////////////////////////////
 
 /*=== mfxDiv.c ==========================================================*/
-extern Vec_Ptr_t *      Mfx_ComputeDivisors( Mfx_Man_t * p, Nwk_Obj_t * pNode, int nLevDivMax );
+extern Vec_Ptr_t *      Mfx_ComputeDivisors( Mfx_Man_t * p, Nwk_Obj_t * pNode, float tArrivalMax );
 /*=== mfxInter.c ==========================================================*/
 extern sat_solver *     Mfx_CreateSolverResub( Mfx_Man_t * p, int * pCands, int nCands, int fInvert );
 extern Hop_Obj_t *      Mfx_Interplate( Mfx_Man_t * p, int * pCands, int nCands );
diff --git a/src/aig/mfx/mfxMan.c b/src/aig/mfx/mfxMan.c
index 1b536f8c..63531770 100644
--- a/src/aig/mfx/mfxMan.c
+++ b/src/aig/mfx/mfxMan.c
@@ -120,8 +120,8 @@ void Mfx_ManPrint( Mfx_Man_t * p )
         if ( p->pPars->fSwapEdge )
             printf( "Swappable edges = %d. Total edges = %d. Ratio = %5.2f.\n", 
                 p->nNodesResub, Nwk_ManGetTotalFanins(p->pNtk), 1.00 * p->nNodesResub / Nwk_ManGetTotalFanins(p->pNtk) );
-        else
-            Mfx_PrintResubStats( p );
+//        else
+//            Mfx_PrintResubStats( p );
 //        printf( "Average ratio of DCs in the resubed nodes = %.2f.\n", 1.0*p->nDcMints/(64 * p->nNodesResub) );
     }
     else
diff --git a/src/aig/mfx/mfxResub.c b/src/aig/mfx/mfxResub.c
index 2eafc559..7179173b 100644
--- a/src/aig/mfx/mfxResub.c
+++ b/src/aig/mfx/mfxResub.c
@@ -45,17 +45,10 @@ void Mfx_UpdateNetwork( Mfx_Man_t * p, Nwk_Obj_t * pObj, Vec_Ptr_t * vFanins, Ho
     int k;
     // create the new node
     pObjNew = Nwk_ManCreateNode( pObj->pMan, Vec_PtrSize(vFanins), Nwk_ObjFanoutNum(pObj) );
-if ( pObjNew->Id == 19969 )
-{
-    int x = 0;
-}
     pObjNew->pFunc = pFunc;
     Vec_PtrForEachEntry( vFanins, pFanin, k )
         Nwk_ObjAddFanin( pObjNew, pFanin );
     // replace the old node by the new node
-//printf( "Replacing node " ); Nwk_ObjPrint( stdout, pObj );
-//printf( "Inserting node " ); Nwk_ObjPrint( stdout, pObjNew );
-    // update the level of the node
     Nwk_ManUpdate( pObj, pObjNew, p->vLevels );
 }