Version abc70706

9 files changed, 210 insertions, 62 deletions

diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index 53566b7d..cd67205c 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -2805,7 +2805,7 @@ int Abc_CommandImfs( Abc_Frame_t * pAbc, int argc, char ** argv )
 
     // set defaults
     pPars->nWindow      = 62;
-    pPars->nGrowthLevel =  3;
+    pPars->nGrowthLevel =  1;
     pPars->nCands       =  5;
     pPars->nSimWords    =  4;
     pPars->fArea        =  0;
@@ -2936,13 +2936,14 @@ int Abc_CommandLutpack( Abc_Frame_t * pAbc, int argc, char ** argv )
     pPars->nLutsMax     =  4; // (N) the maximum number of LUTs in the structure
     pPars->nLutsOver    =  3; // (Q) the maximum number of LUTs not in the MFFC
     pPars->nVarsShared  =  0; // (S) the maximum number of shared variables (crossbars)
-    pPars->nGrowthLevel =  9; // (L) the maximum number of increased levels
+    pPars->nGrowthLevel =  1; // (L) the maximum number of increased levels
     pPars->fSatur       =  1;
     pPars->fZeroCost    =  0; 
-    pPars->fVerbose     =  1;
+    pPars->fFirst       =  0;
+    pPars->fVerbose     =  0;
     pPars->fVeryVerbose =  0;
     Extra_UtilGetoptReset();
-    while ( ( c = Extra_UtilGetopt( argc, argv, "NQSLszvwh" ) ) != EOF )
+    while ( ( c = Extra_UtilGetopt( argc, argv, "NQSLszfvwh" ) ) != EOF )
     {
         switch ( c )
         {
@@ -2996,6 +2997,9 @@ int Abc_CommandLutpack( Abc_Frame_t * pAbc, int argc, char ** argv )
         case 'z':
             pPars->fZeroCost ^= 1;
             break;
+        case 'f':
+            pPars->fFirst ^= 1;
+            break;
         case 'v':
             pPars->fVerbose ^= 1;
             break;
@@ -3029,7 +3033,7 @@ int Abc_CommandLutpack( Abc_Frame_t * pAbc, int argc, char ** argv )
     return 0;
 
 usage:
-    fprintf( pErr, "usage: lutpack [-N <num>] [-Q <num>] [-S <num>] [-L <num>] [-szvwh]\n" );
+    fprintf( pErr, "usage: lutpack [-N <num>] [-Q <num>] [-S <num>] [-L <num>] [-szfvwh]\n" );
     fprintf( pErr, "\t           performs \"rewriting\" for LUT networks\n" );
     fprintf( pErr, "\t-N <num> : the max number of LUTs in the structure (2 <= num) [default = %d]\n", pPars->nLutsMax );
     fprintf( pErr, "\t-Q <num> : the max number of LUTs not in MFFC (0 <= num) [default = %d]\n", pPars->nLutsOver );
@@ -3037,6 +3041,7 @@ usage:
     fprintf( pErr, "\t-L <num> : the largest increase in node level after resynthesis (0 <= num) [default = %d]\n", pPars->nGrowthLevel );
     fprintf( pErr, "\t-s       : toggle iteration till saturation [default = %s]\n", pPars->fSatur? "yes": "no" );
     fprintf( pErr, "\t-z       : toggle zero-cost replacements [default = %s]\n", pPars->fZeroCost? "yes": "no" );
+    fprintf( pErr, "\t-f       : toggle using only first node and first cut [default = %s]\n", pPars->fFirst? "yes": "no" );
     fprintf( pErr, "\t-v       : toggle verbose printout [default = %s]\n", pPars->fVerbose? "yes": "no" );
     fprintf( pErr, "\t-w       : toggle printout subgraph statistics [default = %s]\n", pPars->fVeryVerbose? "yes": "no" );
     fprintf( pErr, "\t-h       : print the command usage\n");
diff --git a/src/base/abci/abcBalance.c b/src/base/abci/abcBalance.c
index f55dc435..f9b3384e 100644
--- a/src/base/abci/abcBalance.c
+++ b/src/base/abci/abcBalance.c
@@ -55,7 +55,7 @@ Abc_Ntk_t * Abc_NtkBalance( Abc_Ntk_t * pNtk, bool fDuplicate, bool fSelective,
     // compute the required times
     if ( fSelective )
     {
-        Abc_NtkStartReverseLevels( pNtk );
+        Abc_NtkStartReverseLevels( pNtk, 0 );
         Abc_NtkMarkCriticalNodes( pNtk );
     }
     // perform balancing
@@ -600,7 +600,7 @@ void Abc_NtkMarkCriticalNodes( Abc_Ntk_t * pNtk )
     Abc_Obj_t * pNode;
     int i, Counter = 0;
     Abc_NtkForEachNode( pNtk, pNode, i )
-        if ( Abc_NodeReadRequiredLevel(pNode) - pNode->Level <= 1 )
+        if ( Abc_ObjRequiredLevel(pNode) - pNode->Level <= 1 )
             pNode->fMarkA = 1, Counter++;
     printf( "The number of nodes on the critical paths = %6d  (%5.2f %%)\n", Counter, 100.0 * Counter / Abc_NtkNodeNum(pNtk) );
 }
diff --git a/src/base/abci/abcIf.c b/src/base/abci/abcIf.c
index 074b8ae8..a9c42ceb 100644
--- a/src/base/abci/abcIf.c
+++ b/src/base/abci/abcIf.c
@@ -263,10 +263,7 @@ Abc_Obj_t * Abc_NodeFromIf_rec( Abc_Ntk_t * pNtkNew, If_Man_t * pIfMan, If_Obj_t
             Abc_ObjAddFanin( pNodeNew, Abc_NodeFromIf_rec(pNtkNew, pIfMan, pIfLeaf, vCover) );
     }
     // set the level of the new node
-    {
-        extern int Res_UpdateNetworkLevelNew( Abc_Obj_t * pObj );
-        pNodeNew->Level = Res_UpdateNetworkLevelNew( pNodeNew );
-    }
+    pNodeNew->Level = Abc_ObjLevelNew( pNodeNew );
     // derive the function of this node
     if ( pIfMan->pPars->fTruth )
     {
diff --git a/src/base/abci/abcRefactor.c b/src/base/abci/abcRefactor.c
index 872ffaf0..210c0534 100644
--- a/src/base/abci/abcRefactor.c
+++ b/src/base/abci/abcRefactor.c
@@ -100,7 +100,7 @@ int Abc_NtkRefactor( Abc_Ntk_t * pNtk, int nNodeSizeMax, int nConeSizeMax, bool
     pManRef->vLeaves   = Abc_NtkManCutReadCutLarge( pManCut );
     // compute the reverse levels if level update is requested
     if ( fUpdateLevel )
-        Abc_NtkStartReverseLevels( pNtk );
+        Abc_NtkStartReverseLevels( pNtk, 0 );
 
     // resynthesize each node once
     nNodes = Abc_NtkObjNumMax(pNtk);
@@ -187,7 +187,7 @@ Dec_Graph_t * Abc_NodeRefactor( Abc_ManRef_t * p, Abc_Obj_t * pNode, Vec_Ptr_t *
     char * pSop;
     int Required;
 
-    Required = fUpdateLevel? Abc_NodeReadRequiredLevel(pNode) : ABC_INFINITY;
+    Required = fUpdateLevel? Abc_ObjRequiredLevel(pNode) : ABC_INFINITY;
 
     p->nNodesConsidered++;
 
diff --git a/src/base/abci/abcRestruct.c b/src/base/abci/abcRestruct.c
index b9ffd932..326d1543 100644
--- a/src/base/abci/abcRestruct.c
+++ b/src/base/abci/abcRestruct.c
@@ -114,7 +114,7 @@ int Abc_NtkRestructure( Abc_Ntk_t * pNtk, int nCutMax, bool fUpdateLevel, bool f
 
     // compute the reverse levels if level update is requested
     if ( fUpdateLevel )
-        Abc_NtkStartReverseLevels( pNtk );
+        Abc_NtkStartReverseLevels( pNtk, 0 );
 
     // start the restructuring manager
     pManRst = Abc_NtkManRstStart( nCutMax, fUpdateLevel, fUseZeros, fVerbose );
@@ -324,7 +324,7 @@ Dec_Graph_t * Abc_NodeRestructureCut( Abc_ManRst_t * p, Abc_Obj_t * pRoot, Cut_C
     p->nCutsConsidered++;
 
     // get the required time for the node
-    Required = p->fUpdateLevel? Abc_NodeReadRequiredLevel(pRoot) : ABC_INFINITY;
+    Required = p->fUpdateLevel? Abc_ObjRequiredLevel(pRoot) : ABC_INFINITY;
 
     // collect the leaves of the cut
     Vec_PtrClear( p->vLeaves );
diff --git a/src/base/abci/abcResub.c b/src/base/abci/abcResub.c
index 243548fa..a954f2ce 100644
--- a/src/base/abci/abcResub.c
+++ b/src/base/abci/abcResub.c
@@ -159,7 +159,7 @@ int Abc_NtkResubstitute( Abc_Ntk_t * pNtk, int nCutMax, int nStepsMax, int nLeve
 
     // compute the reverse levels if level update is requested
     if ( fUpdateLevel )
-        Abc_NtkStartReverseLevels( pNtk );
+        Abc_NtkStartReverseLevels( pNtk, 0 );
 
     if ( Abc_NtkLatchNum(pNtk) )
         Abc_NtkForEachLatch(pNtk, pNode, i)
@@ -1617,7 +1617,7 @@ Dec_Graph_t * Abc_ManResubEval( Abc_ManRes_t * p, Abc_Obj_t * pRoot, Vec_Ptr_t *
     int Required;
     int clk;
 
-    Required = fUpdateLevel? Abc_NodeReadRequiredLevel(pRoot) : ABC_INFINITY;
+    Required = fUpdateLevel? Abc_ObjRequiredLevel(pRoot) : ABC_INFINITY;
 
     assert( nSteps >= 0 );
     assert( nSteps <= 3 );
diff --git a/src/base/abci/abcRewrite.c b/src/base/abci/abcRewrite.c
index 3d06dddf..7760b2d1 100644
--- a/src/base/abci/abcRewrite.c
+++ b/src/base/abci/abcRewrite.c
@@ -83,7 +83,7 @@ int Abc_NtkRewrite( Abc_Ntk_t * pNtk, int fUpdateLevel, int fUseZeros, int fVerb
         return 0;
     // compute the reverse levels if level update is requested
     if ( fUpdateLevel )
-        Abc_NtkStartReverseLevels( pNtk );
+        Abc_NtkStartReverseLevels( pNtk, 0 );
     // start the cut manager
 clk = clock();
     pManCut = Abc_NtkStartCutManForRewrite( pNtk );
diff --git a/src/base/abci/abcTiming.c b/src/base/abci/abcTiming.c
index 93fa3fa5..fd54f519 100644
--- a/src/base/abci/abcTiming.c
+++ b/src/base/abci/abcTiming.c
@@ -630,39 +630,133 @@ void Abc_NodeDelayTraceArrival( Abc_Obj_t * pNode )
 
 /**Function*************************************************************
 
-  Synopsis    [Prepares the AIG for the comptuation of required levels.]
+  Synopsis    [Computes the level of the node using its fanin levels.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Abc_ObjLevelNew( Abc_Obj_t * pObj )
+{
+    Abc_Obj_t * pFanin;
+    int i, Level = 0;
+    Abc_ObjForEachFanin( pObj, pFanin, i )
+        Level = ABC_MAX( Level, Abc_ObjLevel(pFanin) );
+    return Level + 1;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Computes the reverse level of the node using its fanout levels.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Abc_ObjReverseLevelNew( Abc_Obj_t * pObj )
+{
+    Abc_Obj_t * pFanout;
+    int i, LevelCur, Level = 0;
+    Abc_ObjForEachFanout( pObj, pFanout, i )
+    {
+        LevelCur = Abc_ObjReverseLevel( pFanout );
+        Level = ABC_MAX( Level, LevelCur );
+    }
+    return Level + 1;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Returns required level of the node.]
+
+  Description [Converts the reverse levels of the node into its required 
+  level as follows: ReqLevel(Node) = MaxLevels(Ntk) + 1 - LevelR(Node).]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Abc_ObjRequiredLevel( Abc_Obj_t * pObj )
+{
+    Abc_Ntk_t * pNtk = pObj->pNtk;
+    assert( pNtk->vLevelsR );
+    return pNtk->LevelMax + 1 - Abc_ObjReverseLevel(pObj);
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Returns the reverse level of the node.]
+
+  Description [The reverse level is the level of the node in reverse
+  topological order, starting from the COs.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Abc_ObjReverseLevel( Abc_Obj_t * pObj )
+{
+    Abc_Ntk_t * pNtk = pObj->pNtk;
+    assert( pNtk->vLevelsR );
+    Vec_IntFillExtra( pNtk->vLevelsR, pObj->Id + 1, 0 );
+    return Vec_IntEntry(pNtk->vLevelsR, pObj->Id);
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Sets the reverse level of the node.]
+
+  Description [The reverse level is the level of the node in reverse
+  topological order, starting from the COs.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Abc_ObjSetReverseLevel( Abc_Obj_t * pObj, int LevelR )
+{
+    Abc_Ntk_t * pNtk = pObj->pNtk;
+    assert( pNtk->vLevelsR );
+    Vec_IntFillExtra( pNtk->vLevelsR, pObj->Id + 1, 0 );
+    Vec_IntWriteEntry( pNtk->vLevelsR, pObj->Id, LevelR );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Prepares for the computation of required levels.]
 
   Description [This procedure should be called before the required times
   are used. It starts internal data structures, which records the level 
-  from the COs of the AIG nodes in reverse topologogical order.]
+  from the COs of the network nodes in reverse topologogical order.]
                
   SideEffects []
 
   SeeAlso     []
 
 ***********************************************************************/
-void Abc_NtkStartReverseLevels( Abc_Ntk_t * pNtk )
+void Abc_NtkStartReverseLevels( Abc_Ntk_t * pNtk, int nMaxLevelIncrease )
 {
     Vec_Ptr_t * vNodes;
-    Abc_Obj_t * pObj, * pFanout;
-    int i, k, nLevelsCur;
-//    assert( Abc_NtkIsStrash(pNtk) );
+    Abc_Obj_t * pObj;
+    int i;
     // remember the maximum number of direct levels
-//    pNtk->LevelMax = Abc_AigLevel(pNtk);
-    pNtk->LevelMax = Abc_NtkLevel(pNtk);
+    pNtk->LevelMax = Abc_NtkLevel(pNtk) + nMaxLevelIncrease;
     // start the reverse levels
     pNtk->vLevelsR = Vec_IntAlloc( 0 );
-    Vec_IntFill( pNtk->vLevelsR, Abc_NtkObjNumMax(pNtk), 0 );
+    Vec_IntFill( pNtk->vLevelsR, 1 + Abc_NtkObjNumMax(pNtk), 0 );
     // compute levels in reverse topological order
     vNodes = Abc_NtkDfsReverse( pNtk );
     Vec_PtrForEachEntry( vNodes, pObj, i )
-    {
-        nLevelsCur = 0;
-        Abc_ObjForEachFanout( pObj, pFanout, k )
-            if ( nLevelsCur < Vec_IntEntry(pNtk->vLevelsR, pFanout->Id) )
-                nLevelsCur = Vec_IntEntry(pNtk->vLevelsR, pFanout->Id);
-        Vec_IntWriteEntry( pNtk->vLevelsR, pObj->Id, nLevelsCur + 1 );
-    }
+        Abc_ObjSetReverseLevel( pObj, Abc_ObjReverseLevelNew(pObj) );
     Vec_PtrFree( vNodes );
 }
 
@@ -688,64 +782,116 @@ void Abc_NtkStopReverseLevels( Abc_Ntk_t * pNtk )
 
 /**Function*************************************************************
 
-  Synopsis    [Sets the reverse level of the node.]
+  Synopsis    [Incrementally updates level of the nodes.]
 
-  Description [The reverse level is the level of the node in reverse
-  topological order, starting from the COs.]
+  Description []
                
   SideEffects []
 
   SeeAlso     []
 
 ***********************************************************************/
-void Abc_NodeSetReverseLevel( Abc_Obj_t * pObj, int LevelR )
+void Abc_NtkUpdateLevel( Abc_Obj_t * pObjNew, Vec_Vec_t * vLevels )
 {
-    Abc_Ntk_t * pNtk = pObj->pNtk;
-    assert( Abc_NtkIsStrash(pNtk) );
-    assert( pNtk->vLevelsR );
-    Vec_IntFillExtra( pNtk->vLevelsR, pObj->Id + 1, 0 );
-    Vec_IntWriteEntry( pNtk->vLevelsR, pObj->Id, LevelR );
+    Abc_Obj_t * pFanout, * pTemp;
+    int LevelOld, Lev, k, m;
+    // check if level has changed
+    LevelOld = Abc_ObjLevel(pObjNew);
+    if ( LevelOld == Abc_ObjLevelNew(pObjNew) )
+        return;
+    // start the data structure for level update
+    // we cannot fail to visit a node when using this structure because the 
+    // nodes are stored by their _old_ levels, which are assumed to be correct
+    Vec_VecClear( vLevels );
+    Vec_VecPush( vLevels, LevelOld, pObjNew );
+    pObjNew->fMarkA = 1;
+    // recursively update level
+    Vec_VecForEachEntryStart( vLevels, pTemp, Lev, k, LevelOld )
+    {
+        pTemp->fMarkA = 0;
+        assert( Abc_ObjLevel(pTemp) == Lev );
+        Abc_ObjSetLevel( pTemp, Abc_ObjLevelNew(pTemp) );
+        // if the level did not change, to need to check the fanout levels
+        if ( Abc_ObjLevel(pTemp) == Lev )
+            continue;
+        // schedule fanout for level update
+        Abc_ObjForEachFanout( pTemp, pFanout, m )
+        {
+            if ( !Abc_ObjIsCo(pFanout) && !pFanout->fMarkA )
+            {
+                Vec_VecPush( vLevels, Abc_ObjLevel(pFanout), pFanout );
+                pFanout->fMarkA = 1;
+            }
+        }
+    }
 }
 
 /**Function*************************************************************
 
-  Synopsis    [Returns the reverse level of the node.]
+  Synopsis    [Incrementally updates level of the nodes.]
 
-  Description [The reverse level is the level of the node in reverse
-  topological order, starting from the COs.]
+  Description []
                
   SideEffects []
 
   SeeAlso     []
 
 ***********************************************************************/
-int Abc_NodeReadReverseLevel( Abc_Obj_t * pObj )
+void Abc_NtkUpdateReverseLevel( Abc_Obj_t * pObjNew, Vec_Vec_t * vLevels )
 {
-    Abc_Ntk_t * pNtk = pObj->pNtk;
-    assert( Abc_NtkIsStrash(pNtk) );
-    assert( pNtk->vLevelsR );
-    Vec_IntFillExtra( pNtk->vLevelsR, pObj->Id + 1, 0 );
-    return Vec_IntEntry(pNtk->vLevelsR, pObj->Id);
+    Abc_Obj_t * pFanin, * pTemp;
+    int LevelOld, Lev, k, m;
+    // check if level has changed
+    LevelOld = Abc_ObjReverseLevel(pObjNew);
+    if ( LevelOld == Abc_ObjReverseLevelNew(pObjNew) )
+        return;
+    // start the data structure for level update
+    // we cannot fail to visit a node when using this structure because the 
+    // nodes are stored by their _old_ levels, which are assumed to be correct
+    Vec_VecClear( vLevels );
+    Vec_VecPush( vLevels, LevelOld, pObjNew );
+    pObjNew->fMarkA = 1;
+    // recursively update level
+    Vec_VecForEachEntryStart( vLevels, pTemp, Lev, k, LevelOld )
+    {
+        pTemp->fMarkA = 0;
+        LevelOld = Abc_ObjReverseLevel(pTemp); 
+        assert( LevelOld == Lev );
+        Abc_ObjSetReverseLevel( pTemp, Abc_ObjReverseLevelNew(pTemp) );
+        // if the level did not change, to need to check the fanout levels
+        if ( Abc_ObjReverseLevel(pTemp) == Lev )
+            continue;
+        // schedule fanins for level update
+        Abc_ObjForEachFanin( pTemp, pFanin, m )
+        {
+            if ( !Abc_ObjIsCi(pFanin) && !pFanin->fMarkA )
+            {
+                Vec_VecPush( vLevels, Abc_ObjReverseLevel(pFanin), pFanin );
+                pFanin->fMarkA = 1;
+            }
+        }
+    }
 }
 
 /**Function*************************************************************
 
-  Synopsis    [Returns required level of the node.]
+  Synopsis    [Replaces the node and incrementally updates levels.]
 
-  Description [Converts the reverse levels of the node into its required 
-  level as follows: ReqLevel(Node) = MaxLevels(Ntk) + 1 - LevelR(Node).]
+  Description []
                
   SideEffects []
 
   SeeAlso     []
 
 ***********************************************************************/
-int Abc_NodeReadRequiredLevel( Abc_Obj_t * pObj )
+void Abc_NtkUpdate( Abc_Obj_t * pObj, Abc_Obj_t * pObjNew, Vec_Vec_t * vLevels )
 {
-    Abc_Ntk_t * pNtk = pObj->pNtk;
-    assert( Abc_NtkIsStrash(pNtk) );
-    assert( pNtk->vLevelsR );
-    return pNtk->LevelMax + 1 - Vec_IntEntry(pNtk->vLevelsR, pObj->Id);
+    // replace the old node by the new node
+    pObjNew->Level = pObj->Level;
+    Abc_ObjReplace( pObj, pObjNew );
+    // update the level of the node
+    Abc_NtkUpdateLevel( pObjNew, vLevels );
+    Abc_NtkUpdateReverseLevel( pObjNew, vLevels );
 }
 
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/base/abci/abcVerify.c b/src/base/abci/abcVerify.c
index a4c67a8b..6ab2c552 100644
--- a/src/base/abci/abcVerify.c
+++ b/src/base/abci/abcVerify.c
@@ -705,7 +705,7 @@ void Abc_NtkVerifyReportError( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int * pMode
     nErrors = 0;
     for ( i = 0; i < Abc_NtkCoNum(pNtk1); i++ )
         nErrors += (int)( pValues1[i] != pValues2[i] );
-    printf( "Verification failed for %d outputs: ", nErrors );
+    printf( "Verification failed for at least %d outputs: ", nErrors );
     // print the first 3 outputs
     nPrinted = 0;
     for ( i = 0; i < Abc_NtkCoNum(pNtk1); i++ )
@@ -860,7 +860,7 @@ void Abc_NtkVerifyReportErrorSeq( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int * pM
         return;
     }
 
-    printf( "Verification failed for %d output%s of frame %d: ", nErrors, (nErrors>1? "s":""), iFrameError+1 );
+    printf( "Verification failed for at least %d output%s of frame %d: ", nErrors, (nErrors>1? "s":""), iFrameError+1 );
     // print the first 3 outputs
     nPrinted = 0;
     Abc_NtkForEachPo( pNtk1, pObj1, o )