Version abc80403_2

src/aig/aig/aig.h

@@ -528,7 +528,7 @@ extern Vec_Ptr_t *     Aig_ManSupportsRegisters( Aig_Man_t * p );
 extern Vec_Ptr_t *     Aig_ManPartitionSmart( Aig_Man_t * p, int nPartSizeLimit, int fVerbose, Vec_Ptr_t ** pvPartSupps );
 extern Vec_Ptr_t *     Aig_ManPartitionSmartRegisters( Aig_Man_t * pAig, int nSuppSizeLimit, int fVerbose );
 extern Vec_Ptr_t *     Aig_ManPartitionNaive( Aig_Man_t * p, int nPartSize );
-extern Vec_Ptr_t *     Aig_ManMiterPartitioned( Aig_Man_t * p1, Aig_Man_t * p2, int nPartSize );
+extern Vec_Ptr_t *     Aig_ManMiterPartitioned( Aig_Man_t * p1, Aig_Man_t * p2, int nPartSize, int fSmart );
 extern Aig_Man_t *     Aig_ManChoicePartitioned( Vec_Ptr_t * vAigs, int nPartSize, int nConfMax, int nLevelMax, int fVerbose );
 extern Aig_Man_t *     Aig_ManFraigPartitioned( Aig_Man_t * pAig, int nPartSize, int nConfMax, int nLevelMax, int fVerbose );
 extern Aig_Man_t *     Aig_ManChoiceConstructive( Vec_Ptr_t * vAigs, int fVerbose );

src/aig/aig/aigDfs.c

@@ -418,7 +418,7 @@ void Aig_ManChoiceLevel_rec( Aig_Man_t * p, Aig_Obj_t * pObj )
                 LevelMax = Aig_ObjLevel(pNext);
         }
     }
-    else
+    else if ( !Aig_ObjIsConst1(pObj) )
         assert( 0 );
     Aig_ObjSetLevel( pObj, LevelMax );
 }

src/aig/aig/aigDup.c

@@ -359,7 +359,7 @@ Aig_Man_t * Aig_ManDupDfsOrder( Aig_Man_t * p, Aig_Man_t * pOrder )
         }
     }
     Vec_PtrFree( vPios );
-    assert( Aig_ManBufNum(p) != 0 || Aig_ManNodeNum(p) == Aig_ManNodeNum(pNew) );
+//    assert( Aig_ManBufNum(p) != 0 || Aig_ManNodeNum(p) == Aig_ManNodeNum(pNew) );
     if ( p->pEquivs == NULL && p->pReprs == NULL && (nNodes = Aig_ManCleanup( pNew )) )
         printf( "Aig_ManDupDfs(): Cleanup after AIG duplication removed %d nodes.\n", nNodes );
     // duplicate the timing manager

src/aig/aig/aigMan.c

@@ -208,6 +208,7 @@ void Aig_ManStop( Aig_Man_t * p )
     if ( p->vFlopNums) Vec_IntFree( p->vFlopNums );
     if ( p->pManExdc ) Aig_ManStop( p->pManExdc );
     if ( p->vOnehots ) Vec_VecFree( (Vec_Vec_t *)p->vOnehots );
+    FREE( p->pData );
     FREE( p->pSeqModel );
     FREE( p->pName );
     FREE( p->pSpec );

src/aig/aig/aigPart.c

@@ -1092,6 +1092,63 @@ Aig_Man_t * Aig_ManDupPartAll( Aig_Man_t * pOld, Vec_Int_t * vPart )
 
 /**Function*************************************************************
 
+  Synopsis    [Collects internal nodes in the DFS order.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Aig_ManSupportNodes_rec( Aig_Man_t * p, Aig_Obj_t * pObj, Vec_Int_t * vSupport )
+{
+    if ( Aig_ObjIsTravIdCurrent(p, pObj) )
+        return;
+    Aig_ObjSetTravIdCurrent(p, pObj);
+    if ( Aig_ObjIsPi(pObj) )
+    {
+        Vec_IntPush( vSupport, Aig_ObjPioNum(pObj) );
+        return;
+    }
+    Aig_ManSupportNodes_rec( p, Aig_ObjFanin0(pObj), vSupport );
+    Aig_ManSupportNodes_rec( p, Aig_ObjFanin1(pObj), vSupport );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Collects internal nodes and PIs in the DFS order.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Vec_Ptr_t * Aig_ManSupportNodes( Aig_Man_t * p, Vec_Ptr_t * vParts )
+{
+    Vec_Ptr_t * vPartSupps;
+    Vec_Int_t * vPart, * vSupport;
+    int i, k, iOut;
+    Aig_ManSetPioNumbers( p );
+    vPartSupps = Vec_PtrAlloc( Vec_PtrSize(vParts) );
+    Vec_PtrForEachEntry( vParts, vPart, i )
+    {
+        vSupport = Vec_IntAlloc( 100 );
+        Aig_ManIncrementTravId( p );
+        Aig_ObjSetTravIdCurrent( p, Aig_ManConst1(p) );
+        Vec_IntForEachEntry( vPart, iOut, k )
+            Aig_ManSupportNodes_rec( p, Aig_ObjFanin0(Aig_ManPo(p, iOut)), vSupport );
+//        Vec_IntSort( vSupport, 0 );
+        Vec_PtrPush( vPartSupps, vSupport );
+    }
+    Aig_ManCleanPioNumbers( p );
+    return vPartSupps;
+}
+
+/**Function*************************************************************
+
   Synopsis    [Create partitioned miter of the two AIGs.]
 
   Description [Assumes that each output in the second AIG cannot have 
@@ -1102,7 +1159,7 @@ Aig_Man_t * Aig_ManDupPartAll( Aig_Man_t * pOld, Vec_Int_t * vPart )
   SeeAlso     []
 
 ***********************************************************************/
-Vec_Ptr_t * Aig_ManMiterPartitioned( Aig_Man_t * p1, Aig_Man_t * p2, int nPartSize )
+Vec_Ptr_t * Aig_ManMiterPartitioned( Aig_Man_t * p1, Aig_Man_t * p2, int nPartSize, int fSmart )
 {
     Aig_Man_t * pNew;
     Aig_Obj_t * pMiter;
@@ -1111,7 +1168,13 @@ Vec_Ptr_t * Aig_ManMiterPartitioned( Aig_Man_t * p1, Aig_Man_t * p2, int nPartSi
     Vec_Int_t * vPart, * vPartSupp;
     int i, k;
     // partition the first manager
-    vParts = Aig_ManPartitionSmart( p1, nPartSize, 0, &vPartSupps );
+    if ( fSmart )
+        vParts = Aig_ManPartitionSmart( p1, nPartSize, 0, &vPartSupps );
+    else
+    {
+        vParts = Aig_ManPartitionNaive( p1, nPartSize );
+        vPartSupps = Aig_ManSupportNodes( p1, vParts );
+    }
     // derive miters
     vMiters = Vec_PtrAlloc( Vec_PtrSize(vParts) );
     for ( i = 0; i < Vec_PtrSize(vParts); i++ )
@@ -1121,7 +1184,6 @@ Vec_Ptr_t * Aig_ManMiterPartitioned( Aig_Man_t * p1, Aig_Man_t * p2, int nPartSi
         vPartSupp = Vec_PtrEntry( vPartSupps, i );
         // create the new miter
         pNew = Aig_ManStart( 1000 );
-//        pNew->pName = Extra_UtilStrsav( p1->pName );
         // create the PIs
         for ( k = 0; k < Vec_IntSize(vPartSupp); k++ )
             Aig_ObjCreatePi( pNew );
@@ -1497,7 +1559,7 @@ void Aig_ManChoiceEval( Aig_Man_t * p )
 ***********************************************************************/
 Aig_Man_t * Aig_ManChoiceConstructive( Vec_Ptr_t * vAigs, int fVerbose )
 {
-    Aig_Man_t * pNew, * pThis, * pPrev;
+    Aig_Man_t * pNew, * pThis, * pPrev, * pTemp;
     int i;
     // start AIG with choices
     pPrev = Vec_PtrEntry( vAigs, 0 );
@@ -1514,15 +1576,18 @@ Aig_Man_t * Aig_ManChoiceConstructive( Vec_Ptr_t * vAigs, int fVerbose )
         pPrev = pThis;
     }
     // derive the result of choicing
-//Aig_ManPrintStats( pNew );
     pNew = Aig_ManRehash( pNew );
-//Aig_ManPrintStats( pNew );
     // create the equivalent nodes lists
     Aig_ManMarkValidChoices( pNew );
-//Aig_ManPrintStats( pNew );
+    // reconstruct the network
+    pNew = Aig_ManDupDfsOrder( pTemp = pNew, Vec_PtrEntry( vAigs, 0 ) );
+    Aig_ManStop( pTemp );
+    // duplicate the timing manager
+    pTemp = Vec_PtrEntry( vAigs, 0 );
+    if ( pTemp->pManTime )
+        pNew->pManTime = Tim_ManDup( pTemp->pManTime, 0 );
     // reset levels
     Aig_ManChoiceLevel( pNew );
-//    Aig_ManChoiceEval( pNew );
     return pNew;
 }
 

src/aig/dar/darBalance.c

@@ -187,7 +187,7 @@ void Dar_BalancePermute( Aig_Man_t * p, Vec_Ptr_t * vSuper, int LeftBound, int f
     // get the two last nodes
     pObj1 = Vec_PtrEntry( vSuper, RightBound + 1 );
     pObj2 = Vec_PtrEntry( vSuper, RightBound     );
-    if ( Aig_Regular(pObj1) == p->pConst1 || Aig_Regular(pObj2) == p->pConst1 )
+    if ( Aig_Regular(pObj1) == p->pConst1 || Aig_Regular(pObj2) == p->pConst1 || Aig_Regular(pObj1) == Aig_Regular(pObj2) )
         return;
     // find the first node that can be shared
     for ( i = RightBound; i >= LeftBound; i-- )

src/aig/dar/darRefact.c

@@ -376,14 +376,14 @@ int Dar_ManRefactorTryCuts( Ref_Man_t * p, Aig_Obj_t * pObj, int nNodesSaved, in
         pTruth = Aig_ManCutTruth( pObj, vCut, p->vCutNodes, p->vTruthElem, p->vTruthStore );
         if ( Kit_TruthIsConst0(pTruth, Vec_PtrSize(vCut)) )
         {
-            p->GainBest = Vec_PtrSize(p->vCutNodes);
+            p->GainBest = Aig_NodeMffsSupp( p->pAig, pObj, 0, NULL );
             p->pGraphBest = Kit_GraphCreateConst0();
             Vec_PtrCopy( p->vLeavesBest, vCut );
             return p->GainBest;
         }
         if ( Kit_TruthIsConst1(pTruth, Vec_PtrSize(vCut)) )
         {
-            p->GainBest = Vec_PtrSize(p->vCutNodes);
+            p->GainBest = Aig_NodeMffsSupp( p->pAig, pObj, 0, NULL );
             p->pGraphBest = Kit_GraphCreateConst1();
             Vec_PtrCopy( p->vLeavesBest, vCut );
             return p->GainBest;

src/aig/dar/darScript.c

@@ -82,19 +82,27 @@ Aig_Man_t * Dar_ManRwsat( Aig_Man_t * pAig, int fBalance, int fVerbose )
 
     pAig = Aig_ManDupDfs( pAig ); 
     if ( fVerbose ) Aig_ManPrintStats( pAig );
+
+    // balance
+    if ( fBalance )
+    {
+    pAig = Dar_ManBalance( pTemp = pAig, 0 );
+    Aig_ManStop( pTemp );
+    if ( fVerbose ) Aig_ManPrintStats( pAig );
+    }
     
     // rewrite
     Dar_ManRewrite( pAig, pParsRwr );
     pAig = Aig_ManDupDfs( pTemp = pAig ); 
     Aig_ManStop( pTemp );
     if ( fVerbose ) Aig_ManPrintStats( pAig );
-/*    
+
     // refactor
     Dar_ManRefactor( pAig, pParsRef );
     pAig = Aig_ManDupDfs( pTemp = pAig ); 
     Aig_ManStop( pTemp );
     if ( fVerbose ) Aig_ManPrintStats( pAig );
-*/
+
     // balance
     if ( fBalance )
     {
@@ -167,9 +175,9 @@ Aig_Man_t * Dar_ManCompress( Aig_Man_t * pAig, int fBalance, int fUpdateLevel, i
     // balance
     if ( fBalance )
     {
-//    pAig = Dar_ManBalance( pTemp = pAig, fUpdateLevel );
-//    Aig_ManStop( pTemp );
-//    if ( fVerbose ) Aig_ManPrintStats( pAig );
+    pAig = Dar_ManBalance( pTemp = pAig, fUpdateLevel );
+    Aig_ManStop( pTemp );
+    if ( fVerbose ) Aig_ManPrintStats( pAig );
     }
     
     // rewrite
@@ -239,9 +247,9 @@ Aig_Man_t * Dar_ManCompress2( Aig_Man_t * pAig, int fBalance, int fUpdateLevel,
     // balance
     if ( fBalance )
     {
-//    pAig = Dar_ManBalance( pTemp = pAig, fUpdateLevel );
-//    Aig_ManStop( pTemp );
-//    if ( fVerbose ) Aig_ManPrintStats( pAig );
+    pAig = Dar_ManBalance( pTemp = pAig, fUpdateLevel );
+    Aig_ManStop( pTemp );
+    if ( fVerbose ) Aig_ManPrintStats( pAig );
     }
     
 
@@ -336,7 +344,7 @@ Vec_Ptr_t * Dar_ManChoiceSynthesis( Aig_Man_t * pAig, int fBalance, int fUpdateL
     Aig_ManForEachObj( pAig, pObj, i )
         pObj->pHaig = pObj;
 
-    pAig = Dar_ManCompress (pAig, 0, fUpdateLevel, fVerbose);
+    pAig = Dar_ManCompress (pAig, fBalance, fUpdateLevel, fVerbose);
     Vec_PtrPush( vAigs, pAig );
 //Aig_ManPrintStats( pAig );
 

src/aig/fra/fra.h

@@ -258,7 +258,7 @@ static inline int          Fra_ImpCreate( int Left, int Right )
 /*=== fraCec.c ========================================================*/
 extern int                 Fra_FraigSat( Aig_Man_t * pMan, sint64 nConfLimit, sint64 nInsLimit, int fVerbose );
 extern int                 Fra_FraigCec( Aig_Man_t ** ppAig, int fVerbose );
-extern int                 Fra_FraigCecPartitioned( Aig_Man_t * pMan1, Aig_Man_t * pMan2, int nPartSize, int fVerbose );
+extern int                 Fra_FraigCecPartitioned( Aig_Man_t * pMan1, Aig_Man_t * pMan2, int nPartSize, int fSmart, int fVerbose );
 /*=== fraClass.c ========================================================*/
 extern int                 Fra_BmcNodeIsConst( Aig_Obj_t * pObj );
 extern int                 Fra_BmcNodesAreEqual( Aig_Obj_t * pObj0, Aig_Obj_t * pObj1 );

src/aig/fra/fraCec.c

@@ -166,8 +166,7 @@ PRT( "Time", clock() - clk );
 
     // duplicate the AIG
 clk = clock();
-//    pAig = Aig_ManDupDfs( pTemp = pAig );
-    pAig = Dar_ManRwsat( pTemp = pAig, 0, 0 );
+    pAig = Dar_ManRwsat( pTemp = pAig, 1, 0 );
     Aig_ManStop( pTemp );
     if ( fVerbose )
     {
@@ -247,22 +246,25 @@ PRT( "Time", clock() - clk );
   SeeAlso     []
 
 ***********************************************************************/
-int Fra_FraigCecPartitioned( Aig_Man_t * pMan1, Aig_Man_t * pMan2, int nPartSize, int fVerbose )
+int Fra_FraigCecPartitioned( Aig_Man_t * pMan1, Aig_Man_t * pMan2, int nPartSize, int fSmart, int fVerbose )
 {
     Aig_Man_t * pAig;
     Vec_Ptr_t * vParts;
     int i, RetValue = 1, nOutputs;
     // create partitions
-    vParts = Aig_ManMiterPartitioned( pMan1, pMan2, nPartSize );
+    vParts = Aig_ManMiterPartitioned( pMan1, pMan2, nPartSize, fSmart );
     // solve the partitions
     nOutputs = -1;
     Vec_PtrForEachEntry( vParts, pAig, i )
     {
         nOutputs++;
         if ( fVerbose )
+        {
             printf( "Verifying part %4d  (out of %4d)  PI = %5d. PO = %5d. And = %6d. Lev = %4d.\r", 
                 i+1, Vec_PtrSize(vParts), Aig_ManPiNum(pAig), Aig_ManPoNum(pAig), 
                 Aig_ManNodeNum(pAig), Aig_ManLevelNum(pAig) );
+            fflush( stdout );
+        }
         RetValue = Fra_FraigMiterStatus( pAig );
         if ( RetValue == 1 )
             continue;
@@ -306,8 +308,9 @@ int Fra_FraigCecPartitioned( Aig_Man_t * pMan1, Aig_Man_t * pMan2, int nPartSize
   SeeAlso     []
 
 ***********************************************************************/
-int Fra_FraigCecTop( Aig_Man_t * pMan1, Aig_Man_t * pMan2, int nConfLimit, int fPartition, int fVerbose )
+int Fra_FraigCecTop( Aig_Man_t * pMan1, Aig_Man_t * pMan2, int nConfLimit, int nPartSize, int fSmart, int fVerbose )
 {
+    Aig_Man_t * pTemp;
     //Abc_NtkDarCec( pNtk1, pNtk2, fPartition, fVerbose );
     int RetValue, clkTotal = clock();
 
@@ -324,10 +327,19 @@ int Fra_FraigCecTop( Aig_Man_t * pMan1, Aig_Man_t * pMan2, int nConfLimit, int f
     assert( Aig_ManPiNum(pMan1) == Aig_ManPiNum(pMan1) );
     assert( Aig_ManPoNum(pMan1) == Aig_ManPoNum(pMan1) );
 
-    if ( fPartition )
-        RetValue = Fra_FraigCecPartitioned( pMan1, pMan2, 100, fVerbose );
-    else
-        RetValue = Fra_FraigCecPartitioned( pMan1, pMan2, Aig_ManPoNum(pMan1), fVerbose );
+    // make sure that the first miter has more nodes
+    if ( Aig_ManNodeNum(pMan1) < Aig_ManNodeNum(pMan2) )
+    {
+        pTemp = pMan1;
+        pMan1 = pMan2;
+        pMan2 = pTemp;
+    }
+    assert( Aig_ManNodeNum(pMan1) >= Aig_ManNodeNum(pMan2) );
+
+    if ( nPartSize )
+        RetValue = Fra_FraigCecPartitioned( pMan1, pMan2, nPartSize, fSmart, fVerbose );
+    else // no partitioning
+        RetValue = Fra_FraigCecPartitioned( pMan1, pMan2, Aig_ManPoNum(pMan1), 0, fVerbose );
 
     // report the miter
     if ( RetValue == 1 )

src/aig/mfx/mfxCore.c

@@ -312,6 +312,10 @@ int Mfx_Perform( Nwk_Man_t * pNtk, Mfx_Par_t * pPars, If_Lib_t * pLutLib )
     // free the manager
     p->timeTotal = clock() - clk;
     Mfx_ManStop( p );
+
+    // update network into the topological order
+//    if ( pPars->fResub )
+//        Nwk_ManTopological( pNtk );
     return 1;
 }
 

src/aig/ntl/ntlExtract.c

@@ -387,7 +387,7 @@ int Ntl_ManExtract_rec( Ntl_Man_t * p, Ntl_Net_t * pNet )
     // add box inputs/outputs to COs/CIs
     if ( Ntl_ObjIsBox(pObj) )
     {
-        int LevelCur, LevelMax = -AIG_INFINITY;
+        int LevelCur, LevelMax = -TIME_ETERNITY;
         Vec_IntPush( p->vBox1Cos, Aig_ManPoNum(p->pAig) );
         Ntl_ObjForEachFanin( pObj, pNetFanin, i )
         {

src/aig/ntl/ntlInsert.c

@@ -137,6 +137,7 @@ int Ntl_ManInsert( Ntl_Man_t * p, Vec_Ptr_t * vMapping, Aig_Man_t * pAig )
 int Ntl_ManInsertNtk( Ntl_Man_t * p, Nwk_Man_t * pNtk )
 {
     char Buffer[100];
+    Vec_Ptr_t * vObjs;
     Vec_Int_t * vTruth;
     Vec_Int_t * vCover;
     Ntl_Mod_t * pRoot;
@@ -160,8 +161,13 @@ int Ntl_ManInsertNtk( Ntl_Man_t * p, Nwk_Man_t * pNtk )
     vTruth = Vec_IntAlloc( 1 << 16 );
     vCover = Vec_IntAlloc( 1 << 16 );
     nDigits = Aig_Base10Log( Nwk_ManNodeNum(pNtk) );
-    Nwk_ManForEachNode( pNtk, pObj, i )
+//    Nwk_ManForEachObj( pNtk, pObj, i )
+    vObjs = Nwk_ManDfs( pNtk );
+    Vec_PtrForEachEntry( vObjs, pObj, i )
+//    Nwk_ManForEachNode( pNtk, pObj, i )
     {
+        if ( !Nwk_ObjIsNode(pObj) )
+            continue;
         pNode = Ntl_ModelCreateNode( pRoot, Nwk_ObjFaninNum(pObj) );
         pTruth = Hop_ManConvertAigToTruth( pNtk->pManHop, Hop_Regular(pObj->pFunc), Nwk_ObjFaninNum(pObj), vTruth, 0 );
         if ( Hop_IsComplement(pObj->pFunc) )
@@ -194,6 +200,7 @@ int Ntl_ManInsertNtk( Ntl_Man_t * p, Nwk_Man_t * pNtk )
         }
         pObj->pCopy = pNet;
     }
+    Vec_PtrFree( vObjs );
     Vec_IntFree( vCover );
     Vec_IntFree( vTruth );
     // mark CIs and outputs of the registers

src/aig/ntl/ntlReadBlif.c

@@ -974,9 +974,9 @@ static int Ioa_ReadParseLineTimes( Ioa_ReadMod_t * p, char * pLine, int fOutput
     // find the delay number
     pTokenNum = Vec_PtrEntryLast(vTokens);
     if ( !strcmp( pTokenNum, "-inf" ) )
-        Delay = -AIG_INFINITY;
+        Delay = -TIME_ETERNITY;
     else if ( !strcmp( pTokenNum, "inf" ) ) 
-        Delay = AIG_INFINITY;
+        Delay = TIME_ETERNITY;
     else
         Delay = atof( pTokenNum );
     if ( Delay == 0.0 && pTokenNum[0] != '0' )

src/aig/nwk/nwkBidec.c

@@ -88,6 +88,11 @@ void Nwk_ManBidecResyn( Nwk_Man_t * pNtk, int fVerbose )
     int clk = clock();
     pPars->nVarsMax = Nwk_ManGetFaninMax( pNtk );
     pPars->fVerbose = fVerbose;
+    if ( pPars->nVarsMax < 2 )
+    {
+        printf( "Resynthesis is not performed for networks whose nodes are less than 2 inputs.\n" );
+        return;
+    }
     if ( pPars->nVarsMax > 15 )
     {
         if ( fVerbose )

src/aig/nwk/nwkMap.c

@@ -52,7 +52,7 @@ void Nwk_ManSetIfParsDefault( If_Par_t * pPars )
     pPars->nFlowIters  =  1;
     pPars->nAreaIters  =  2;
     pPars->DelayTarget = -1;
-    pPars->Epsilon     =  (float)0.01;
+    pPars->Epsilon     =  (float)0.001;
     pPars->fPreprocess =  1;
     pPars->fArea       =  0;
     pPars->fFancy      =  0;

src/aig/nwk/nwkStrash.c

@@ -95,7 +95,8 @@ Aig_Obj_t * Nwk_ManStrashNode( Aig_Man_t * p, Nwk_Obj_t * pObj )
 ***********************************************************************/
 Aig_Man_t * Nwk_ManStrash( Nwk_Man_t * pNtk )
 {
-    Aig_Man_t * pMan;//, * pTemp;
+    Vec_Ptr_t * vObjs;
+    Aig_Man_t * pMan;
     Aig_Obj_t * pObjNew;
     Nwk_Obj_t * pObj;
     int i, Level;
@@ -105,6 +106,10 @@ Aig_Man_t * Nwk_ManStrash( Nwk_Man_t * pNtk )
     pMan->pManTime = Tim_ManDup( pNtk->pManTime, 1 );
     Tim_ManIncrementTravId( pMan->pManTime );
     Nwk_ManForEachObj( pNtk, pObj, i )
+        pObj->pCopy = NULL;
+//    Nwk_ManForEachObj( pNtk, pObj, i )
+    vObjs = Nwk_ManDfs( pNtk );
+    Vec_PtrForEachEntry( vObjs, pObj, i )
     {
         if ( Nwk_ObjIsCi(pObj) )
         {
@@ -126,9 +131,8 @@ Aig_Man_t * Nwk_ManStrash( Nwk_Man_t * pNtk )
             assert( 0 );
         pObj->pCopy = pObjNew;
     }
+    Vec_PtrFree( vObjs );
     Aig_ManCleanup( pMan );
-//    pMan = Aig_ManDupOrdered( pTemp = pMan );
-//    Aig_ManStop( pTemp );
     return pMan;
 }
 

src/aig/nwk/nwkTiming.c

@@ -17,7 +17,7 @@
   Revision    [$Id: nwkTiming.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
 
 ***********************************************************************/
-
+ 
 #include "nwk.h"
 
 ////////////////////////////////////////////////////////////////////////
@@ -46,7 +46,7 @@ void Nwk_ManCleanTiming( Nwk_Man_t * pNtk )
     Nwk_ManForEachObj( pNtk, pObj, i )
     {
         pObj->tArrival = pObj->tSlack = 0.0;
-        pObj->tRequired = AIG_INFINITY;
+        pObj->tRequired = TIME_ETERNITY;
     }
 }
 
@@ -138,7 +138,7 @@ float Nwk_NodeComputeArrival( Nwk_Obj_t * pObj, int fUseSorting )
         return Nwk_ObjArrival(pObj);
     if ( Nwk_ObjIsCo(pObj) )
         return Nwk_ObjArrival( Nwk_ObjFanin0(pObj) );
-    tArrival = -AIG_INFINITY;
+    tArrival = -TIME_ETERNITY;
     if ( pLutLib == NULL )
     {
         Nwk_ObjForEachFanin( pObj, pFanin, k )
@@ -196,7 +196,7 @@ float Nwk_NodeComputeRequired( Nwk_Obj_t * pObj, int fUseSorting )
     assert( Nwk_ObjIsNode(pObj) || Nwk_ObjIsCi(pObj) || Nwk_ObjIsCo(pObj) );
     if ( Nwk_ObjIsCo(pObj) )
         return Nwk_ObjRequired(pObj);
-    tRequired = AIG_INFINITY;
+    tRequired = TIME_ETERNITY;
     if ( pLutLib == NULL )
     {
         Nwk_ObjForEachFanout( pObj, pFanout, k )
@@ -333,7 +333,7 @@ float Nwk_ManDelayTraceLut( Nwk_Man_t * pNtk )
     {
         printf( "The max LUT size (%d) is less than the max fanin count (%d).\n", 
             pLutLib->LutMax, Nwk_ManGetFaninMax(pNtk) );
-        return -AIG_INFINITY;
+        return -TIME_ETERNITY;
     }
 
     // compute the reverse order of all objects
@@ -356,7 +356,7 @@ float Nwk_ManDelayTraceLut( Nwk_Man_t * pNtk )
     }
 
     // get the latest arrival times
-    tArrival = -AIG_INFINITY;
+    tArrival = -TIME_ETERNITY;
     Nwk_ManForEachPo( pNtk, pObj, i )
         if ( tArrival < Nwk_ObjArrival(pObj) )
             tArrival = Nwk_ObjArrival(pObj);
@@ -388,11 +388,12 @@ float Nwk_ManDelayTraceLut( Nwk_Man_t * pNtk )
         else if ( Nwk_ObjIsCo(pObj) )
         {
             if ( pNtk->pManTime )
+            {
                 tRequired = Tim_ManGetPoRequired( pNtk->pManTime, pObj->PioId );
-            else
-                tRequired = Nwk_ObjRequired(pObj);
-            if ( Nwk_ObjRequired(Nwk_ObjFanin0(pObj)) > tRequired )
-                Nwk_ObjSetRequired( Nwk_ObjFanin0(pObj), tRequired );
+                Nwk_ObjSetRequired( pObj, tRequired );
+            }
+            if ( Nwk_ObjRequired(Nwk_ObjFanin0(pObj)) > Nwk_ObjRequired(pObj) )
+                Nwk_ObjSetRequired( Nwk_ObjFanin0(pObj), Nwk_ObjRequired(pObj) );
         }
 
         // set slack for this object
@@ -424,14 +425,12 @@ int Nwk_ManVerifyTiming(  Nwk_Man_t * pNtk )
     {
         tArrival = Nwk_NodeComputeArrival( pObj, 1 );
         tRequired = Nwk_NodeComputeRequired( pObj, 1 );
-        if ( Nwk_ObjIsCi(pObj) && pNtk->pManTime )
-            tArrival = Tim_ManGetPiArrival( pNtk->pManTime, pObj->PioId );
-        if ( Nwk_ObjIsCo(pObj) && pNtk->pManTime )
-            tArrival = Tim_ManGetPoRequired( pNtk->pManTime, pObj->PioId );
         if ( !Nwk_ManTimeEqual( tArrival, Nwk_ObjArrival(pObj), (float)0.01 ) )
-            printf( "Nwk_ManVerifyTiming(): Arrival time of object %d is incorrect.\n", pObj->Id );
+            printf( "Nwk_ManVerifyTiming(): Object %d has different arrival time (%.2f) from computed (%.2f).\n", 
+                pObj->Id, Nwk_ObjArrival(pObj), tArrival );
         if ( !Nwk_ManTimeEqual( tRequired, Nwk_ObjRequired(pObj), (float)0.01 ) )
-            printf( "Nwk_ManVerifyTiming(): Required time of object %d is incorrect.\n", pObj->Id );
+            printf( "Nwk_ManVerifyTiming(): Object %d has different required time (%.2f) from computed (%.2f).\n", 
+                pObj->Id, Nwk_ObjRequired(pObj), tRequired );
     }
     return 1;
 }
@@ -586,9 +585,9 @@ void Nwk_NodeUpdateArrival( Nwk_Obj_t * pObj )
             {
                 Tim_ManSetPoArrival( pManTime, pTemp->PioId, tArrival );
                 iBox = Tim_ManBoxForCo( pManTime, pNext->PioId );
-                Tim_ManSetCurrentTravIdBoxInputs( pManTime, iBox );
                 if ( iBox >= 0 ) // this is not a true PO
                 {
+                    Tim_ManSetCurrentTravIdBoxInputs( pManTime, iBox );
                     iTerm1 = Tim_ManBoxOutputFirst( pManTime, iBox );
                     nTerms = Tim_ManBoxOutputNum( pManTime, iBox );
                     for ( i = 0; i < nTerms; i++ )
@@ -635,14 +634,6 @@ void Nwk_NodeUpdateRequired( Nwk_Obj_t * pObj )
     float tRequired;
     int i, k, iBox, iTerm1, nTerms;
     assert( Nwk_ObjIsNode(pObj) );
-
-if ( pObj->Id == 1384 )
-{
-    int x = 0;
-//    Nwk_ObjPrint( Nwk_ManObj(pObj->pMan, 1384) );
-//    Nwk_ObjPrint( Nwk_ManObj(pObj->pMan, 422) );
-}
-
     // make sure the node's required time remained the same
     tRequired = Nwk_NodeComputeRequired( pObj, 1 );
     assert( Nwk_ManTimeEqual( tRequired, Nwk_ObjRequired(pObj), (float)0.01 ) );
@@ -667,16 +658,16 @@ if ( pObj->Id == 1384 )
         if ( Nwk_ManTimeEqual( tRequired, Nwk_ObjRequired(pTemp), (float)0.01 ) )
             continue;
         Nwk_ObjSetRequired( pTemp, tRequired );
-        // add the fanouts to the queue
+        // add the fanins to the queue
         if ( Nwk_ObjIsCi(pTemp) )
         {
             if ( pManTime )
             {
                 Tim_ManSetPiRequired( pManTime, pTemp->PioId, tRequired );
                 iBox = Tim_ManBoxForCi( pManTime, pNext->PioId );
-                Tim_ManSetCurrentTravIdBoxOutputs( pManTime, iBox );
                 if ( iBox >= 0 ) // this is not a true PO
                 {
+                    Tim_ManSetCurrentTravIdBoxOutputs( pManTime, iBox );
                     iTerm1 = Tim_ManBoxInputFirst( pManTime, iBox );
                     nTerms = Tim_ManBoxInputNum( pManTime, iBox );
                     for ( i = 0; i < nTerms; i++ )
@@ -780,9 +771,9 @@ void Nwk_ManUpdateLevel( Nwk_Obj_t * pObj )
             if ( pManTime )
             {
                 iBox = Tim_ManBoxForCo( pManTime, pNext->PioId );
-                Tim_ManSetCurrentTravIdBoxInputs( pManTime, iBox );
                 if ( iBox >= 0 ) // this is not a true PO
                 {
+                    Tim_ManSetCurrentTravIdBoxInputs( pManTime, iBox );
                     iTerm1 = Tim_ManBoxOutputFirst( pManTime, iBox );
                     nTerms = Tim_ManBoxOutputNum( pManTime, iBox );
                     for ( i = 0; i < nTerms; i++ )
@@ -850,12 +841,10 @@ int Nwk_ManVerifyLevel( Nwk_Man_t * pNtk )
 ***********************************************************************/
 void Nwk_ManUpdate( Nwk_Obj_t * pObj, Nwk_Obj_t * pObjNew, Vec_Vec_t * vLevels )
 {
-//    float Temp;
     assert( pObj->pMan == pObjNew->pMan );
     assert( pObj != pObjNew );
     assert( Nwk_ObjFanoutNum(pObj) > 0 );
     assert( Nwk_ObjIsNode(pObj) && !Nwk_ObjIsCo(pObjNew) );
-//    Temp = Nwk_NodeComputeRequired( pObj, 1 );
     // transfer fanouts to the old node
     Nwk_ObjTransferFanout( pObj, pObjNew );
     // transfer the timing information
@@ -866,7 +855,7 @@ void Nwk_ManUpdate( Nwk_Obj_t * pObj, Nwk_Obj_t * pObjNew, Vec_Vec_t * vLevels )
     pObjNew->tArrival = pObj->tArrival;
     pObjNew->tRequired = pObj->tRequired;
     // update required times of the old fanins
-    pObj->tRequired = AIG_INFINITY;
+    pObj->tRequired = TIME_ETERNITY;
     Nwk_NodeUpdateRequired( pObj );
     // remove the old node
     Nwk_ManDeleteNode_rec( pObj );

src/aig/tim/tim.c

@@ -31,7 +31,6 @@
 #define AIG_MIN(a,b)       (((a) < (b))? (a) : (b))
 #define AIG_MAX(a,b)       (((a) > (b))? (a) : (b))
 #define AIG_ABS(a)         (((a) >= 0)?  (a) :-(a))
-#define AIG_INFINITY       (100000000)
 
 ////////////////////////////////////////////////////////////////////////
 ///                        DECLARATIONS                              ///
@@ -133,7 +132,7 @@ Tim_Man_t * Tim_ManStart( int nPis, int nPos )
     {
         p->pPis[i].Id = i;
         p->pPis[i].iObj2Box = p->pPis[i].iObj2Num = -1;
-        p->pPis[i].timeReq = AIG_INFINITY;
+        p->pPis[i].timeReq = TIME_ETERNITY;
         p->pPis[i].timeArr = 0.0;
         p->pPis[i].TravId = 0;
     }
@@ -141,7 +140,7 @@ Tim_Man_t * Tim_ManStart( int nPis, int nPos )
     {
         p->pPos[i].Id = i;
         p->pPos[i].iObj2Box = p->pPos[i].iObj2Num = -1;
-        p->pPos[i].timeReq = AIG_INFINITY;
+        p->pPos[i].timeReq = TIME_ETERNITY;
         p->pPos[i].timeArr = 0.0;
         p->pPos[i].TravId = 0;
     }
@@ -673,7 +672,7 @@ float Tim_ManGetPiArrival( Tim_Man_t * p, int iPi )
     Tim_ManBoxForEachOutput( p, pBox, pObjRes, i )
     {
         pDelays = pBox->pDelayTable + i * pBox->nInputs;
-        DelayBest = -AIG_INFINITY;
+        DelayBest = -TIME_ETERNITY;
         Tim_ManBoxForEachInput( p, pBox, pObj, k )
             DelayBest = AIG_MAX( DelayBest, pObj->timeArr + pDelays[k] );
         pObjRes->timeArr = DelayBest;
@@ -718,7 +717,7 @@ float Tim_ManGetPoRequired( Tim_Man_t * p, int iPo )
     // compute the required times for each input of the box (POs)
     Tim_ManBoxForEachInput( p, pBox, pObjRes, i )
     {
-        DelayBest = AIG_INFINITY;
+        DelayBest = TIME_ETERNITY;
         Tim_ManBoxForEachOutput( p, pBox, pObj, k )
         {
             pDelays = pBox->pDelayTable + k * pBox->nInputs;

src/aig/tim/tim.h

@@ -43,6 +43,7 @@ typedef struct Tim_Man_t_           Tim_Man_t;
 ///                      MACRO DEFINITIONS                           ///
 ////////////////////////////////////////////////////////////////////////
 
+#define TIME_ETERNITY 10000
 
 ////////////////////////////////////////////////////////////////////////
 ///                             ITERATORS                            ///

src/base/abci/abc.c

@@ -15094,7 +15094,7 @@ int Abc_CommandAbc8DC2( Abc_Frame_t * pAbc, int argc, char ** argv )
     extern Aig_Man_t * Dar_ManCompress2( Aig_Man_t * pAig, int fBalance, int fUpdateLevel, int fFanout, int fVerbose );
 
     // set defaults
-    fBalance     = 0;
+    fBalance     = 1;
     fUpdateLevel = 1;
     fVerbose     = 0;
     Extra_UtilGetoptReset();
@@ -15768,19 +15768,21 @@ int Abc_CommandAbc8Cec( Abc_Frame_t * pAbc, int argc, char ** argv )
     int c;
     int fVerbose;
     int nConfLimit;
-    int fPartition;
+    int fSmart;
+    int nPartSize;
     extern Aig_Man_t * Ntl_ManCollapse( void * p );
     extern void * Ntl_ManDup( void * pOld );
     extern void Ntl_ManFree( void * p );
 
-    extern int Fra_FraigCecTop( Aig_Man_t * pMan1, Aig_Man_t * pMan2, int nConfLimit, int fPartition, int fVerbose );
+    extern int Fra_FraigCecTop( Aig_Man_t * pMan1, Aig_Man_t * pMan2, int nConfLimit, int nPartSize, int fSmart, int fVerbose );
 
     // set defaults
-    fVerbose =  0;
     nConfLimit = 10000;   
-    fPartition = 0;
+    nPartSize  = 100;
+    fSmart     = 0;
+    fVerbose   =  0;
     Extra_UtilGetoptReset();
-    while ( ( c = Extra_UtilGetopt( argc, argv, "Cpvh" ) ) != EOF )
+    while ( ( c = Extra_UtilGetopt( argc, argv, "CPsvh" ) ) != EOF )
     {
         switch ( c )
         {
@@ -15795,8 +15797,19 @@ int Abc_CommandAbc8Cec( Abc_Frame_t * pAbc, int argc, char ** argv )
             if ( nConfLimit < 0 ) 
                 goto usage;
             break;
-        case 'p':
-            fPartition ^= 1;
+        case 'P':
+            if ( globalUtilOptind >= argc )
+            {
+                fprintf( stdout, "Command line switch \"-P\" should be followed by an integer.\n" );
+                goto usage;
+            }
+            nPartSize = atoi(argv[globalUtilOptind]);
+            globalUtilOptind++;
+            if ( nPartSize < 0 ) 
+                goto usage;
+            break;
+        case 's':
+            fSmart ^= 1;
             break;
         case 'v':
             fVerbose ^= 1;
@@ -15836,16 +15849,17 @@ int Abc_CommandAbc8Cec( Abc_Frame_t * pAbc, int argc, char ** argv )
     Ntl_ManFree( pTemp );
 
     // perform verification
-    Fra_FraigCecTop( pAig1, pAig2, nConfLimit, fPartition, fVerbose );
+    Fra_FraigCecTop( pAig1, pAig2, nConfLimit, nPartSize, fSmart, fVerbose );
     Aig_ManStop( pAig1 );
     Aig_ManStop( pAig2 );
     return 0;
 
 usage:
-    fprintf( stdout, "usage: *cec [-C num] [-pvh] <file1> <file2>\n" );
+    fprintf( stdout, "usage: *cec [-C num] [-P num] [-svh] <file1> <file2>\n" );
     fprintf( stdout, "\t         performs combinational equivalence checking\n" );
     fprintf( stdout, "\t-C num : limit on the number of conflicts [default = %d]\n", nConfLimit );
-    fprintf( stdout, "\t-p     : toggle automatic partitioning [default = %s]\n", fPartition? "yes": "no" );
+    fprintf( stdout, "\t-P num : the partition size for partitioned CEC [default = %d]\n", nPartSize );
+    fprintf( stdout, "\t-s     : toggle smart and natural output partitioning [default = %s]\n", fSmart? "smart": "natural" );
     fprintf( stdout, "\t-v     : toggles verbose output [default = %s]\n", fVerbose? "yes": "no" );
     fprintf( stdout, "\t-h     : print the command usage\n");
     fprintf( stdout, "\tfile1  : (optional) the file with the first network\n");

src/base/abci/abcDar.c

@@ -946,7 +946,7 @@ int Abc_NtkDarCec( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int fPartition, int fVe
     {
         pMan1 = Abc_NtkToDar( pNtk1, 0, 0 );
         pMan2 = Abc_NtkToDar( pNtk2, 0, 0 );
-        RetValue = Fra_FraigCecPartitioned( pMan1, pMan2, 100, fVerbose );
+        RetValue = Fra_FraigCecPartitioned( pMan1, pMan2, 100, 1, fVerbose );
         Aig_ManStop( pMan1 );
         Aig_ManStop( pMan2 );
         goto finish;

src/base/abci/abcVerify.c

@@ -397,6 +397,7 @@ void Abc_NtkCecFraigPartAuto( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int nSeconds
         printf( "Verifying part %4d  (out of %4d)  PI = %5d. PO = %5d. And = %6d. Lev = %4d.\r", 
             i+1, Vec_PtrSize(vParts), Abc_NtkPiNum(pMiterPart), Abc_NtkPoNum(pMiterPart), 
             Abc_NtkNodeNum(pMiterPart), Abc_AigLevel(pMiterPart) );
+        fflush( stdout );
         // solve the problem
         RetValue = Abc_NtkIvyProve( &pMiterPart, pParams );
         if ( RetValue == -1 )

src/base/io/io.c

@@ -1408,7 +1408,7 @@ int IoCommandWriteBench( Abc_Frame_t * pAbc, int argc, char **argv )
     // call the corresponding file writer
     if ( !fUseLuts )
         Io_Write( pAbc->pNtkCur, pFileName, IO_FILE_BENCH );
-    else
+    else if ( pAbc->pNtkCur )
     {
         Abc_Ntk_t * pNtkTemp;
         pNtkTemp = Abc_NtkToNetlist( pAbc->pNtkCur );
@@ -1416,6 +1416,8 @@ int IoCommandWriteBench( Abc_Frame_t * pAbc, int argc, char **argv )
         Io_WriteBenchLut( pNtkTemp, pFileName );
         Abc_NtkDelete( pNtkTemp );
     }
+    else
+        printf( "There is no current network.\n" );
     return 0;
 
 usage:

src/map/if/ifLib.c

@@ -90,7 +90,7 @@ If_Lib_t * If_LutLibRead( char * FileName )
             return NULL;
         }
 
-        // check if var delays are specifies
+        // check if var delays are specified
         if ( k > 1 )
             p->fVarPinDelays = 1;
 

src/map/if/ifMap.c

@@ -88,7 +88,7 @@ void If_ObjPerformMappingAnd( If_Man_t * p, If_Obj_t * pObj, int Mode, int fPrep
     {
         // recompute the parameters of the best cut
         pCut->Delay = If_CutDelay( p, pCut );
-        assert( pCut->Delay <= pObj->Required + p->fEpsilon );
+//        assert( pCut->Delay <= pObj->Required + p->fEpsilon );
         pCut->Area = (Mode == 2)? If_CutAreaDerefed( p, pCut ) : If_CutAreaFlow( p, pCut );
         if ( p->pPars->fEdge )
             pCut->Edge = (Mode == 2)? If_CutEdgeDerefed( p, pCut ) : If_CutEdgeFlow( p, pCut );