Version abc90118

12 files changed, 236 insertions, 52 deletions

diff --git a/src/aig/ntl/ntl.h b/src/aig/ntl/ntl.h
index 54db901f..ac266ca5 100644
--- a/src/aig/ntl/ntl.h
+++ b/src/aig/ntl/ntl.h
@@ -79,6 +79,10 @@ struct Ntl_Man_t_
     Aig_Man_t *        pAig;           // the extracted AIG
     Tim_Man_t *        pManTime;       // the timing manager
     int                iLastCi;        // the last true CI
+    void *             pNal;           // additional data
+    void (*pNalF)(void *);             // additional data
+    void (*pNalD)(void *,void *);      // additional data
+    void (*pNalW)(void *,void *);      // additional data
     // hashing names into models
     Ntl_Mod_t **       pModTable;      // the hash table of names into models
     int                nModTableSize;  // the allocated table size
@@ -93,6 +97,7 @@ struct Ntl_Mod_t_
     Vec_Ptr_t *        vObjs;          // the array of all objects
     Vec_Ptr_t *        vPis;           // the array of PI objects
     Vec_Ptr_t *        vPos;           // the array of PO objects
+    Vec_Ptr_t *        vNets;          // the array of nets
     int                nObjs[NTL_OBJ_VOID]; // counter of objects of each type
     // box attributes
     unsigned int       attrWhite   :1; // box has known logic
@@ -104,6 +109,9 @@ struct Ntl_Mod_t_
     Ntl_Net_t **       pTable;         // the hash table of names into nets
     int                nTableSize;     // the allocated table size
     int                nEntries;       // the number of entries in the hash table
+    // clocks of the model
+    Vec_Ptr_t *        vClocks;        // the clock signals
+    Vec_Vec_t *        vClockFlops;    // the flops of each clock
     // delay information
     Vec_Int_t *        vDelays;
     Vec_Int_t *        vTimeInputs;
@@ -154,6 +162,7 @@ struct Ntl_Net_t_
         int            iTemp;          // other data
     };
     Ntl_Obj_t *        pDriver;        // driver of the net
+    int                NetId;          // unique ID of the net
     char               nVisits;        // the number of times the net is visited
     char               fMark;          // temporary mark
     char               pName[0];       // the name of this net
@@ -175,18 +184,19 @@ struct Ntl_Lut_t_
 ////////////////////////////////////////////////////////////////////////
 ///                      INLINED FUNCTIONS                           ///
 ////////////////////////////////////////////////////////////////////////
+
 #ifdef WIN32
-#define DLLEXPORT __declspec(dllexport)
-#define DLLIMPORT __declspec(dllimport)
+#define ABC_DLLEXPORT __declspec(dllexport)
+#define ABC_DLLIMPORT __declspec(dllimport)
 #else  /* defined(WIN32) */
-#define DLLIMPORT
+#define ABC_DLLIMPORT
 #endif /* defined(WIN32) */
 
 #ifndef ABC_DLL
-#define ABC_DLL DLLIMPORT
+#define ABC_DLL ABC_DLLIMPORT
 #endif
 
-static inline Ntl_Mod_t * Ntl_ManRootModel( Ntl_Man_t * p )       { return (Ntl_Mod_t *)Vec_PtrEntry( p->vModels, 0 );       } 
+static inline Ntl_Mod_t * Ntl_ManRootModel( Ntl_Man_t * p )       { return (Ntl_Mod_t *)Vec_PtrEntry( p->vModels, 0 );   } 
 
 static inline int         Ntl_ModelPiNum( Ntl_Mod_t * p )         { return p->nObjs[NTL_OBJ_PI];                } 
 static inline int         Ntl_ModelPoNum( Ntl_Mod_t * p )         { return p->nObjs[NTL_OBJ_PO];                } 
@@ -195,8 +205,10 @@ static inline int         Ntl_ModelLut1Num( Ntl_Mod_t * p )       { return p->nO
 static inline int         Ntl_ModelLatchNum( Ntl_Mod_t * p )      { return p->nObjs[NTL_OBJ_LATCH];             } 
 static inline int         Ntl_ModelBoxNum( Ntl_Mod_t * p )        { return p->nObjs[NTL_OBJ_BOX];               } 
 
-static inline Ntl_Obj_t * Ntl_ModelPi( Ntl_Mod_t * p, int i )     { return (Ntl_Obj_t *)Vec_PtrEntry(p->vPis, i);            } 
-static inline Ntl_Obj_t * Ntl_ModelPo( Ntl_Mod_t * p, int i )     { return (Ntl_Obj_t *)Vec_PtrEntry(p->vPos, i);            } 
+static inline Ntl_Obj_t * Ntl_ModelPi( Ntl_Mod_t * p, int i )     { return (Ntl_Obj_t *)Vec_PtrEntry(p->vPis, i);        } 
+static inline Ntl_Obj_t * Ntl_ModelPo( Ntl_Mod_t * p, int i )     { return (Ntl_Obj_t *)Vec_PtrEntry(p->vPos, i);        } 
+static inline Ntl_Obj_t * Ntl_ModelObj( Ntl_Mod_t * p, int i )    { return (Ntl_Obj_t *)Vec_PtrEntry(p->vObjs, i);       } 
+static inline Ntl_Net_t * Ntl_ModelNet( Ntl_Mod_t * p, int i )    { return (Ntl_Net_t *)Vec_PtrEntry(p->vNets, i);       } 
 
 static inline char *      Ntl_ModelPiName( Ntl_Mod_t * p, int i ) { return Ntl_ModelPi(p, i)->pFanio[0]->pName; } 
 static inline char *      Ntl_ModelPoName( Ntl_Mod_t * p, int i ) { return Ntl_ModelPo(p, i)->pFanio[0]->pName; } 
@@ -253,8 +265,8 @@ static inline int         Ntl_ObjIsSeqRoot( Ntl_Obj_t * p )       { return Ntl_O
 #define Ntl_ModelForEachPo( pNwk, pObj, i )                                     \
     for ( i = 0; (i < Vec_PtrSize(pNwk->vPos)) && (((pObj) = (Ntl_Obj_t*)Vec_PtrEntry(pNwk->vPos, i)), 1); i++ )
 #define Ntl_ModelForEachNet( pNwk, pNet, i )                                    \
-    for ( i = 0; i < pNwk->nTableSize; i++ )                                    \
-        for ( pNet = pNwk->pTable[i]; pNet; pNet = pNet->pNext ) 
+    Vec_PtrForEachEntry( pNwk->vNets, pNet, i )                                 \
+        if ( pNet == NULL ) {} else
 #define Ntl_ModelForEachObj( pNwk, pObj, i )                                    \
     for ( i = 0; (i < Vec_PtrSize(pNwk->vObjs)) && (((pObj) = (Ntl_Obj_t*)Vec_PtrEntry(pNwk->vObjs, i)), 1); i++ ) \
         if ( pObj == NULL ) {} else
@@ -359,6 +371,7 @@ extern ABC_DLL int             Ntl_ModelFindPioNumber( Ntl_Mod_t * p, int fPiOnl
 extern ABC_DLL int             Ntl_ModelSetNetDriver( Ntl_Obj_t * pObj, Ntl_Net_t * pNet );
 extern ABC_DLL int             Ntl_ModelClearNetDriver( Ntl_Obj_t * pObj, Ntl_Net_t * pNet );
 extern ABC_DLL void            Ntl_ModelDeleteNet( Ntl_Mod_t * p, Ntl_Net_t * pNet );
+extern ABC_DLL void            Ntl_ModelInsertNet( Ntl_Mod_t * p, Ntl_Net_t * pNet );
 extern ABC_DLL int             Ntl_ModelCountNets( Ntl_Mod_t * p );
 extern ABC_DLL int             Ntl_ManAddModel( Ntl_Man_t * p, Ntl_Mod_t * pModel );
 extern ABC_DLL Ntl_Mod_t *     Ntl_ManFindModel( Ntl_Man_t * p, const char * pName );
diff --git a/src/aig/ntl/ntlCheck.c b/src/aig/ntl/ntlCheck.c
index 47f14525..82ef388b 100644
--- a/src/aig/ntl/ntlCheck.c
+++ b/src/aig/ntl/ntlCheck.c
@@ -206,11 +206,13 @@ checkobjs:
             printf( "Net in bin %d does not have a name\n", i );
             fStatus = 0;
         }
+/*
         if ( pNet->pDriver == NULL )
         {
             printf( "Net %s does not have a driver\n", pNet->pName );
             fStatus = 0;
         }
+*/
     }
 
     // check objects
diff --git a/src/aig/ntl/ntlCore.c b/src/aig/ntl/ntlCore.c
index 6bff57d9..b170cdad 100644
--- a/src/aig/ntl/ntlCore.c
+++ b/src/aig/ntl/ntlCore.c
@@ -43,14 +43,14 @@
 Aig_Man_t * Ntl_ManPerformChoicing( Aig_Man_t * pAig, int fBalance, int fUpdateLevel, int fConstruct, int nConfMax, int nLevelMax, int fVerbose )
 {
     extern Aig_Man_t * Dar_ManBalance( Aig_Man_t * pAig, int fUpdateLevel );
-    extern Aig_Man_t * Dar_ManCompress( Aig_Man_t * pAig, int fBalance, int fUpdateLevel, int fVerbose );
+    extern Aig_Man_t * Dar_ManCompress( Aig_Man_t * pAig, int fBalance, int fUpdateLevel, int fPower, int fVerbose );
     extern Aig_Man_t * Dar_ManChoice( Aig_Man_t * pAig, int fBalance, int fUpdateLevel, int fConstruct, int nConfMax, int nLevelMax, int fVerbose );
     Aig_Man_t * pTemp;
     // perform synthesis
 //printf( "Pre-synthesis AIG:  " );
 //Aig_ManPrintStats( pAig );
 //    pTemp = Dar_ManBalance( pAig, 1 );
-//    pTemp = Dar_ManCompress( pAig, 1, 1, 0 );
+//    pTemp = Dar_ManCompress( pAig, 1, 1, 0, 0 );
     pTemp = Dar_ManChoice( pAig, fBalance, fUpdateLevel, fConstruct, nConfMax, nLevelMax, fVerbose );
 //printf( "Post-synthesis AIG: " );
 //Aig_ManPrintStats( pTemp );
diff --git a/src/aig/ntl/ntlExtract.c b/src/aig/ntl/ntlExtract.c
index 56710a25..6923ac7a 100644
--- a/src/aig/ntl/ntlExtract.c
+++ b/src/aig/ntl/ntlExtract.c
@@ -175,7 +175,7 @@ int Ntl_ManExtract_rec( Ntl_Man_t * p, Ntl_Net_t * pNet )
         if ( !Ntl_ManExtract_rec( p, pNetFanin ) )
             return 0;
     // add box inputs/outputs to COs/CIs
-    if ( Ntl_ObjIsBox(pObj) )
+    if ( Ntl_ObjIsBox(pObj) ) 
     {
         int LevelCur, LevelMax = -TIM_ETERNITY;
         assert( Ntl_BoxIsComb(pObj) );
@@ -370,7 +370,7 @@ int Ntl_ManCollapseBoxSeq1_rec( Ntl_Man_t * p, Ntl_Obj_t * pBox, int fSeq )
             pNet->pCopy = Aig_Not(pNet->pCopy);
         pNet->nVisits = 2;
         // remember the class of this register
-        Vec_IntPush( p->vRegClasses, pObj->LatchId.regClass );
+        Vec_IntPush( p->vRegClasses, p->pNal ? pBox->iTemp : pObj->LatchId.regClass );
     }
     // compute AIG for the internal nodes
     Ntl_ModelForEachPo( pModel, pObj, i )
diff --git a/src/aig/ntl/ntlFraig.c b/src/aig/ntl/ntlFraig.c
index 27d863af..d2ae4204 100644
--- a/src/aig/ntl/ntlFraig.c
+++ b/src/aig/ntl/ntlFraig.c
@@ -215,9 +215,9 @@ Aig_Obj_t ** Ntl_ManFraigDeriveClasses( Aig_Man_t * pAig, Ntl_Man_t * pNew, Aig_
 void Ntl_ManReduce( Ntl_Man_t * p, Aig_Man_t * pAig )
 {
     Aig_Obj_t * pObj, * pObjRepr;
-    Ntl_Net_t * pNet, * pNetRepr;
+    Ntl_Net_t * pNet, * pNetRepr, * pNetNew;
     Ntl_Mod_t * pRoot;
-    Ntl_Obj_t * pNode;
+    Ntl_Obj_t * pNode, * pNodeOld;
     int i, fCompl, Counter = 0;
     assert( pAig->pReprs );
     pRoot = Ntl_ManRootModel( p );
@@ -271,10 +271,23 @@ void Ntl_ManReduce( Ntl_Man_t * p, Aig_Man_t * pAig )
         pNode->pSop = fCompl? Ntl_ManStoreSop( p->pMemSops, "0 1\n" ) : Ntl_ManStoreSop( p->pMemSops, "1 1\n" );
         Ntl_ObjSetFanin( pNode, pNetRepr, 0 );
         // make the new node drive the equivalent net (pNet)
+        pNodeOld = pNet->pDriver;
         if ( !Ntl_ModelClearNetDriver( pNet->pDriver, pNet ) )
             printf( "Ntl_ManReduce(): Internal error! Net already has no driver.\n" );
         if ( !Ntl_ModelSetNetDriver( pNode, pNet ) )
             printf( "Ntl_ManReduce(): Internal error! Net already has a driver.\n" );
+
+        // remove this net from the hash table (but do not remove from the array)
+        Ntl_ModelDeleteNet( pRoot, pNet );
+        // create new net with the same name
+        pNetNew = Ntl_ModelFindOrCreateNet( pRoot, pNet->pName );
+        // clean the name
+        pNet->pName[0] = 0;
+
+        // make the old node drive the new net without fanouts
+        if ( !Ntl_ModelSetNetDriver( pNodeOld, pNetNew ) )
+            printf( "Ntl_ManReduce(): Internal error! Net already has a driver.\n" );
+
         Counter++;
     }
 }
@@ -372,6 +385,11 @@ Ntl_Man_t * Ntl_ManFraig( Ntl_Man_t * p, int nPartSize, int nConfLimit, int nLev
     pAig = Ntl_ManExtract( p );
     pNew = Ntl_ManInsertAig( p, pAig );
     pAigCol = Ntl_ManCollapseComb( pNew );
+    if ( pAigCol == NULL )
+    {
+        Aig_ManStop( pAig );
+        return pNew;
+    }
 
     // perform fraiging for the given design
     nPartSize = nPartSize? nPartSize : Aig_ManPoNum(pAigCol);
@@ -406,13 +424,15 @@ Ntl_Man_t * Ntl_ManScl( Ntl_Man_t * p, int fLatchConst, int fLatchEqual, int fVe
     pAig = Ntl_ManExtract( p );
     pNew = Ntl_ManInsertAig( p, pAig );
     pAigCol = Ntl_ManCollapseSeq( pNew, 0 );
-//Saig_ManDumpBlif( pAigCol, "1s.blif" );
+    if ( pAigCol == NULL )
+    {
+        Aig_ManStop( pAig );
+        return pNew;
+    }
 
     // perform SCL for the given design
     pTemp = Aig_ManScl( pAigCol, fLatchConst, fLatchEqual, fVerbose );
     Aig_ManStop( pTemp );
-    if ( pNew->vRegClasses && Vec_IntSize(pNew->vRegClasses) && pAigCol->pReprs )
-        Ntl_ManFilterRegisterClasses( pAigCol, pNew->vRegClasses, fVerbose );
 
     // finalize the transformation
     pNew = Ntl_ManFinalize( pAux = pNew, pAig, pAigCol, fVerbose );
@@ -435,25 +455,26 @@ Ntl_Man_t * Ntl_ManScl( Ntl_Man_t * p, int fLatchConst, int fLatchEqual, int fVe
 ***********************************************************************/
 Ntl_Man_t * Ntl_ManLcorr( Ntl_Man_t * p, int nConfMax, int fVerbose )
 {
-    Ssw_Pars_t Pars, * pPars = &Pars;
     Ntl_Man_t * pNew, * pAux;
     Aig_Man_t * pAig, * pAigCol, * pTemp;
+    Ssw_Pars_t Pars, * pPars = &Pars;
+    Ssw_ManSetDefaultParamsLcorr( pPars );
+    pPars->nBTLimit = nConfMax;
+    pPars->fVerbose = fVerbose;
 
     // collapse the AIG
     pAig = Ntl_ManExtract( p );
     pNew = Ntl_ManInsertAig( p, pAig );
-    pAigCol = Ntl_ManCollapseSeq( pNew, 0 );
+    pAigCol = Ntl_ManCollapseSeq( pNew, pPars->nMinDomSize );
+    if ( pAigCol == NULL )
+    {
+        Aig_ManStop( pAig );
+        return pNew;
+    }
 
-    // perform SCL for the given design
-//    pTemp = Fra_FraigLatchCorrespondence( pAigCol, 0, nConfMax, 0, fVerbose, NULL, 0 );
-    Ssw_ManSetDefaultParamsLcorr( pPars );
-    pPars->nBTLimit = nConfMax;
-    pPars->fVerbose = fVerbose;
+    // perform LCORR for the given design
     pTemp = Ssw_LatchCorrespondence( pAigCol, pPars );
-
     Aig_ManStop( pTemp );
-    if ( p->vRegClasses && Vec_IntSize(p->vRegClasses) && pAigCol->pReprs )
-        Ntl_ManFilterRegisterClasses( pAigCol, p->vRegClasses, fVerbose );
 
     // finalize the transformation
     pNew = Ntl_ManFinalize( pAux = pNew, pAig, pAigCol, fVerbose );
diff --git a/src/aig/ntl/ntlInsert.c b/src/aig/ntl/ntlInsert.c
index 52f76151..21f2d246 100644
--- a/src/aig/ntl/ntlInsert.c
+++ b/src/aig/ntl/ntlInsert.c
@@ -42,7 +42,7 @@
 ***********************************************************************/
 Ntl_Man_t * Ntl_ManInsertMapping( Ntl_Man_t * p, Vec_Ptr_t * vMapping, Aig_Man_t * pAig )
 {
-    char Buffer[100];
+    char Buffer[1000];
     Vec_Ptr_t * vCopies;
     Vec_Int_t * vCover;
     Ntl_Mod_t * pRoot;
@@ -141,7 +141,7 @@ Ntl_Man_t * Ntl_ManInsertMapping( Ntl_Man_t * p, Vec_Ptr_t * vMapping, Aig_Man_t
 ***********************************************************************/
 Ntl_Man_t * Ntl_ManInsertAig( Ntl_Man_t * p, Aig_Man_t * pAig )
 {
-    char Buffer[100];
+    char Buffer[1000];
     Ntl_Mod_t * pRoot;
     Ntl_Obj_t * pNode;
     Ntl_Net_t * pNet, * pNetCo;
@@ -243,7 +243,6 @@ Ntl_Man_t * Ntl_ManInsertAig( Ntl_Man_t * p, Aig_Man_t * pAig )
     return p;
 }
 
-
 /**Function*************************************************************
 
   Synopsis    [Inserts the given mapping into the netlist.]
@@ -257,7 +256,7 @@ Ntl_Man_t * Ntl_ManInsertAig( Ntl_Man_t * p, Aig_Man_t * pAig )
 ***********************************************************************/
 Ntl_Man_t * Ntl_ManInsertNtk( Ntl_Man_t * p, Nwk_Man_t * pNtk )
 {
-    char Buffer[100]; 
+    char Buffer[1000]; 
     Vec_Ptr_t * vObjs;
     Vec_Int_t * vTruth;
     Vec_Int_t * vCover;
@@ -276,8 +275,8 @@ Ntl_Man_t * Ntl_ManInsertNtk( Ntl_Man_t * p, Nwk_Man_t * pNtk )
     Ntl_ManForEachCiNet( p, pNet, i )
         Nwk_ManCi( pNtk, i )->pCopy = pNet;
     // create a new node for each LUT
-    vTruth = Vec_IntAlloc( 1 << 16 );
-    vCover = Vec_IntAlloc( 1 << 16 );
+    vTruth  = Vec_IntAlloc( 1 << 16 );
+    vCover  = Vec_IntAlloc( 1 << 16 );
     nDigits = Aig_Base10Log( Nwk_ManNodeNum(pNtk) );
     // go through the nodes in the topological order
     vObjs = Nwk_ManDfs( pNtk );
@@ -289,7 +288,6 @@ Ntl_Man_t * Ntl_ManInsertNtk( Ntl_Man_t * p, Nwk_Man_t * pNtk )
         pTruth = Hop_ManConvertAigToTruth( pNtk->pManHop, Hop_Regular(pObj->pFunc), Nwk_ObjFaninNum(pObj), vTruth, 0 );
         if ( Hop_IsComplement(pObj->pFunc) )
             Kit_TruthNot( pTruth, pTruth, Nwk_ObjFaninNum(pObj) );
-        pNode->pSop = Kit_PlaFromTruth( p->pMemSops, pTruth, Nwk_ObjFaninNum(pObj), vCover );
         if ( !Kit_TruthIsConst0(pTruth, Nwk_ObjFaninNum(pObj)) && !Kit_TruthIsConst1(pTruth, Nwk_ObjFaninNum(pObj)) )
         {
             Nwk_ObjForEachFanin( pObj, pFanin, k )
@@ -303,8 +301,17 @@ Ntl_Man_t * Ntl_ManInsertNtk( Ntl_Man_t * p, Nwk_Man_t * pNtk )
                 Ntl_ObjSetFanin( pNode, pNet, k );
             }
         }
-        else
+        else if ( Kit_TruthIsConst0(pTruth, Nwk_ObjFaninNum(pObj)) )
+        {
+            pObj->pFunc = Hop_ManConst0(pNtk->pManHop);
             pNode->nFanins = 0;
+        }
+        else if ( Kit_TruthIsConst1(pTruth, Nwk_ObjFaninNum(pObj)) )
+        {
+            pObj->pFunc = Hop_ManConst1(pNtk->pManHop);
+            pNode->nFanins = 0;
+        }
+        pNode->pSop = Kit_PlaFromTruth( p->pMemSops, pTruth, Nwk_ObjFaninNum(pObj), vCover );
         sprintf( Buffer, "lut%0*d", nDigits, i );
         if ( (pNet = Ntl_ModelFindNet( pRoot, Buffer )) )
         {
@@ -334,11 +341,29 @@ Ntl_Man_t * Ntl_ManInsertNtk( Ntl_Man_t * p, Nwk_Man_t * pNtk )
         // get the corresponding PO and its driver
         pObj = Nwk_ManCo( pNtk, i );
         pFanin = Nwk_ObjFanin0( pObj );
-        // get the net driving the driver
-        pNet = pFanin->pCopy;
-        pNode = Ntl_ModelCreateNode( pRoot, 1 );
-        pNode->pSop = pObj->fInvert? Ntl_ManStoreSop( p->pMemSops, "0 1\n" ) : Ntl_ManStoreSop( p->pMemSops, "1 1\n" );
-        Ntl_ObjSetFanin( pNode, pNet, 0 );
+        // get the net driving this PO
+        pNet = pFanin->pCopy; 
+        if ( Nwk_ObjFanoutNum(pFanin) == 1 && Ntl_ObjIsNode(pNet->pDriver) )
+        {
+            pNode = pNet->pDriver;
+            if ( !Ntl_ModelClearNetDriver( pNode, pNet ) )
+            {
+                printf( "Ntl_ManInsertNtk(): Internal error! Net already has no driver.\n" );
+                return NULL;
+            }
+            // remove this net 
+            Ntl_ModelDeleteNet( pRoot, pNet );
+            Vec_PtrWriteEntry( pRoot->vNets, pNet->NetId, NULL );
+            // update node's function
+            if ( pObj->fInvert )
+                Kit_PlaComplement( pNode->pSop );
+        }
+        else
+        {
+            pNode = Ntl_ModelCreateNode( pRoot, 1 );
+            pNode->pSop = pObj->fInvert? Ntl_ManStoreSop( p->pMemSops, "0 1\n" ) : Ntl_ManStoreSop( p->pMemSops, "1 1\n" );
+            Ntl_ObjSetFanin( pNode, pNet, 0 );
+        }
         // update the CO driver net
         assert( pNetCo->pDriver == NULL );
         if ( !Ntl_ModelSetNetDriver( pNode, pNetCo ) )
diff --git a/src/aig/ntl/ntlMan.c b/src/aig/ntl/ntlMan.c
index dd481537..8b26e405 100644
--- a/src/aig/ntl/ntlMan.c
+++ b/src/aig/ntl/ntlMan.c
@@ -108,6 +108,7 @@ Ntl_Man_t * Ntl_ManStartFrom( Ntl_Man_t * pOld )
     pNew->pName = Ntl_ManStoreFileName( pNew, pOld->pName );
     pNew->pSpec = Ntl_ManStoreName( pNew, pOld->pName );
     Vec_PtrForEachEntry( pOld->vModels, pModel, i )
+    {
         if ( i == 0 )
         {
             Ntl_ManMarkCiCoNets( pOld );
@@ -116,15 +117,21 @@ Ntl_Man_t * Ntl_ManStartFrom( Ntl_Man_t * pOld )
         }
         else
             pModel->pCopy = Ntl_ModelDup( pNew, pModel );
+    }
     Vec_PtrForEachEntry( pOld->vModels, pModel, i )
         Ntl_ModelForEachBox( pModel, pBox, k )
+        {
             ((Ntl_Obj_t *)pBox->pCopy)->pImplem = pBox->pImplem->pCopy;
+            ((Ntl_Obj_t *)pBox->pCopy)->iTemp = pBox->iTemp;
+        }
     Ntl_ManForEachCiNet( pOld, pNet, i )
         Vec_PtrPush( pNew->vCis, pNet->pCopy );
     Ntl_ManForEachCoNet( pOld, pNet, i )
         Vec_PtrPush( pNew->vCos, pNet->pCopy );
     if ( pOld->pManTime )
         pNew->pManTime = Tim_ManDup( pOld->pManTime, 0 );
+    if ( pOld->pNal )
+        pOld->pNalD( pOld, pNew );
     return pNew;
 }
 
@@ -195,13 +202,14 @@ void Ntl_ManFree( Ntl_Man_t * p )
     if ( p->pMemSops )   Aig_MmFlexStop( p->pMemSops, 0 );
     if ( p->pAig )       Aig_ManStop( p->pAig );
     if ( p->pManTime )   Tim_ManStop( p->pManTime );
+    if ( p->pNal )       p->pNalF( p->pNal );
     FREE( p->pModTable );
     free( p );
 }
 
 /**Function*************************************************************
 
-  Synopsis    [Deallocates the netlist manager.]
+  Synopsis    []
 
   Description []
                
@@ -219,6 +227,7 @@ void Ntl_ManPrintStats( Ntl_Man_t * p )
     printf( "po = %5d  ",      Ntl_ModelPoNum(pRoot) );
     printf( "lat = %5d  ",     Ntl_ModelLatchNum(pRoot) );
     printf( "node = %5d  ",    Ntl_ModelNodeNum(pRoot) );
+    printf( "\n    " );
     printf( "inv/buf = %5d  ", Ntl_ModelLut1Num(pRoot) );
     printf( "box = %4d  ",     Ntl_ModelBoxNum(pRoot) );
     printf( "mod = %3d  ",     Vec_PtrSize(p->vModels) );
@@ -230,6 +239,50 @@ void Ntl_ManPrintStats( Ntl_Man_t * p )
     fflush( stdout );
 }
 
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Nwk_ManPrintStatsShort( Ntl_Man_t * p, Aig_Man_t * pAig, Nwk_Man_t * pNtk )
+{
+    Ntl_Mod_t * pRoot;
+    Ntl_Obj_t * pObj;
+    int i, Counter = 0;
+    pRoot = Ntl_ManRootModel( p );
+    Ntl_ModelForEachBox( pRoot, pObj, i )
+        if ( strcmp(pObj->pImplem->pName, "dff") == 0 )
+            Counter++;
+    printf( "%-15s : ",  p->pName );
+    printf( "pi =%5d  ", Ntl_ModelPiNum(pRoot) );
+    printf( "po =%5d  ", Ntl_ModelPoNum(pRoot) );
+    printf( "ff =%5d  ", Counter );
+    if ( pAig != NULL )
+    {
+        Counter = Aig_ManCountChoices( pAig );
+        if ( Counter )
+            printf( "cho =%7d  ", Counter );
+        else
+            printf( "aig =%7d  ", Aig_ManNodeNum(pAig) );
+    }
+    if ( pNtk == NULL )
+        printf( "Mapping is not available.\n" );
+    else
+    {
+        printf( "lut =%5d  ",  Nwk_ManNodeNum(pNtk) );
+        printf( "lev =%3d  ",  Nwk_ManLevel(pNtk) );
+//        printf( "del =%5.2f ", Nwk_ManDelayTraceLut(pNtk) );
+        printf( "\n" );
+    }
+}
+
 /**Function*************************************************************
 
   Synopsis    [Deallocates the netlist manager.]
@@ -283,6 +336,8 @@ void Ntl_ManSaveBoxType( Ntl_Obj_t * pObj )
 ***********************************************************************/
 void Ntl_ManPrintTypes( Ntl_Man_t * p )
 {
+    Vec_Ptr_t * vFlops;
+    Ntl_Net_t * pNet;
     Ntl_Mod_t * pModel;
     Ntl_Obj_t * pObj;
     int i;
@@ -296,7 +351,7 @@ void Ntl_ManPrintTypes( Ntl_Man_t * p )
     {
         if ( !p->BoxTypes[i] )
             continue;
-        printf( "%5d :", p->BoxTypes[i] );
+        printf( "Type %2d  Num = %7d :", i, p->BoxTypes[i] );
         printf( " %s", ((i &  1) > 0)? "white   ": "black   " );
         printf( " %s", ((i &  2) > 0)? "box     ": "logic   " );
         printf( " %s", ((i &  4) > 0)? "comb    ": "seq     " );
@@ -304,9 +359,22 @@ void Ntl_ManPrintTypes( Ntl_Man_t * p )
         printf( " %s", ((i & 16) > 0)? "no_merge": "merge   " );
         printf( "\n" );
     }
-    printf( "Total box instances = %6d.\n\n", Ntl_ModelBoxNum(pModel) );
+    printf( "MODEL STATISTICS:\n" );
+    Ntl_ManForEachModel( p, pModel, i )
+        if ( i ) printf( "Model %2d :  Name = %10s  Used = %6d.\n", i, pModel->pName, pModel->nUsed );
     for ( i = 0; i < 32; i++ )
         p->BoxTypes[i] = 0;
+    pModel = Ntl_ManRootModel( p );
+    if ( pModel->vClockFlops )
+    {
+        printf( "CLOCK STATISTICS:\n" );
+        Vec_VecForEachLevel( pModel->vClockFlops, vFlops, i )
+        {
+            pNet = Vec_PtrEntry( pModel->vClocks, i );
+            printf( "Clock %2d :  Name = %30s   Flops = %6d.\n", i+1, pNet->pName, Vec_PtrSize(vFlops) );
+        }
+    }
+    printf( "\n" );
 }
 
 /**Function*************************************************************
@@ -336,6 +404,7 @@ Ntl_Mod_t * Ntl_ModelAlloc( Ntl_Man_t * pMan, char * pName )
     p->vObjs = Vec_PtrAlloc( 100 );
     p->vPis  = Vec_PtrAlloc( 10 );
     p->vPos  = Vec_PtrAlloc( 10 ); 
+    p->vNets = Vec_PtrAlloc( 100 ); 
     // start the table
     p->nTableSize = Aig_PrimeCudd( 100 );
     p->pTable = ALLOC( Ntl_Net_t *, p->nTableSize );
@@ -382,7 +451,9 @@ Ntl_Mod_t * Ntl_ModelStartFrom( Ntl_Man_t * pManNew, Ntl_Mod_t * pModelOld )
     }
     Ntl_ModelForEachNet( pModelOld, pNet, i )
     {
-        if ( pNet->fMark )
+        if ( pNet->pDriver == NULL )
+            pNet->pCopy = Ntl_ModelFindOrCreateNet( pModelNew, pNet->pName );
+        else if ( pNet->fMark )
         {
             pNet->pCopy = Ntl_ModelFindOrCreateNet( pModelNew, pNet->pName );
             ((Ntl_Net_t *)pNet->pCopy)->pDriver = pNet->pDriver->pCopy;
@@ -485,6 +556,9 @@ void Ntl_ModelFree( Ntl_Mod_t * p )
     if ( p->vTimeOutputs )  Vec_IntFree( p->vTimeOutputs );
     if ( p->vTimeInputs )   Vec_IntFree( p->vTimeInputs );
     if ( p->vDelays )       Vec_IntFree( p->vDelays );
+    if ( p->vClocks )       Vec_PtrFree( p->vClocks );
+    if ( p->vClockFlops )   Vec_VecFree( p->vClockFlops );
+    Vec_PtrFree( p->vNets );
     Vec_PtrFree( p->vObjs );
     Vec_PtrFree( p->vPis );
     Vec_PtrFree( p->vPos );
diff --git a/src/aig/ntl/ntlReadBlif.c b/src/aig/ntl/ntlReadBlif.c
index d1a1b99d..3021d556 100644
--- a/src/aig/ntl/ntlReadBlif.c
+++ b/src/aig/ntl/ntlReadBlif.c
@@ -1322,6 +1322,7 @@ static char * Ioa_ReadParseTableBlif( Ioa_ReadMod_t * p, char * pTable, int nFan
     char * pProduct, * pOutput;
     int i, Polarity = -1;
 
+
     p->pMan->nTablesRead++;
     // get the tokens
     Ioa_ReadSplitIntoTokens( vTokens, pTable, '.' );
@@ -1330,6 +1331,8 @@ static char * Ioa_ReadParseTableBlif( Ioa_ReadMod_t * p, char * pTable, int nFan
     if ( Vec_PtrSize(vTokens) == 1 )
     {
         pOutput = Vec_PtrEntry( vTokens, 0 );
+        if ( *pOutput == '\"' )
+            return Ntl_ManStoreSop( p->pMan->pDesign->pMemSops, pOutput );
         if ( ((pOutput[0] - '0') & 0x8E) || pOutput[1] )
         {
             sprintf( p->pMan->sError, "Line %d: Constant table has wrong output value \"%s\".", Ioa_ReadGetLine(p->pMan, pOutput), pOutput );
diff --git a/src/aig/ntl/ntlSweep.c b/src/aig/ntl/ntlSweep.c
index fc95415d..b2c700fb 100644
--- a/src/aig/ntl/ntlSweep.c
+++ b/src/aig/ntl/ntlSweep.c
@@ -139,8 +139,11 @@ int Ntl_ManSweep( Ntl_Man_t * p, int fVerbose )
         }
         // remove the fanout nets
         Ntl_ObjForEachFanout( pObj, pNet, k )
-            if ( pNet != NULL )
+            if ( pNet != NULL && pNet->pName[0] != 0 )
+            {
                 Ntl_ModelDeleteNet( pRoot, pNet );
+                Vec_PtrWriteEntry( pRoot->vNets, pNet->NetId, NULL );
+            }
         // remove the object
         if ( Ntl_ObjIsNode(pObj) && Ntl_ObjFaninNum(pObj) == 1 )
             pRoot->nObjs[NTL_OBJ_LUT1]--;
@@ -150,7 +153,7 @@ int Ntl_ManSweep( Ntl_Man_t * p, int fVerbose )
         pObj->Type = NTL_OBJ_NONE;
         Counter++;
     }
-
+ 
 
 
     // print detailed statistics of sweeping
@@ -191,7 +194,7 @@ int Ntl_ManSweep( Ntl_Man_t * p, int fVerbose )
                     }
                 }
             }
-            printf("\nLUTboxType =%d\n", numLutBox);
+//            printf("\nLUTboxType =%d\n", numLutBox);
         }
     }
     if ( !Ntl_ManCheck( p ) )
diff --git a/src/aig/ntl/ntlTable.c b/src/aig/ntl/ntlTable.c
index aa122900..62f65d6c 100644
--- a/src/aig/ntl/ntlTable.c
+++ b/src/aig/ntl/ntlTable.c
@@ -58,6 +58,8 @@ Ntl_Net_t * Ntl_ModelCreateNet( Ntl_Mod_t * p, const char * pName )
     pNet = (Ntl_Net_t *)Aig_MmFlexEntryFetch( p->pMan->pMemObjs, sizeof(Ntl_Net_t) + strlen(pName) + 1 );
     memset( pNet, 0, sizeof(Ntl_Net_t) );
     strcpy( pNet->pName, pName );
+    pNet->NetId = Vec_PtrSize( p->vNets );
+    Vec_PtrPush( p->vNets, pNet );
     return pNet;
 }
 
@@ -104,7 +106,7 @@ clk = clock();
 
 /**Function*************************************************************
 
-  Synopsis    [Finds or creates the net.]
+  Synopsis    [Finds net.]
 
   Description []
                
@@ -125,7 +127,7 @@ Ntl_Net_t * Ntl_ModelFindNet( Ntl_Mod_t * p, const char * pName )
 
 /**Function*************************************************************
 
-  Synopsis    [Finds or creates the net.]
+  Synopsis    [Deletes net from the hash table.]
 
   Description []
                
@@ -150,6 +152,26 @@ void Ntl_ModelDeleteNet( Ntl_Mod_t * p, Ntl_Net_t * pNet )
         p->pTable[Key] = pEnt->pNext;
     else
         pPrev->pNext = pEnt->pNext;
+    p->nEntries--;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Inserts net into the hash table.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Ntl_ModelInsertNet( Ntl_Mod_t * p, Ntl_Net_t * pNet )
+{
+    unsigned Key = Ntl_HashString( pNet->pName, p->nTableSize );
+    assert( Ntl_ModelFindNet( p, pNet->pName ) == NULL );
+    pNet->pNext = p->pTable[Key];
+    p->pTable[Key] = pNet;
 }
 
 /**Function*************************************************************
@@ -178,6 +200,17 @@ Ntl_Net_t * Ntl_ModelFindOrCreateNet( Ntl_Mod_t * p, const char * pName )
     return pEnt;
 }
 
+/**Function*************************************************************
+
+  Synopsis    [Creates new net.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
 Ntl_Net_t * Ntl_ModelDontFindCreateNet( Ntl_Mod_t * p, const char * pName )
 {
     Ntl_Net_t * pEnt;
diff --git a/src/aig/ntl/ntlUtil.c b/src/aig/ntl/ntlUtil.c
index 51f3b818..6e797590 100644
--- a/src/aig/ntl/ntlUtil.c
+++ b/src/aig/ntl/ntlUtil.c
@@ -424,7 +424,7 @@ Vec_Vec_t * Ntl_ManTransformRegClasses( Ntl_Man_t * pMan, int nSizeMax, int fVer
     vParts = Vec_PtrAlloc( 100 );
     for ( i = 0; i <= ClassMax; i++ )
     {
-        if ( pClassNums[i] < nSizeMax )
+        if ( pClassNums[i] == 0 || pClassNums[i] < nSizeMax )
             continue;
         vPart = Vec_IntAlloc( pClassNums[i] );
         Vec_IntForEachEntry( pMan->vRegClasses, Class, k )
diff --git a/src/aig/ntl/ntlWriteBlif.c b/src/aig/ntl/ntlWriteBlif.c
index 6b7f0996..3df49270 100644
--- a/src/aig/ntl/ntlWriteBlif.c
+++ b/src/aig/ntl/ntlWriteBlif.c
@@ -140,6 +140,8 @@ void Ioa_WriteBlifModel( FILE * pFile, Ntl_Mod_t * pModel, int fMain )
                 fprintf( pFile, " %s", pNet->pName );
             fprintf( pFile, " %s\n", Ntl_ObjFanout0(pObj)->pName );
             fprintf( pFile, "%s", pObj->pSop );
+            if ( *pObj->pSop == '\"' )
+                fprintf( pFile, "\n" );
         }
         else if ( Ntl_ObjIsLatch(pObj) )
         {
@@ -390,6 +392,8 @@ void Ioa_WriteBlifModelGz( gzFile pFile, Ntl_Mod_t * pModel, int fMain )
                 gzprintf( pFile, " %s", pNet->pName );
             gzprintf( pFile, " %s\n", Ntl_ObjFanout0(pObj)->pName );
             gzprintf( pFile, "%s", pObj->pSop );
+            if ( *pObj->pSop == '\"' )
+                gzprintf( pFile, "\n" );
         }
         else if ( Ntl_ObjIsLatch(pObj) )
         {
@@ -567,6 +571,8 @@ void Ioa_WriteBlifModelBz2( bz2file * b, Ntl_Mod_t * pModel, int fMain )
                 fprintfBz2( b, " %s", pNet->pName );
             fprintfBz2( b, " %s\n", Ntl_ObjFanout0(pObj)->pName );
             fprintfBz2( b, "%s", pObj->pSop );
+            if ( *pObj->pSop == '\"' )
+                fprintfBz2( b, "\n" );
         }
         else if ( Ntl_ObjIsLatch(pObj) )
         {
@@ -625,7 +631,11 @@ void Ioa_WriteBlif( Ntl_Man_t * p, char * pFileName )
     Ntl_Mod_t * pModel;
     int i, bzError;
     bz2file b;
-
+    if ( p->pNal )
+    {
+        p->pNalW( p, pFileName );
+        return;
+    }
     // write the GZ file
     if (!strncmp(pFileName+strlen(pFileName)-3,".gz",3)) 
     {