Version abc80610

13 files changed, 1045 insertions, 599 deletions

diff --git a/src/aig/ntl/ntl.h b/src/aig/ntl/ntl.h
index 4179754c..b496cb13 100644
--- a/src/aig/ntl/ntl.h
+++ b/src/aig/ntl/ntl.h
@@ -43,6 +43,7 @@ extern "C" {
 
 typedef struct Ntl_Man_t_    Ntl_Man_t;
 typedef struct Ntl_Mod_t_    Ntl_Mod_t;
+typedef struct Ntl_Reg_t_    Ntl_Reg_t;
 typedef struct Ntl_Obj_t_    Ntl_Obj_t;
 typedef struct Ntl_Net_t_    Ntl_Net_t;
 typedef struct Ntl_Lut_t_    Ntl_Lut_t;
@@ -65,6 +66,7 @@ struct Ntl_Man_t_
     char *             pName;          // the name of this design
     char *             pSpec;          // the name of input file
     Vec_Ptr_t *        vModels;        // the array of all models used to represent boxes
+    int                BoxTypes[15];   // the array of box types among the models
     // memory managers
     Aig_MmFlex_t *     pMemObjs;       // memory for objects
     Aig_MmFlex_t *     pMemSops;       // memory for SOPs
@@ -75,6 +77,12 @@ struct Ntl_Man_t_
     Vec_Int_t *        vBox1Cos;       // the first COs of the boxes
     Aig_Man_t *        pAig;           // the extracted AIG
     Tim_Man_t *        pManTime;       // the timing manager
+    int                iLastCi;        // the last true CI
+    Vec_Ptr_t *        vLatchIns;      // the AIG nodes driving latch inputs for internal latches
+    // hashing names into models
+    Ntl_Mod_t **       pModTable;      // the hash table of names into models
+    int                nModTableSize;  // the allocated table size
+    int                nModEntries;    // the number of entries in the hash table
 };
 
 struct Ntl_Mod_t_
@@ -86,21 +94,33 @@ struct Ntl_Mod_t_
     Vec_Ptr_t *        vPis;           // the array of PI objects
     Vec_Ptr_t *        vPos;           // the array of PO objects
     int                nObjs[NTL_OBJ_VOID]; // counter of objects of each type
-    int                fKeep;          // indicates persistant model
+    // box attributes
+    unsigned int       attrWhite :  1; // box has known logic
+    unsigned int       attrBox   :  1; // box is to remain unmapped
+    unsigned int       attrComb  :  1; // box is combinational
+    unsigned int       attrKeep  :  1; // box cannot be removed by structural sweep
     // hashing names into nets
     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
     // delay information
     Vec_Int_t *        vDelays;
-    Vec_Int_t *        vArrivals;
-    Vec_Int_t *        vRequireds;
+    Vec_Int_t *        vTimeInputs;
+    Vec_Int_t *        vTimeOutputs;
     float *            pDelayTable;   
     // other data members
+    Ntl_Mod_t *        pNext;
     void *             pCopy;
     int                nUsed, nRems;
 }; 
 
+struct Ntl_Reg_t_
+{
+    unsigned int       regInit   :  2; // register initial value
+    unsigned int       regType   :  3; // register type
+    unsigned int       regClass  : 28; // register class
+};
+
 struct Ntl_Obj_t_
 {
     Ntl_Mod_t *        pModel;         // the model  
@@ -113,7 +133,11 @@ struct Ntl_Obj_t_
     union {                            // functionality
         Ntl_Mod_t *    pImplem;        // model (for boxes)
         char *         pSop;           // SOP (for logic nodes)
-        unsigned       LatchId;        // init state + register class (for latches) 
+        Ntl_Reg_t      LatchId;        // init state + register class (for latches) 
+    };
+    union {                            // clock / other data
+        Ntl_Net_t *    pClock;         // clock (for registers)
+        void *         pTemp;          // other data 
     };
     Ntl_Net_t *        pFanio[0];      // fanins/fanouts
 };
@@ -164,8 +188,6 @@ static inline int         Ntl_ModelNodeNum( Ntl_Mod_t * p )       { return p->nO
 static inline int         Ntl_ModelLut1Num( Ntl_Mod_t * p )       { return p->nObjs[NTL_OBJ_LUT1];              } 
 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 int         Ntl_ModelCiNum( Ntl_Mod_t * p )         { return p->nObjs[NTL_OBJ_PI] + p->nObjs[NTL_OBJ_LATCH]; } 
-static inline int         Ntl_ModelCoNum( Ntl_Mod_t * p )         { return p->nObjs[NTL_OBJ_PO] + p->nObjs[NTL_OBJ_LATCH]; } 
 
 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);            } 
@@ -173,8 +195,6 @@ static inline Ntl_Obj_t * Ntl_ModelPo( Ntl_Mod_t * p, int i )     { return (Ntl_
 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; } 
 
-static inline int         Ntl_ModelIsBlackBox( Ntl_Mod_t * p )    { return Ntl_ModelPiNum(p) + Ntl_ModelPoNum(p) == Vec_PtrSize(p->vObjs); } 
-
 static inline int         Ntl_ObjFaninNum( Ntl_Obj_t * p )        { return p->nFanins;                          } 
 static inline int         Ntl_ObjFanoutNum( Ntl_Obj_t * p )       { return p->nFanouts;                         } 
 
@@ -193,6 +213,23 @@ static inline Ntl_Net_t * Ntl_ObjFanout( Ntl_Obj_t * p, int i )   { return p->pF
 static inline void        Ntl_ObjSetFanin( Ntl_Obj_t * p, Ntl_Net_t * pNet, int i )    { p->pFanio[i] = pNet;   } 
 static inline void        Ntl_ObjSetFanout( Ntl_Obj_t * p, Ntl_Net_t * pNet, int i )   { p->pFanio[p->nFanins+i] = pNet; pNet->pDriver = p; } 
 
+static inline int         Ntl_ObjIsInit1( Ntl_Obj_t * p )         { assert( Ntl_ObjIsLatch(p) ); return p->LatchId.regInit == 1;   } 
+static inline void        Ntl_ObjSetInit0( Ntl_Obj_t * p )        { assert( Ntl_ObjIsLatch(p) ); p->LatchId.regInit = 0;           } 
+
+static inline int         Ntl_BoxIsWhite( Ntl_Obj_t * p )         { assert( Ntl_ObjIsBox(p) ); return p->pImplem->attrWhite;    } 
+static inline int         Ntl_BoxIsBlack( Ntl_Obj_t * p )         { assert( Ntl_ObjIsBox(p) ); return !p->pImplem->attrWhite;   } 
+static inline int         Ntl_BoxIsComb( Ntl_Obj_t * p )          { assert( Ntl_ObjIsBox(p) ); return p->pImplem->attrComb;     } 
+static inline int         Ntl_BoxIsSeq( Ntl_Obj_t * p )           { assert( Ntl_ObjIsBox(p) ); return !p->pImplem->attrComb;    } 
+
+static inline int         Ntl_ObjIsMapLeaf( Ntl_Obj_t * p )       { return Ntl_ObjIsPi(p) || (Ntl_ObjIsBox(p) && Ntl_BoxIsSeq(p));   } 
+static inline int         Ntl_ObjIsMapRoot( Ntl_Obj_t * p )       { return Ntl_ObjIsPo(p) || (Ntl_ObjIsBox(p) && Ntl_BoxIsSeq(p));   } 
+
+static inline int         Ntl_ObjIsCombLeaf( Ntl_Obj_t * p )      { return Ntl_ObjIsPi(p) || (Ntl_ObjIsBox(p) && (Ntl_BoxIsSeq(p) || Ntl_BoxIsBlack(p)));   } 
+static inline int         Ntl_ObjIsCombRoot( Ntl_Obj_t * p )      { return Ntl_ObjIsPo(p) || (Ntl_ObjIsBox(p) && (Ntl_BoxIsSeq(p) || Ntl_BoxIsBlack(p)));   } 
+
+static inline int         Ntl_ObjIsSeqLeaf( Ntl_Obj_t * p )       { return Ntl_ObjIsPi(p) || (Ntl_ObjIsBox(p) && Ntl_BoxIsBlack(p));   } 
+static inline int         Ntl_ObjIsSeqRoot( Ntl_Obj_t * p )       { return Ntl_ObjIsPo(p) || (Ntl_ObjIsBox(p) && Ntl_BoxIsBlack(p));   } 
+
 ////////////////////////////////////////////////////////////////////////
 ///                         ITERATORS                                ///
 ////////////////////////////////////////////////////////////////////////
@@ -203,10 +240,10 @@ static inline void        Ntl_ObjSetFanout( Ntl_Obj_t * p, Ntl_Net_t * pNet, int
     Vec_PtrForEachEntry( p->vCis, pNet, i )
 #define Ntl_ManForEachCoNet( p, pNet, i )                                       \
     Vec_PtrForEachEntry( p->vCos, pNet, i )
-#define Ntl_ManForEachNode( p, pObj, i )                                   \
+#define Ntl_ManForEachNode( p, pObj, i )                                        \
     for ( i = 0; (i < Vec_PtrSize(p->vNodes)) && (((pObj) = Vec_PtrEntry(p->vNodes, i)), 1); i++ ) \
         if ( (pObj) == NULL || !Ntl_ObjIsNode(pObj) ) {} else
-#define Ntl_ManForEachBox( p, pObj, i )                                    \
+#define Ntl_ManForEachBox( p, pObj, i )                                         \
     for ( i = 0; (i < Vec_PtrSize(p->vNodes)) && (((pObj) = Vec_PtrEntry(p->vNodes, i)), 1); i++ ) \
         if ( (pObj) == NULL || !Ntl_ObjIsBox(pObj) ) {} else
 
@@ -214,6 +251,9 @@ static inline void        Ntl_ObjSetFanout( Ntl_Obj_t * p, Ntl_Net_t * pNet, int
     for ( i = 0; (i < Vec_PtrSize(pNwk->vPis)) && (((pObj) = (Ntl_Obj_t*)Vec_PtrEntry(pNwk->vPis, i)), 1); i++ )
 #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 ) 
 #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
@@ -226,15 +266,31 @@ static inline void        Ntl_ObjSetFanout( Ntl_Obj_t * p, Ntl_Net_t * pNet, int
 #define Ntl_ModelForEachBox( 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 || !Ntl_ObjIsBox(pObj) ) {} else
-#define Ntl_ModelForEachNet( pNwk, pNet, i )                                    \
-    for ( i = 0; i < pNwk->nTableSize; i++ )                                    \
-        for ( pNet = pNwk->pTable[i]; pNet; pNet = pNet->pNext ) 
 
 #define Ntl_ObjForEachFanin( pObj, pFanin, i )                                  \
     for ( i = 0; (i < (pObj)->nFanins) && (((pFanin) = (pObj)->pFanio[i]), 1); i++ )
 #define Ntl_ObjForEachFanout( pObj, pFanout, i )                                \
     for ( i = 0; (i < (pObj)->nFanouts) && (((pFanout) = (pObj)->pFanio[(pObj)->nFanins+i]), 1); i++ )
 
+#define Ntl_ModelForEachMapLeaf( 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 || !Ntl_ObjIsMapLeaf(pObj) ) {} else
+#define Ntl_ModelForEachMapRoot( 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 || !Ntl_ObjIsMapRoot(pObj) ) {} else
+#define Ntl_ModelForEachCombLeaf( 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 || !Ntl_ObjIsCombLeaf(pObj) ) {} else
+#define Ntl_ModelForEachCombRoot( 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 || !Ntl_ObjIsCombRoot(pObj) ) {} else
+#define Ntl_ModelForEachSeqLeaf( 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 || !Ntl_ObjIsSeqLeaf(pObj) ) {} else
+#define Ntl_ModelForEachSeqRoot( 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 || !Ntl_ObjIsSeqRoot(pObj) ) {} else
+
 ////////////////////////////////////////////////////////////////////////
 ///                    FUNCTION DECLARATIONS                         ///
 ////////////////////////////////////////////////////////////////////////
@@ -247,17 +303,17 @@ extern ABC_DLL void            Ntl_ManPrepareCec( char * pFileName1, char * pFil
 extern ABC_DLL Aig_Man_t *     Ntl_ManPrepareSec( char * pFileName1, char * pFileName2 );
 /*=== ntlExtract.c ==========================================================*/
 extern ABC_DLL Aig_Man_t *     Ntl_ManExtract( Ntl_Man_t * p );
-extern ABC_DLL Aig_Man_t *     Ntl_ManCollapse( Ntl_Man_t * p, int fSeq );
-extern ABC_DLL Aig_Man_t *     Ntl_ManCollapseForCec( Ntl_Man_t * p );
-extern ABC_DLL Aig_Man_t *     Ntl_ManCollapseForSec( Ntl_Man_t * p1, Ntl_Man_t * p2 );
+extern ABC_DLL Aig_Man_t *     Ntl_ManCollapseComb( Ntl_Man_t * p );
+extern ABC_DLL Aig_Man_t *     Ntl_ManCollapseSeq( Ntl_Man_t * p );
 /*=== ntlInsert.c ==========================================================*/
 extern ABC_DLL Ntl_Man_t *     Ntl_ManInsertMapping( Ntl_Man_t * p, Vec_Ptr_t * vMapping, Aig_Man_t * pAig );
 extern ABC_DLL Ntl_Man_t *     Ntl_ManInsertAig( Ntl_Man_t * p, Aig_Man_t * pAig );
 extern ABC_DLL Ntl_Man_t *     Ntl_ManInsertNtk( Ntl_Man_t * p, Nwk_Man_t * pNtk );
 /*=== ntlCheck.c ==========================================================*/
 extern ABC_DLL int             Ntl_ManCheck( Ntl_Man_t * pMan );
-extern ABC_DLL int             Ntl_ModelCheck( Ntl_Mod_t * pModel );
+extern ABC_DLL int             Ntl_ModelCheck( Ntl_Mod_t * pModel, int fMain );
 extern ABC_DLL void            Ntl_ModelFixNonDrivenNets( Ntl_Mod_t * pModel );
+extern ABC_DLL void            Ntl_ModelTransformLatches( Ntl_Mod_t * pModel );
 /*=== ntlMan.c ============================================================*/
 extern ABC_DLL Ntl_Man_t *     Ntl_ManAlloc();
 extern ABC_DLL void            Ntl_ManCleanup( Ntl_Man_t * p );
@@ -269,10 +325,12 @@ extern ABC_DLL int             Ntl_ManLatchNum( Ntl_Man_t * p );
 extern ABC_DLL Ntl_Mod_t *     Ntl_ManFindModel( Ntl_Man_t * p, char * pName );
 extern ABC_DLL void            Ntl_ManPrintStats( Ntl_Man_t * p );
 extern ABC_DLL Tim_Man_t *     Ntl_ManReadTimeMan( Ntl_Man_t * p );
+extern ABC_DLL void            Ntl_ManPrintTypes( Ntl_Man_t * p );
 extern ABC_DLL Ntl_Mod_t *     Ntl_ModelAlloc( Ntl_Man_t * pMan, char * pName );
 extern ABC_DLL Ntl_Mod_t *     Ntl_ModelStartFrom( Ntl_Man_t * pManNew, Ntl_Mod_t * pModelOld );
 extern ABC_DLL Ntl_Mod_t *     Ntl_ModelDup( Ntl_Man_t * pManNew, Ntl_Mod_t * pModelOld );
 extern ABC_DLL void            Ntl_ModelFree( Ntl_Mod_t * p );
+extern ABC_DLL Ntl_Mod_t *     Ntl_ManCreateLatchModel( Ntl_Man_t * pMan, int Init );
 /*=== ntlMap.c ============================================================*/
 extern ABC_DLL Vec_Ptr_t *     Ntl_MappingAlloc( int nLuts, int nVars );
 extern ABC_DLL Vec_Ptr_t *     Ntl_MappingFromAig( Aig_Man_t * p );
@@ -294,11 +352,13 @@ extern ABC_DLL int             Ntl_ManSweep( Ntl_Man_t * p, int fVerbose );
 /*=== ntlTable.c ==========================================================*/
 extern ABC_DLL Ntl_Net_t *     Ntl_ModelFindNet( Ntl_Mod_t * p, char * pName );
 extern ABC_DLL Ntl_Net_t *     Ntl_ModelFindOrCreateNet( Ntl_Mod_t * p, char * pName );
-extern ABC_DLL int             Ntl_ModelFindPioNumber( Ntl_Mod_t * p, char * pName, int * pNumber );
+extern ABC_DLL int             Ntl_ModelFindPioNumber( Ntl_Mod_t * p, int fPiOnly, int fPoOnly, char * pName, int * pNumber );
 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 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, char * pName );
 /*=== ntlTime.c ==========================================================*/
 extern ABC_DLL Tim_Man_t *     Ntl_ManCreateTiming( Ntl_Man_t * p );
 /*=== ntlReadBlif.c ==========================================================*/
@@ -315,9 +375,14 @@ extern ABC_DLL Vec_Ptr_t *     Ntl_ManCollectCiNames( Ntl_Man_t * p );
 extern ABC_DLL Vec_Ptr_t *     Ntl_ManCollectCoNames( Ntl_Man_t * p );
 extern ABC_DLL void            Ntl_ManMarkCiCoNets( Ntl_Man_t * p );
 extern ABC_DLL void            Ntl_ManUnmarkCiCoNets( Ntl_Man_t * p );
-extern ABC_DLL int             Ntl_ManCheckNetsAreNotMarked( Ntl_Mod_t * pModel );
 extern ABC_DLL void            Ntl_ManSetZeroInitValues( Ntl_Man_t * p );
 extern ABC_DLL void            Ntl_ManTransformInitValues( Ntl_Man_t * p );
+extern ABC_DLL int             Ntl_ModelCombLeafNum( Ntl_Mod_t * p );
+extern ABC_DLL int             Ntl_ModelCombRootNum( Ntl_Mod_t * p );
+extern ABC_DLL int             Ntl_ModelSeqLeafNum( Ntl_Mod_t * p );
+extern ABC_DLL int             Ntl_ModelSeqRootNum( Ntl_Mod_t * p );
+extern ABC_DLL int             Ntl_ModelCheckNetsAreNotMarked( Ntl_Mod_t * pModel );
+extern ABC_DLL void            Ntl_ModelClearNets( Ntl_Mod_t * pModel );
 
 #ifdef __cplusplus
 }
diff --git a/src/aig/ntl/ntlCheck.c b/src/aig/ntl/ntlCheck.c
index d5100312..d3aecc8d 100644
--- a/src/aig/ntl/ntlCheck.c
+++ b/src/aig/ntl/ntlCheck.c
@@ -40,11 +40,100 @@
   SeeAlso     []
 
 ***********************************************************************/
-int Ntl_ModelCheck( Ntl_Mod_t * pModel )
+int Ntl_ModelCheck( Ntl_Mod_t * pModel, int fMain )
 {
     Ntl_Obj_t * pObj;
     Ntl_Net_t * pNet;
     int i, k, fStatus = 1;
+
+    // check root level model
+    if ( fMain )
+    {
+        if ( Ntl_ModelLatchNum(pModel) > 0 )
+        {
+            printf( "Root level model has %d registers.\n", pModel->pName, Ntl_ModelLatchNum(pModel) );
+            fStatus = 0;
+        }
+        goto checkobjs;
+    }
+
+    // check delay information
+    if ( pModel->attrBox && pModel->attrComb )
+    {
+        if ( pModel->vDelays == NULL )
+        {
+            printf( "Warning: Comb model %s does not have delay info. Default 1.0 delays are assumed.\n", pModel->pName );
+            pModel->vDelays = Vec_IntAlloc( 3 );
+            Vec_IntPush( pModel->vDelays, -1 );
+            Vec_IntPush( pModel->vDelays, -1 );
+            Vec_IntPush( pModel->vDelays, Aig_Float2Int(1.0) );        
+        }
+        if ( pModel->vTimeInputs != NULL )
+        {
+            printf( "Combinational model %s has input arrival/required time information.\n", pModel->pName );
+            fStatus = 0;
+        }
+        if ( pModel->vTimeOutputs != NULL )
+        {
+            printf( "Combinational model %s has output arrival/required time information.\n", pModel->pName );
+            fStatus = 0;
+        }
+    }
+    if ( pModel->attrBox && !pModel->attrComb )
+    {
+        if ( pModel->vDelays != NULL )
+        {
+            printf( "Sequential model %s has delay info.\n", pModel->pName );
+            fStatus = 0;
+        }
+        if ( pModel->vTimeInputs == NULL )
+        {
+            printf( "Warning: Seq model %s does not have input arrival/required time info. Default 0.0 is assumed.\n", pModel->pName );
+            pModel->vTimeInputs = Vec_IntAlloc( 2 );
+            Vec_IntPush( pModel->vTimeInputs, -1 );
+            Vec_IntPush( pModel->vTimeInputs, Aig_Float2Int(1.0) );        
+        }
+        if ( pModel->vTimeOutputs == NULL )
+        {
+            printf( "Warning: Seq model %s does not have output arrival/required time info. Default 0.0 is assumed.\n", pModel->pName );
+            pModel->vTimeOutputs = Vec_IntAlloc( 2 );
+            Vec_IntPush( pModel->vTimeOutputs, -1 );
+            Vec_IntPush( pModel->vTimeOutputs, Aig_Float2Int(1.0) );        
+        }
+    }
+
+    // check box attributes
+    if ( pModel->attrBox )
+    {
+        if ( !pModel->attrWhite )
+        {
+            if ( Ntl_ModelNodeNum(pModel) + Ntl_ModelLut1Num(pModel) > 0 )
+            {
+                printf( "Model %s is a blackbox, yet it has %d nodes.\n", pModel->pName, Ntl_ModelNodeNum(pModel) + Ntl_ModelLut1Num(pModel) );
+                fStatus = 0;
+            }
+            if ( Ntl_ModelLatchNum(pModel) > 0 )
+            {
+                printf( "Model %s is a blackbox, yet it has %d registers.\n", pModel->pName, Ntl_ModelLatchNum(pModel) );
+                fStatus = 0;
+            }
+            return fStatus;
+        }
+        // this is a white box
+        if ( pModel->attrComb && Ntl_ModelNodeNum(pModel) + Ntl_ModelLut1Num(pModel) == 0 )
+        {
+            printf( "Model %s is a comb blackbox, yet it has no nodes.\n", pModel->pName );
+            fStatus = 0;
+        }
+        if ( !pModel->attrComb && Ntl_ModelLatchNum(pModel) == 0 )
+        {
+            printf( "Model %s is a seq blackbox, yet it has no registers.\n", pModel->pName );
+            fStatus = 0;
+        }
+    }
+
+checkobjs:
+    // check nets
     Ntl_ModelForEachNet( pModel, pNet, i )
     {
         if ( pNet->pName == NULL )
@@ -58,6 +147,8 @@ int Ntl_ModelCheck( Ntl_Mod_t * pModel )
             fStatus = 0;
         }
     }
+
+    // check objects
     Ntl_ModelForEachObj( pModel, pObj, i )
     {
         Ntl_ObjForEachFanin( pObj, pNet, k )
@@ -89,8 +180,8 @@ int Ntl_ModelCheck( Ntl_Mod_t * pModel )
 ***********************************************************************/
 int Ntl_ManCheck( Ntl_Man_t * pMan )
 {
-    Ntl_Mod_t * pMod1, * pMod2;
-    int i, k, fStatus = 1;
+    Ntl_Mod_t * pMod1;
+    int i, fStatus = 1;
     // check that the models have unique names
     Ntl_ManForEachModel( pMan, pMod1, i )
     {
@@ -99,16 +190,6 @@ int Ntl_ManCheck( Ntl_Man_t * pMan )
             printf( "Model %d does not have a name\n", i );
             fStatus = 0;
         }
-        Ntl_ManForEachModel( pMan, pMod2, k )
-        {
-            if ( i >= k )
-                continue;
-            if ( strcmp(pMod1->pName, pMod2->pName) == 0 )
-            {
-                printf( "Models %d and %d have the same name (%s).\n", i, k, pMod1->pName );
-                fStatus = 0;
-            }
-        }
     }
     // check that the models (except the first one) do not have boxes
     Ntl_ManForEachModel( pMan, pMod1, i )
@@ -124,9 +205,8 @@ int Ntl_ManCheck( Ntl_Man_t * pMan )
     // check models
     Ntl_ManForEachModel( pMan, pMod1, i )
     {
-        if ( !Ntl_ModelCheck( pMod1 ) )
+        if ( !Ntl_ModelCheck( pMod1, i==0 ) )
             fStatus = 0;
-        break;
     }
     return fStatus;
 }
@@ -150,7 +230,7 @@ void Ntl_ModelFixNonDrivenNets( Ntl_Mod_t * pModel )
     Ntl_Obj_t * pNode;
     int i;
 
-    if ( Ntl_ModelIsBlackBox(pModel) )
+    if ( !pModel->attrWhite )
         return;
 
     // check for non-driven nets
@@ -186,6 +266,37 @@ void Ntl_ModelFixNonDrivenNets( Ntl_Mod_t * pModel )
     Vec_PtrFree( vNets );
 }
 
+/**Function*************************************************************
+
+  Synopsis    [Fixed problems with non-driven nets in the model.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Ntl_ModelTransformLatches( Ntl_Mod_t * pModel )
+{ 
+    Ntl_Mod_t * pMod[3] = { NULL };
+    Ntl_Obj_t * pLatch;
+    int i, Init;
+    if ( Ntl_ModelLatchNum(pModel) == 0 )
+        return;
+    Ntl_ModelForEachLatch( pModel, pLatch, i )
+    {
+        Init = pLatch->LatchId.regInit;
+        if ( pMod[Init] == NULL )
+            pMod[Init] = Ntl_ManCreateLatchModel( pModel->pMan, Init );
+        pLatch->pImplem = pMod[Init];
+        pLatch->Type = NTL_OBJ_BOX;
+    }
+    printf( "Root level model %s: %d registers turned into white seq boxes.\n", pModel->pName, Ntl_ModelLatchNum(pModel) );
+    pModel->nObjs[NTL_OBJ_BOX] += Ntl_ModelLatchNum(pModel);
+    pModel->nObjs[NTL_OBJ_LATCH] = 0;
+}
+
 
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
diff --git a/src/aig/ntl/ntlEc.c b/src/aig/ntl/ntlEc.c
index 8c7f7156..3ed6556d 100644
--- a/src/aig/ntl/ntlEc.c
+++ b/src/aig/ntl/ntlEc.c
@@ -42,33 +42,48 @@
 void Ntl_ManCreateMissingInputs( Ntl_Mod_t * p1, Ntl_Mod_t * p2, int fSeq )
 {
     Ntl_Obj_t * pObj;
-    Ntl_Net_t * pNet;
-    int i;
-    Ntl_ModelForEachPi( p1, pObj, i )
-    {
-        pNet = Ntl_ModelFindNet( p2, Ntl_ObjFanout0(pObj)->pName );
-        if ( pNet == NULL )
-            Ntl_ModelCreatePiWithName( p2, Ntl_ObjFanout0(pObj)->pName );
-    }
-    Ntl_ModelForEachPi( p2, pObj, i )
+    Ntl_Net_t * pNet, * pNext;
+    int i, k;
+    if ( fSeq )
     {
-        pNet = Ntl_ModelFindNet( p1, Ntl_ObjFanout0(pObj)->pName );
-        if ( pNet == NULL )
-            Ntl_ModelCreatePiWithName( p1, Ntl_ObjFanout0(pObj)->pName );
+        Ntl_ModelForEachSeqLeaf( p1, pObj, i )
+        {
+            Ntl_ObjForEachFanout( pObj, pNext, k )
+            {
+                pNet = Ntl_ModelFindNet( p2, pNext->pName );
+                if ( pNet == NULL )
+                    Ntl_ModelCreatePiWithName( p2, pNext->pName );
+            }
+        }
+        Ntl_ModelForEachSeqLeaf( p2, pObj, i )
+        {
+            Ntl_ObjForEachFanout( pObj, pNext, k )
+            {
+                pNet = Ntl_ModelFindNet( p1, pNext->pName );
+                if ( pNet == NULL )
+                    Ntl_ModelCreatePiWithName( p1, pNext->pName );
+            }
+        }
     }
-    if ( !fSeq )
+    else
     {
-        Ntl_ModelForEachLatch( p1, pObj, i )
+        Ntl_ModelForEachCombLeaf( p1, pObj, i )
         {
-            pNet = Ntl_ModelFindNet( p2, Ntl_ObjFanout0(pObj)->pName );
-            if ( pNet == NULL )
-                Ntl_ModelCreatePiWithName( p2, Ntl_ObjFanout0(pObj)->pName );
+            Ntl_ObjForEachFanout( pObj, pNext, k )
+            {
+                pNet = Ntl_ModelFindNet( p2, pNext->pName );
+                if ( pNet == NULL )
+                    Ntl_ModelCreatePiWithName( p2, pNext->pName );
+            }
         }
-        Ntl_ModelForEachLatch( p2, pObj, i )
+        Ntl_ModelForEachCombLeaf( p2, pObj, i )
         {
-            pNet = Ntl_ModelFindNet( p1, Ntl_ObjFanout0(pObj)->pName );
-            if ( pNet == NULL )
-                Ntl_ModelCreatePiWithName( p1, Ntl_ObjFanout0(pObj)->pName );
+            Ntl_ObjForEachFanout( pObj, pNext, k )
+            {
+                pNet = Ntl_ModelFindNet( p1, pNext->pName );
+                if ( pNet == NULL )
+                    Ntl_ModelCreatePiWithName( p1, pNext->pName );
+            }
         }
     }
 }
@@ -89,38 +104,45 @@ void Ntl_ManDeriveCommonCis( Ntl_Man_t * pMan1, Ntl_Man_t * pMan2, int fSeq )
     Ntl_Mod_t * p1 = Ntl_ManRootModel(pMan1);
     Ntl_Mod_t * p2 = Ntl_ManRootModel(pMan2);
     Ntl_Obj_t * pObj;
-    Ntl_Net_t * pNet;
-    int i;
-    if ( fSeq )
-        assert( Ntl_ModelPiNum(p1) == Ntl_ModelPiNum(p2) );
-    else
-        assert( Ntl_ModelCiNum(p1) == Ntl_ModelCiNum(p2) );
+    Ntl_Net_t * pNet, * pNext;
+    int i, k;
     // order the CIs 
     Vec_PtrClear( pMan1->vCis );
     Vec_PtrClear( pMan2->vCis );
-    Ntl_ModelForEachPi( p1, pObj, i )
+    if ( fSeq ) 
     {
-        pNet = Ntl_ModelFindNet( p2, Ntl_ObjFanout0(pObj)->pName );
-        if ( pNet == NULL )
+        assert( Ntl_ModelSeqLeafNum(p1) == Ntl_ModelSeqLeafNum(p2) );
+        Ntl_ModelForEachSeqLeaf( p1, pObj, i )
         {
-            printf( "Ntl_ManDeriveCommonCis(): Internal error!\n" );
-            return;
+            Ntl_ObjForEachFanout( pObj, pNext, k )
+            {
+                pNet = Ntl_ModelFindNet( p2, pNext->pName );
+                if ( pNet == NULL )
+                {
+                    printf( "Ntl_ManDeriveCommonCis(): Internal error!\n" );
+                    return;
+                }
+                Vec_PtrPush( pMan1->vCis, pNext );    
+                Vec_PtrPush( pMan2->vCis, pNet );  
+            }
         }
-        Vec_PtrPush( pMan1->vCis, pObj );    
-        Vec_PtrPush( pMan2->vCis, pNet->pDriver );    
     }
-    if ( !fSeq )
+    else
     {
-        Ntl_ModelForEachLatch( p1, pObj, i )
+        assert( Ntl_ModelCombLeafNum(p1) == Ntl_ModelCombLeafNum(p2) );
+        Ntl_ModelForEachCombLeaf( p1, pObj, i )
         {
-            pNet = Ntl_ModelFindNet( p2, Ntl_ObjFanout0(pObj)->pName );
-            if ( pNet == NULL )
+            Ntl_ObjForEachFanout( pObj, pNext, k )
             {
-                printf( "Ntl_ManDeriveCommonCis(): Internal error!\n" );
-                return;
+                pNet = Ntl_ModelFindNet( p2, pNext->pName );
+                if ( pNet == NULL )
+                {
+                    printf( "Ntl_ManDeriveCommonCis(): Internal error!\n" );
+                    return;
+                }
+                Vec_PtrPush( pMan1->vCis, pNext );    
+                Vec_PtrPush( pMan2->vCis, pNet );  
             }
-            Vec_PtrPush( pMan1->vCis, pObj );    
-            Vec_PtrPush( pMan2->vCis, pNet->pDriver );    
         }
     }
 }
@@ -141,45 +163,47 @@ void Ntl_ManDeriveCommonCos( Ntl_Man_t * pMan1, Ntl_Man_t * pMan2, int fSeq )
     Ntl_Mod_t * p1 = Ntl_ManRootModel(pMan1);
     Ntl_Mod_t * p2 = Ntl_ManRootModel(pMan2);
     Ntl_Obj_t * pObj;
-    Ntl_Net_t * pNet;
-    int i;
-//    if ( fSeq )
-//        assert( Ntl_ModelPoNum(p1) == Ntl_ModelPoNum(p2) );
-//    else
-//        assert( Ntl_ModelCoNum(p1) == Ntl_ModelCoNum(p2) );
-    // remember PO in the corresponding net of the second design
-    Ntl_ModelForEachPo( p2, pObj, i )
-        Ntl_ObjFanin0(pObj)->pCopy = pObj;
+    Ntl_Net_t * pNet, * pNext;
+    int i, k;
     // order the COs 
     Vec_PtrClear( pMan1->vCos );
     Vec_PtrClear( pMan2->vCos );
-    Ntl_ModelForEachPo( p1, pObj, i )
+    if ( fSeq ) 
     {
-        pNet = Ntl_ModelFindNet( p2, Ntl_ObjFanin0(pObj)->pName );
-        if ( pNet == NULL )
+        assert( Ntl_ModelSeqRootNum(p1) == Ntl_ModelSeqRootNum(p2) );
+        Ntl_ModelForEachSeqRoot( p1, pObj, i )
         {
-            printf( "Ntl_ManDeriveCommonCos(): Cannot find output %s in the second design. Skipping it!\n", 
-                Ntl_ObjFanin0(pObj)->pName );
-            continue;
+            Ntl_ObjForEachFanin( pObj, pNext, k )
+            {
+                pNet = Ntl_ModelFindNet( p2, pNext->pName );
+                if ( pNet == NULL )
+                {
+                    printf( "Ntl_ManDeriveCommonCos(): Cannot find output %s in the second design. Skipping it!\n", 
+                        pNext->pName );
+                    continue;
+                }
+                Vec_PtrPush( pMan1->vCos, pNext );    
+                Vec_PtrPush( pMan2->vCos, pNet );  
+            }
         }
-        Vec_PtrPush( pMan1->vCos, pObj );    
-        Vec_PtrPush( pMan2->vCos, pNet->pCopy );    
     }
-    if ( !fSeq )
+    else
     {
-        Ntl_ModelForEachLatch( p2, pObj, i )
-            Ntl_ObjFanin0(pObj)->pCopy = pObj;
-        Ntl_ModelForEachLatch( p1, pObj, i )
+        assert( Ntl_ModelCombRootNum(p1) == Ntl_ModelCombRootNum(p2) );
+        Ntl_ModelForEachCombRoot( p1, pObj, i )
         {
-            pNet = Ntl_ModelFindNet( p2, Ntl_ObjFanin0(pObj)->pName );
-            if ( pNet == NULL )
+            Ntl_ObjForEachFanin( pObj, pNext, k )
             {
-                printf( "Ntl_ManDeriveCommonCos(): Cannot find output %s in the second design. Skipping it!\n", 
-                    Ntl_ObjFanin0(pObj)->pName );
-                continue;
+                pNet = Ntl_ModelFindNet( p2, pNext->pName );
+                if ( pNet == NULL )
+                {
+                    printf( "Ntl_ManDeriveCommonCos(): Cannot find output %s in the second design. Skipping it!\n", 
+                        pNext->pName );
+                    continue;
+                }
+                Vec_PtrPush( pMan1->vCos, pNext );    
+                Vec_PtrPush( pMan2->vCos, pNet );  
             }
-            Vec_PtrPush( pMan1->vCos, pObj );    
-            Vec_PtrPush( pMan2->vCos, pNet->pCopy );    
         }
     }
 }
@@ -214,19 +238,19 @@ void Ntl_ManPrepareCec( char * pFileName1, char * pFileName2, Aig_Man_t ** ppMan
     // make sure they are compatible
     pModel1 = Ntl_ManRootModel( pMan1 );
     pModel2 = Ntl_ManRootModel( pMan2 );
-    if ( Ntl_ModelCiNum(pModel1) != Ntl_ModelCiNum(pModel2) )
+    if ( Ntl_ModelCombLeafNum(pModel1) != Ntl_ModelCombLeafNum(pModel2) )
     {
         printf( "Warning: The number of inputs in the designs is different (%d and %d).\n", 
-            Ntl_ModelCiNum(pModel1), Ntl_ModelCiNum(pModel2) );
+            Ntl_ModelCombLeafNum(pModel1), Ntl_ModelCombLeafNum(pModel2) );
     }
-    if ( Ntl_ModelCoNum(pModel1) != Ntl_ModelCoNum(pModel2) )
+    if ( Ntl_ModelCombRootNum(pModel1) != Ntl_ModelCombRootNum(pModel2) )
     {
         printf( "Warning: The number of outputs in the designs is different (%d and %d).\n", 
-            Ntl_ModelCoNum(pModel1), Ntl_ModelCoNum(pModel2) );
+            Ntl_ModelCombRootNum(pModel1), Ntl_ModelCombRootNum(pModel2) );
     }
     // normalize inputs/outputs
     Ntl_ManCreateMissingInputs( pModel1, pModel2, 0 );
-    if ( Ntl_ModelCiNum(pModel1) != Ntl_ModelCiNum(pModel2) )
+    if ( Ntl_ModelCombLeafNum(pModel1) != Ntl_ModelCombLeafNum(pModel2) )
     {
         if ( pMan1 )  Ntl_ManFree( pMan1 );
         if ( pMan2 )  Ntl_ManFree( pMan2 );
@@ -243,8 +267,8 @@ void Ntl_ManPrepareCec( char * pFileName1, char * pFileName2, Aig_Man_t ** ppMan
         return;
     }
     // derive AIGs
-    *ppMan1 = Ntl_ManCollapseForCec( pMan1 );
-    *ppMan2 = Ntl_ManCollapseForCec( pMan2 );
+    *ppMan1 = Ntl_ManCollapseComb( pMan1 );
+    *ppMan2 = Ntl_ManCollapseComb( pMan2 );
     // cleanup 
     Ntl_ManFree( pMan1 );
     Ntl_ManFree( pMan2 );
@@ -263,7 +287,9 @@ void Ntl_ManPrepareCec( char * pFileName1, char * pFileName2, Aig_Man_t ** ppMan
 ***********************************************************************/
 Aig_Man_t * Ntl_ManPrepareSec( char * pFileName1, char * pFileName2 )
 {
-    Aig_Man_t * pAig;
+    extern Aig_Man_t * Saig_ManCreateMiter( Aig_Man_t * p1, Aig_Man_t * p2, int Oper );
+
+    Aig_Man_t * pAig1, * pAig2, * pAig;
     Ntl_Man_t * pMan1, * pMan2;
     Ntl_Mod_t * pModel1, * pModel2;
     // read the netlists
@@ -286,12 +312,12 @@ Aig_Man_t * Ntl_ManPrepareSec( char * pFileName1, char * pFileName2 )
         printf( "Ntl_ManPrepareSec(): The designs have no latches. Use combinational command \"*cec\".\n" );
         return NULL;
     }
-    if ( Ntl_ModelPiNum(pModel1) != Ntl_ModelPiNum(pModel2) )
+    if ( Ntl_ModelSeqLeafNum(pModel1) != Ntl_ModelSeqLeafNum(pModel2) )
     {
         printf( "Warning: The number of inputs in the designs is different (%d and %d).\n", 
             Ntl_ModelPiNum(pModel1), Ntl_ModelPiNum(pModel2) );
     }
-    if ( Ntl_ModelPoNum(pModel1) != Ntl_ModelPoNum(pModel2) )
+    if ( Ntl_ModelSeqRootNum(pModel1) != Ntl_ModelSeqRootNum(pModel2) )
     {
         printf( "Warning: The number of outputs in the designs is different (%d and %d).\n", 
             Ntl_ModelPoNum(pModel1), Ntl_ModelPoNum(pModel2) );
@@ -308,9 +334,12 @@ Aig_Man_t * Ntl_ManPrepareSec( char * pFileName1, char * pFileName2 )
         return NULL;
     }
     // derive AIGs
-    pAig = Ntl_ManCollapseForSec( pMan1, pMan2 );
+    pAig1 = Ntl_ManCollapseSeq( pMan1 );
+    pAig2 = Ntl_ManCollapseSeq( pMan2 );
+    pAig = Saig_ManCreateMiter( pAig1, pAig2, 0 );
+    Aig_ManStop( pAig1 );
+    Aig_ManStop( pAig2 );
     // cleanup
-    pMan1->pAig = pMan2->pAig = NULL;
     Ntl_ManFree( pMan1 );
     Ntl_ManFree( pMan2 );
     return pAig;
diff --git a/src/aig/ntl/ntlExtract.c b/src/aig/ntl/ntlExtract.c
index be6626df..a552f949 100644
--- a/src/aig/ntl/ntlExtract.c
+++ b/src/aig/ntl/ntlExtract.c
@@ -178,6 +178,9 @@ int Ntl_ManExtract_rec( Ntl_Man_t * p, Ntl_Net_t * pNet )
     if ( Ntl_ObjIsBox(pObj) )
     {
         int LevelCur, LevelMax = -TIM_ETERNITY;
+        assert( Ntl_BoxIsComb(pObj) );
+        assert( Ntl_ModelLatchNum(pObj->pImplem) == 0 );
+        assert( pObj->pImplem->vDelays != NULL );
         Vec_IntPush( p->vBox1Cos, Aig_ManPoNum(p->pAig) );
         Ntl_ObjForEachFanin( pObj, pNetFanin, i )
         {
@@ -218,7 +221,7 @@ Aig_Man_t * Ntl_ManExtract( Ntl_Man_t * p )
     Ntl_Mod_t * pRoot;
     Ntl_Obj_t * pObj;
     Ntl_Net_t * pNet;
-    int i, nUselessObjects;
+    int i, k, nUselessObjects;
     Ntl_ManCleanup( p );
     assert( Vec_PtrSize(p->vCis) == 0 );
     assert( Vec_PtrSize(p->vCos) == 0 );
@@ -231,63 +234,39 @@ Aig_Man_t * Ntl_ManExtract( Ntl_Man_t * p )
     p->pAig->pSpec = Aig_UtilStrsav( p->pSpec );
     // get the root model
     pRoot = Ntl_ManRootModel( p );
+    assert( Ntl_ModelLatchNum(pRoot) == 0 );
     // clear net visited flags
-    Ntl_ModelForEachNet( pRoot, pNet, i )
+    Ntl_ModelClearNets( pRoot );
+    // collect mapping leafs
+    Ntl_ModelForEachMapLeaf( pRoot, pObj, i )
     {
-        pNet->nVisits = 0;
-        pNet->pCopy = NULL;
-    }
-    // collect primary inputs
-    Ntl_ModelForEachPi( pRoot, pObj, i )
-    {
-        assert( Ntl_ObjFanoutNum(pObj) == 1 );
-        pNet = Ntl_ObjFanout0(pObj);
-        Vec_PtrPush( p->vCis, pNet );
-        pNet->pCopy = Aig_ObjCreatePi( p->pAig );
-        if ( pNet->nVisits )
-        {
-            printf( "Ntl_ManExtract(): Primary input appears twice in the list.\n" );
-            return 0;
-        }
-        pNet->nVisits = 2;
-    }
-    // collect latch outputs
-    Ntl_ModelForEachLatch( pRoot, pObj, i )
-    {
-        assert( Ntl_ObjFanoutNum(pObj) == 1 );
-        pNet = Ntl_ObjFanout0(pObj);
-        Vec_PtrPush( p->vCis, pNet );
-        pNet->pCopy = Aig_ObjCreatePi( p->pAig );
-        if ( pNet->nVisits )
+        assert( !Ntl_ObjIsBox(pObj) || Ntl_BoxIsBlack(pObj) || Ntl_ModelLatchNum(pObj->pImplem) > 0 );
+        Ntl_ObjForEachFanout( pObj, pNet, k )
         {
-            printf( "Ntl_ManExtract(): Latch output is duplicated or defined as a primary input.\n" );
-            return 0;
+            Vec_PtrPush( p->vCis, pNet );
+            pNet->pCopy = Aig_ObjCreatePi( p->pAig );
+            if ( pNet->nVisits )
+            {
+                printf( "Ntl_ManExtract(): Seq leaf is duplicated or defined as a primary input.\n" );
+                return 0;
+            }
+            pNet->nVisits = 2;
         }
-        pNet->nVisits = 2;
     }
-    // visit the nodes starting from primary outputs
-    Ntl_ModelForEachPo( pRoot, pObj, i )
+    p->iLastCi = Aig_ManPiNum(p->pAig);
+    // collect mapping roots
+    Ntl_ModelForEachMapRoot( pRoot, pObj, i )
     {
-        pNet = Ntl_ObjFanin0(pObj);
-        if ( !Ntl_ManExtract_rec( p, pNet ) )
-        {
-            printf( "Ntl_ManExtract(): Error: Combinational loop is detected.\n" );
-            return 0;
-        }
-        Vec_PtrPush( p->vCos, pNet );
-        Aig_ObjCreatePo( p->pAig, pNet->pCopy );
-    }
-    // visit the nodes starting from latch inputs 
-    Ntl_ModelForEachLatch( pRoot, pObj, i )
-    {
-        pNet = Ntl_ObjFanin0(pObj);
-        if ( !Ntl_ManExtract_rec( p, pNet ) )
+        Ntl_ObjForEachFanin( pObj, pNet, k )
         {
-            printf( "Ntl_ManExtract(): Error: Combinational loop is detected.\n" );
-            return 0;
+            if ( !Ntl_ManExtract_rec( p, pNet ) )
+            {
+                printf( "Ntl_ManExtract(): Error: Combinational loop is detected.\n" );
+                return 0;
+            }
+            Vec_PtrPush( p->vCos, pNet );
+            Aig_ObjCreatePo( p->pAig, pNet->pCopy );
         }
-        Vec_PtrPush( p->vCos, pNet );
-        Aig_ObjCreatePo( p->pAig, pNet->pCopy );
     }
     // visit dangling boxes
     Ntl_ModelForEachBox( pRoot, pObj, i )
@@ -314,6 +293,9 @@ Aig_Man_t * Ntl_ManExtract( Ntl_Man_t * p )
     return pAig;    
 }
 
+
+
+
 /**Function*************************************************************
 
   Synopsis    [Collects the nodes in a topological order.]
@@ -325,9 +307,9 @@ Aig_Man_t * Ntl_ManExtract( Ntl_Man_t * p )
   SeeAlso     []
 
 ***********************************************************************/
-int Ntl_ManBuildModelAig( Ntl_Man_t * p, Ntl_Obj_t * pBox )
+int Ntl_ManCollapseBox_rec( Ntl_Man_t * p, Ntl_Obj_t * pBox, int fSeq )
 {
-    extern int Ntl_ManCollapse_rec( Ntl_Man_t * p, Ntl_Net_t * pNet );
+    extern int Ntl_ManCollapse_rec( Ntl_Man_t * p, Ntl_Net_t * pNet, int fSeq );
     Ntl_Mod_t * pModel = pBox->pImplem;
     Ntl_Obj_t * pObj;
     Ntl_Net_t * pNet, * pNetBox;
@@ -335,8 +317,7 @@ int Ntl_ManBuildModelAig( Ntl_Man_t * p, Ntl_Obj_t * pBox )
     assert( Ntl_ObjFaninNum(pBox) == Ntl_ModelPiNum(pModel) );
     assert( Ntl_ObjFanoutNum(pBox) == Ntl_ModelPoNum(pModel) );
     // clear net visited flags
-    Ntl_ModelForEachNet( pModel, pNet, i )
-        pNet->nVisits = 0;
+    Ntl_ModelClearNets( pModel );
     // transfer from the box to the PIs of the model
     Ntl_ModelForEachPi( pModel, pObj, i )
     {
@@ -345,17 +326,41 @@ int Ntl_ManBuildModelAig( Ntl_Man_t * p, Ntl_Obj_t * pBox )
         pNet->pCopy = pNetBox->pCopy;
         pNet->nVisits = 2;
     }
+    // check if there are registers
+    if ( Ntl_ModelLatchNum(pModel) )
+    {
+        Ntl_ModelForEachLatch( pModel, pObj, i )
+        {
+            pNet = Ntl_ObjFanout0(pObj);
+            pNet->pCopy = Aig_ObjCreatePi( p->pAig );
+            if ( fSeq && Ntl_ObjIsInit1( pObj ) )
+                pNet->pCopy = Aig_Not(pNet->pCopy);
+            pNet->nVisits = 2;
+        }
+    }
     // compute AIG for the internal nodes
     Ntl_ModelForEachPo( pModel, pObj, i )
-        if ( !Ntl_ManCollapse_rec( p, Ntl_ObjFanin0(pObj) ) )
-            return 0;
-    // transfer from the POs of the model to the box
-    Ntl_ModelForEachPo( pModel, pObj, i )
     {
         pNet = Ntl_ObjFanin0(pObj);
+        if ( !Ntl_ManCollapse_rec( p, pNet, fSeq ) )
+            return 0;
         pNetBox = Ntl_ObjFanout( pBox, i );
         pNetBox->pCopy = pNet->pCopy;
     }
+    // compute AIGs for the registers
+    if ( Ntl_ModelLatchNum(pModel) )
+    {
+        Ntl_ModelForEachLatch( pModel, pObj, i )
+        {
+            pNet = Ntl_ObjFanin0(pObj);
+            if ( !Ntl_ManCollapse_rec( p, pNet, fSeq ) )
+                return 0;
+            if ( fSeq && Ntl_ObjIsInit1( pObj ) )
+                Vec_PtrPush( p->vLatchIns, Aig_Not(pNet->pCopy) );
+            else
+                Vec_PtrPush( p->vLatchIns, pNet->pCopy );
+        }
+    }
     return 1;
 }
 
@@ -370,7 +375,7 @@ int Ntl_ManBuildModelAig( Ntl_Man_t * p, Ntl_Obj_t * pBox )
   SeeAlso     []
 
 ***********************************************************************/
-int Ntl_ManCollapse_rec( Ntl_Man_t * p, Ntl_Net_t * pNet )
+int Ntl_ManCollapse_rec( Ntl_Man_t * p, Ntl_Net_t * pNet, int fSeq )
 {
     Ntl_Obj_t * pObj;
     Ntl_Net_t * pNetFanin;
@@ -388,12 +393,13 @@ int Ntl_ManCollapse_rec( Ntl_Man_t * p, Ntl_Net_t * pNet )
     assert( Ntl_ObjIsNode(pObj) || Ntl_ObjIsBox(pObj) );
     // visit the input nets of the box
     Ntl_ObjForEachFanin( pObj, pNetFanin, i )
-        if ( !Ntl_ManCollapse_rec( p, pNetFanin ) )
+        if ( !Ntl_ManCollapse_rec( p, pNetFanin, fSeq ) )
             return 0;
     // add box inputs/outputs to COs/CIs
     if ( Ntl_ObjIsBox(pObj) )
     {
-        if ( !Ntl_ManBuildModelAig( p, pObj ) )
+        assert( Ntl_BoxIsWhite(pObj) );
+        if ( !Ntl_ManCollapseBox_rec( p, pObj, fSeq ) )
             return 0;
     }
     if ( Ntl_ObjIsNode(pObj) )
@@ -417,310 +423,125 @@ int Ntl_ManCollapse_rec( Ntl_Man_t * p, Ntl_Net_t * pNet )
 Aig_Man_t * Ntl_ManCollapse( Ntl_Man_t * p, int fSeq )
 {
     Aig_Man_t * pAig;
+    Aig_Obj_t * pTemp;
     Ntl_Mod_t * pRoot;
-    Ntl_Obj_t * pObj;
     Ntl_Net_t * pNet;
     int i;
-    // start the AIG manager
-    assert( p->pAig == NULL );
+    assert( Vec_PtrSize(p->vCis) != 0 );
+    assert( Vec_PtrSize(p->vCos) != 0 );
+    assert( Vec_PtrSize(p->vLatchIns) == 0 );
+    // clear net visited flags
+    pRoot = Ntl_ManRootModel(p);
+    Ntl_ModelClearNets( pRoot );
+    assert( Ntl_ModelLatchNum(pRoot) == 0 );
+    // create the manager
     p->pAig = Aig_ManStart( 10000 );
     p->pAig->pName = Aig_UtilStrsav( p->pName );
     p->pAig->pSpec = Aig_UtilStrsav( p->pSpec );
-    // get the root model
-    pRoot = Ntl_ManRootModel( p );
-    // clear net visited flags
-    Ntl_ModelForEachNet( pRoot, pNet, i )
-    {
-        pNet->nVisits = 0;
-        pNet->pCopy = NULL;
-    }
-    // collect primary inputs
-    Ntl_ModelForEachPi( pRoot, pObj, i )
-    {
-        assert( Ntl_ObjFanoutNum(pObj) == 1 );
-        pNet = Ntl_ObjFanout0(pObj);
-        pNet->pCopy = Aig_ObjCreatePi( p->pAig );
-        if ( pNet->nVisits )
-        {
-            printf( "Ntl_ManCollapse(): Primary input appears twice in the list.\n" );
-            return 0;
-        }
-        pNet->nVisits = 2;
-    }
-    // collect latch outputs
-    Ntl_ModelForEachLatch( pRoot, pObj, i )
+    // set the inputs
+    Ntl_ManForEachCiNet( p, pNet, i )
     {
-        assert( Ntl_ObjFanoutNum(pObj) == 1 );
-        pNet = Ntl_ObjFanout0(pObj);
         pNet->pCopy = Aig_ObjCreatePi( p->pAig );
-        if ( fSeq && (pObj->LatchId & 3) == 1 )
-            pNet->pCopy = Aig_Not(pNet->pCopy);
         if ( pNet->nVisits )
         {
-            printf( "Ntl_ManCollapse(): Latch output is duplicated or defined as a primary input.\n" );
+            printf( "Ntl_ManCollapseForCec(): Primary input appears twice in the list.\n" );
             return 0;
         }
         pNet->nVisits = 2;
     }
-    // visit the nodes starting from primary outputs
-    Ntl_ModelForEachPo( pRoot, pObj, i )
+    // derive the outputs
+    Ntl_ManForEachCoNet( p, pNet, i )
     {
-        pNet = Ntl_ObjFanin0(pObj);
-        if ( !Ntl_ManCollapse_rec( p, pNet ) )
+        if ( !Ntl_ManCollapse_rec( p, pNet, fSeq ) )
         {
-            printf( "Ntl_ManCollapse(): Error: Combinational loop is detected.\n" );
+            printf( "Ntl_ManCollapseForCec(): Error: Combinational loop is detected.\n" );
             return 0;
         }
         Aig_ObjCreatePo( p->pAig, pNet->pCopy );
     }
-    // visit the nodes starting from latch inputs outputs
-    Ntl_ModelForEachLatch( pRoot, pObj, i )
-    {
-        pNet = Ntl_ObjFanin0(pObj);
-        if ( !Ntl_ManCollapse_rec( p, pNet ) )
-        {
-            printf( "Ntl_ManCollapse(): Error: Combinational loop is detected.\n" );
-            return 0;
-        }
-        if ( fSeq && (pObj->LatchId & 3) == 1 )
-            Aig_ObjCreatePo( p->pAig, Aig_Not(pNet->pCopy) );
-        else
-            Aig_ObjCreatePo( p->pAig, pNet->pCopy );
-    }
+    // add the latch inputs
+    Vec_PtrForEachEntry( p->vLatchIns, pTemp, i )
+        Aig_ObjCreatePo( p->pAig, pTemp );
     // cleanup the AIG
+    Aig_ManSetRegNum( p->pAig, Vec_PtrSize(p->vLatchIns) );
     Aig_ManCleanup( p->pAig );
     pAig = p->pAig; p->pAig = NULL;
     return pAig;    
 }
 
+
 /**Function*************************************************************
 
-  Synopsis    [Derives AIG for CEC.]
+  Synopsis    [Collapses the netlist combinationally.]
 
-  Description [Uses CIs/COs collected in the internal arrays.]
+  Description [Checks for combinational loops. Collects PI/PO nets.
+  Collects nodes in the topological order.]
                
   SideEffects []
 
   SeeAlso     []
 
 ***********************************************************************/
-Aig_Man_t * Ntl_ManCollapseForCec( Ntl_Man_t * p )
+Aig_Man_t * Ntl_ManCollapseComb( Ntl_Man_t * p )
 {
-    Aig_Man_t * pAig;
     Ntl_Mod_t * pRoot;
     Ntl_Obj_t * pObj;
     Ntl_Net_t * pNet;
-    int i;
-    // clear net visited flags
+    int i, k;
+    Vec_PtrClear( p->vCis );
+    Vec_PtrClear( p->vCos );
+    Vec_PtrClear( p->vLatchIns );
+    // prepare the model
     pRoot = Ntl_ManRootModel(p);
-    Ntl_ModelForEachNet( pRoot, pNet, i )
-    {
-        pNet->nVisits = 0;
-        pNet->pCopy = NULL;
-    }
-    // create the manager
-    p->pAig = Aig_ManStart( 10000 );
-    p->pAig->pName = Aig_UtilStrsav( p->pName );
-    p->pAig->pSpec = Aig_UtilStrsav( p->pSpec );
-    // set the inputs
-    Ntl_ManForEachCiNet( p, pObj, i )
-    {
-        assert( Ntl_ObjFanoutNum(pObj) == 1 );
-        pNet = Ntl_ObjFanout0(pObj);
-        pNet->pCopy = Aig_ObjCreatePi( p->pAig );
-        if ( pNet->nVisits )
-        {
-            printf( "Ntl_ManCollapseForCec(): Primary input appears twice in the list.\n" );
-            return 0;
-        }
-        pNet->nVisits = 2;
-    }
-    // derive the outputs
-    Ntl_ManForEachCoNet( p, pObj, i )
-    {
-        pNet = Ntl_ObjFanin0(pObj);
-        if ( !Ntl_ManCollapse_rec( p, pNet ) )
-        {
-            printf( "Ntl_ManCollapseForCec(): Error: Combinational loop is detected.\n" );
-            return 0;
-        }
-        Aig_ObjCreatePo( p->pAig, pNet->pCopy );
-    }
-    // cleanup the AIG
-    Aig_ManCleanup( p->pAig );
-    pAig = p->pAig; p->pAig = NULL;
-    return pAig;    
+    // collect the leaves for this traversal
+    Ntl_ModelForEachCombLeaf( pRoot, pObj, i )
+        Ntl_ObjForEachFanout( pObj, pNet, k )
+            Vec_PtrPush( p->vCis, pNet );
+    // collect the roots for this traversal
+    Ntl_ModelForEachCombRoot( pRoot, pObj, i )
+        Ntl_ObjForEachFanin( pObj, pNet, k )
+            Vec_PtrPush( p->vCos, pNet );
+    // perform the traversal
+    return Ntl_ManCollapse( p, 0 );
 }
 
 /**Function*************************************************************
 
-  Synopsis    [Derives AIG for SEC.]
+  Synopsis    [Collapses the netlist combinationally.]
 
-  Description [Uses CIs/COs collected in the internal arrays.]
+  Description [Checks for combinational loops. Collects PI/PO nets.
+  Collects nodes in the topological order.]
                
   SideEffects []
 
   SeeAlso     []
 
 ***********************************************************************/
-Aig_Man_t * Ntl_ManCollapseForSec( Ntl_Man_t * p1, Ntl_Man_t * p2 )
+Aig_Man_t * Ntl_ManCollapseSeq( Ntl_Man_t * p )
 {
-    Aig_Man_t * pAig;
-    Aig_Obj_t * pMiter;
-    Ntl_Mod_t * pRoot1, * pRoot2;
+    Ntl_Mod_t * pRoot;
     Ntl_Obj_t * pObj;
     Ntl_Net_t * pNet;
-    Vec_Ptr_t * vPairs;
-    int i;
-    assert( Vec_PtrSize(p1->vCis) > 0 );
-    assert( Vec_PtrSize(p1->vCos) > 0 );
-    assert( Vec_PtrSize(p1->vCis) == Vec_PtrSize(p2->vCis) );
-    assert( Vec_PtrSize(p1->vCos) == Vec_PtrSize(p2->vCos) );
-
-    // create the manager
-    pAig = p1->pAig = p2->pAig = Aig_ManStart( 10000 );
-    pAig->pName = Aig_UtilStrsav( p1->pName );
-    pAig->pSpec = Aig_UtilStrsav( p1->pSpec );
-    vPairs = Vec_PtrStart( 2 * Vec_PtrSize(p1->vCos) );
-    // placehoder output to be used later for the miter output
-    Aig_ObjCreatePo( pAig, Aig_ManConst1(pAig) );
-
-    /////////////////////////////////////////////////////
-    // clear net visited flags
-    pRoot1 = Ntl_ManRootModel(p1);
-    Ntl_ModelForEachNet( pRoot1, pNet, i )
-    {
-        pNet->nVisits = 0;
-        pNet->pCopy = NULL;
-    }
-    // primary inputs
-    Ntl_ManForEachCiNet( p1, pObj, i )
-    {
-        assert( Ntl_ObjFanoutNum(pObj) == 1 );
-        pNet = Ntl_ObjFanout0(pObj);
-        pNet->pCopy = Aig_ObjCreatePi( pAig );
-        if ( pNet->nVisits )
-        {
-            printf( "Ntl_ManCollapseForSec(): Primary input appears twice in the list.\n" );
-            return 0;
-        }
-        pNet->nVisits = 2;
-    }
-    // latch outputs
-    Ntl_ModelForEachLatch( pRoot1, pObj, i )
-    {
-        assert( Ntl_ObjFanoutNum(pObj) == 1 );
-        pNet = Ntl_ObjFanout0(pObj);
-        pNet->pCopy = Aig_ObjCreatePi( pAig );
-        if ( (pObj->LatchId & 3) == 1 )
-            pNet->pCopy = Aig_Not(pNet->pCopy);
-        if ( pNet->nVisits )
-        {
-            printf( "Ntl_ManCollapseForSec(): Latch output is duplicated or defined as a primary input.\n" );
-            return 0;
-        }
-        pNet->nVisits = 2;
-    }
-    // derive the outputs
-    Ntl_ManForEachCoNet( p1, pObj, i )
-    {
-        pNet = Ntl_ObjFanin0(pObj);
-        if ( !Ntl_ManCollapse_rec( p1, pNet ) )
-        {
-            printf( "Ntl_ManCollapseForSec(): Error: Combinational loop is detected.\n" );
-            return 0;
-        }
-//        Aig_ObjCreatePo( pAig, pNet->pCopy );
-        Vec_PtrWriteEntry( vPairs, 2 * i, pNet->pCopy );
-    }
-    // visit the nodes starting from latch inputs outputs
-    Ntl_ModelForEachLatch( pRoot1, pObj, i )
-    {
-        pNet = Ntl_ObjFanin0(pObj);
-        if ( !Ntl_ManCollapse_rec( p1, pNet ) )
-        {
-            printf( "Ntl_ManCollapseForSec(): Error: Combinational loop is detected.\n" );
-            return 0;
-        }
-        if ( (pObj->LatchId & 3) == 1 )
-            Aig_ObjCreatePo( pAig, Aig_Not(pNet->pCopy) );
-        else
-            Aig_ObjCreatePo( pAig, pNet->pCopy );
-    }
-
-    /////////////////////////////////////////////////////
-    // clear net visited flags
-    pRoot2 = Ntl_ManRootModel(p2);
-    Ntl_ModelForEachNet( pRoot2, pNet, i )
-    {
-        pNet->nVisits = 0;
-        pNet->pCopy = NULL;
-    }
-    // primary inputs
-    Ntl_ManForEachCiNet( p2, pObj, i )
-    {
-        assert( Ntl_ObjFanoutNum(pObj) == 1 );
-        pNet = Ntl_ObjFanout0(pObj);
-        pNet->pCopy = Aig_ManPi( pAig, i );
-        if ( pNet->nVisits )
-        {
-            printf( "Ntl_ManCollapseForSec(): Primary input appears twice in the list.\n" );
-            return 0;
-        }
-        pNet->nVisits = 2;
-    }
-    // latch outputs
-    Ntl_ModelForEachLatch( pRoot2, pObj, i )
-    {
-        assert( Ntl_ObjFanoutNum(pObj) == 1 );
-        pNet = Ntl_ObjFanout0(pObj);
-        pNet->pCopy = Aig_ObjCreatePi( pAig );
-        if ( (pObj->LatchId & 3) == 1 )
-            pNet->pCopy = Aig_Not(pNet->pCopy);
-        if ( pNet->nVisits )
-        {
-            printf( "Ntl_ManCollapseForSec(): Latch output is duplicated or defined as a primary input.\n" );
-            return 0;
-        }
-        pNet->nVisits = 2;
-    }
-    // derive the outputs
-    Ntl_ManForEachCoNet( p2, pObj, i )
-    {
-        pNet = Ntl_ObjFanin0(pObj);
-        if ( !Ntl_ManCollapse_rec( p2, pNet ) )
-        {
-            printf( "Ntl_ManCollapseForSec(): Error: Combinational loop is detected.\n" );
-            return 0;
-        }
-//        Aig_ObjCreatePo( pAig, pNet->pCopy );
-        Vec_PtrWriteEntry( vPairs, 2 * i + 1, pNet->pCopy );
-    }
-    // visit the nodes starting from latch inputs outputs
-    Ntl_ModelForEachLatch( pRoot2, pObj, i )
-    {
-        pNet = Ntl_ObjFanin0(pObj);
-        if ( !Ntl_ManCollapse_rec( p2, pNet ) )
-        {
-            printf( "Ntl_ManCollapseForSec(): Error: Combinational loop is detected.\n" );
-            return 0;
-        }
-        if ( (pObj->LatchId & 3) == 1 )
-            Aig_ObjCreatePo( pAig, Aig_Not(pNet->pCopy) );
-        else
-            Aig_ObjCreatePo( pAig, pNet->pCopy );
-    }
-
-    /////////////////////////////////////////////////////
-    pMiter = Aig_Miter(pAig, vPairs);
-    Vec_PtrFree( vPairs );
-    Aig_ObjPatchFanin0( pAig, Aig_ManPo(pAig,0), pMiter  );
-    Aig_ManSetRegNum( pAig, Ntl_ModelLatchNum( pRoot1 ) + Ntl_ModelLatchNum( pRoot2 ) );
-    Aig_ManCleanup( pAig );
-    return pAig;    
+    int i, k;
+    Vec_PtrClear( p->vCis );
+    Vec_PtrClear( p->vCos );
+    Vec_PtrClear( p->vLatchIns );
+    // prepare the model
+    pRoot = Ntl_ManRootModel(p);
+    // collect the leaves for this traversal
+    Ntl_ModelForEachSeqLeaf( pRoot, pObj, i )
+        Ntl_ObjForEachFanout( pObj, pNet, k )
+            Vec_PtrPush( p->vCis, pNet );
+    // collect the roots for this traversal
+    Ntl_ModelForEachSeqRoot( pRoot, pObj, i )
+        Ntl_ObjForEachFanin( pObj, pNet, k )
+            Vec_PtrPush( p->vCos, pNet );
+    // perform the traversal
+    return Ntl_ManCollapse( p, 1 );
 }
 
 
+
 /**Function*************************************************************
 
   Synopsis    [Increments reference counter of the net.]
@@ -806,11 +627,7 @@ Nwk_Man_t * Ntl_ManExtractNwk( Ntl_Man_t * p, Aig_Man_t * pAig, Tim_Man_t * pMan
     vCover = Vec_IntAlloc( 100 );
     vMemory = Vec_IntAlloc( 1 << 16 );
     // count the number of fanouts of each net
-    Ntl_ModelForEachNet( pRoot, pNet, i )
-    {
-        pNet->pCopy = NULL;
-        pNet->fMark = 0;
-    }
+    Ntl_ModelClearNets( pRoot );
     Ntl_ModelForEachObj( pRoot, pObj, i )
         Ntl_ObjForEachFanin( pObj, pNet, k )
             Ntl_NetIncrementRefs( pNet );
@@ -867,11 +684,7 @@ Nwk_Man_t * Ntl_ManExtractNwk( Ntl_Man_t * p, Aig_Man_t * pAig, Tim_Man_t * pMan
         }
     }
 //    Aig_ManCleanPioNumbers( pAig );
-    Ntl_ModelForEachNet( pRoot, pNet, i )
-    {
-        pNet->pCopy = NULL;
-        pNet->fMark = 0;
-    }
+    Ntl_ModelClearNets( pRoot );
     Vec_IntFree( vCover );
     Vec_IntFree( vMemory );
     // create timing manager from the current design
diff --git a/src/aig/ntl/ntlFraig.c b/src/aig/ntl/ntlFraig.c
index 6de41679..cdc1323b 100644
--- a/src/aig/ntl/ntlFraig.c
+++ b/src/aig/ntl/ntlFraig.c
@@ -203,7 +203,7 @@ void Ntl_ManResetComplemented( Ntl_Man_t * p, Aig_Man_t * pAigCol )
     pRoot = Ntl_ManRootModel(p);
     Ntl_ModelForEachLatch( pRoot, pObj, i )
     {
-        if ( (pObj->LatchId & 3) == 1 )
+        if ( Ntl_ObjIsInit1( pObj ) )
         {
             pObjCol = Ntl_ObjFanout0(pObj)->pCopy;
             assert( pObjCol->fPhase == 0 );
@@ -275,7 +275,7 @@ Ntl_Man_t * Ntl_ManFraig( Ntl_Man_t * p, int nPartSize, int nConfLimit, int nLev
     // collapse the AIG
     pAig = Ntl_ManExtract( p );
     pNew = Ntl_ManInsertAig( p, pAig );
-    pAigCol = Ntl_ManCollapse( pNew, 0 );
+    pAigCol = Ntl_ManCollapseComb( pNew );
 
     // perform fraiging for the given design
     nPartSize = nPartSize? nPartSize : Aig_ManPoNum(pAigCol);
@@ -309,7 +309,7 @@ Ntl_Man_t * Ntl_ManScl( Ntl_Man_t * p, int fLatchConst, int fLatchEqual, int fVe
     // collapse the AIG
     pAig = Ntl_ManExtract( p );
     pNew = Ntl_ManInsertAig( p, pAig );
-    pAigCol = Ntl_ManCollapse( pNew, 1 );
+    pAigCol = Ntl_ManCollapseSeq( pNew );
 
     // perform SCL for the given design
     Aig_ManSetRegNum( pAigCol, Ntl_ModelLatchNum(Ntl_ManRootModel(p)) );
@@ -343,7 +343,7 @@ Ntl_Man_t * Ntl_ManLcorr( Ntl_Man_t * p, int nConfMax, int fVerbose )
     // collapse the AIG
     pAig = Ntl_ManExtract( p );
     pNew = Ntl_ManInsertAig( p, pAig );
-    pAigCol = Ntl_ManCollapse( pNew, 1 );
+    pAigCol = Ntl_ManCollapseSeq( pNew );
 
     // perform SCL for the given design
     Aig_ManSetRegNum( pAigCol, Ntl_ModelLatchNum(Ntl_ManRootModel(p)) );
@@ -377,7 +377,7 @@ Ntl_Man_t * Ntl_ManSsw( Ntl_Man_t * p, Fra_Ssw_t * pPars )
     // collapse the AIG
     pAig = Ntl_ManExtract( p );
     pNew = Ntl_ManInsertAig( p, pAig );
-    pAigCol = Ntl_ManCollapse( pNew, 1 );
+    pAigCol = Ntl_ManCollapseSeq( pNew );
 
     // perform SCL for the given design
     Aig_ManSetRegNum( pAigCol, Ntl_ModelLatchNum(Ntl_ManRootModel(p)) );
@@ -502,7 +502,7 @@ void Ntl_ManFlipEdges( Ntl_Man_t * p, Aig_Man_t * pAigCol )
     iLatch = 0;
     Ntl_ModelForEachLatch( pRoot, pObj, i )
     {
-        if ( (pObj->LatchId & 3) == 1 )
+        if ( Ntl_ObjIsInit1( pObj ) )
         {
             pObjCol = Aig_ManPi( pAigCol, Ntl_ModelPiNum(pRoot) + iLatch );
             assert( pObjCol->fMarkA == 0 );
@@ -524,7 +524,7 @@ void Ntl_ManFlipEdges( Ntl_Man_t * p, Aig_Man_t * pAigCol )
     iLatch = 0;
     Ntl_ModelForEachLatch( pRoot, pObj, i )
     {
-        if ( (pObj->LatchId & 3) == 1 )
+        if ( Ntl_ObjIsInit1( pObj ) )
         {
             // flip the latch input
             pObjCol = Aig_ManPo( pAigCol, Ntl_ModelPoNum(pRoot) + iLatch );
@@ -554,7 +554,7 @@ Ntl_Man_t * Ntl_ManSsw2( Ntl_Man_t * p, Fra_Ssw_t * pPars )
     Ntl_Man_t * pNew;
     Aig_Man_t * pAigRed, * pAigCol;
     // collapse the AIG
-    pAigCol = Ntl_ManCollapse( p, 1 );
+    pAigCol = Ntl_ManCollapseSeq( p );
     Aig_ManSetRegNum( pAigCol, Ntl_ModelLatchNum(Ntl_ManRootModel(p)) );
     // transform the collapsed AIG
     pAigRed = Fra_FraigInduction( pAigCol, pPars );
diff --git a/src/aig/ntl/ntlInsert.c b/src/aig/ntl/ntlInsert.c
index 3cd9470b..9675eb28 100644
--- a/src/aig/ntl/ntlInsert.c
+++ b/src/aig/ntl/ntlInsert.c
@@ -257,7 +257,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[100]; 
     Vec_Ptr_t * vObjs;
     Vec_Int_t * vTruth;
     Vec_Int_t * vCover;
diff --git a/src/aig/ntl/ntlMan.c b/src/aig/ntl/ntlMan.c
index e80e02c6..0083e04c 100644
--- a/src/aig/ntl/ntlMan.c
+++ b/src/aig/ntl/ntlMan.c
@@ -50,9 +50,14 @@ Ntl_Man_t * Ntl_ManAlloc()
     p->vCos = Vec_PtrAlloc( 1000 );
     p->vNodes = Vec_PtrAlloc( 1000 );
     p->vBox1Cos = Vec_IntAlloc( 1000 );
+    p->vLatchIns = Vec_PtrAlloc( 1000 );
     // start the manager
     p->pMemObjs = Aig_MmFlexStart();
     p->pMemSops = Aig_MmFlexStart();
+    // allocate model table
+    p->nModTableSize = Aig_PrimeCudd( 100 );
+    p->pModTable = ALLOC( Ntl_Mod_t *, p->nModTableSize );
+    memset( p->pModTable, 0, sizeof(Ntl_Mod_t *) * p->nModTableSize );
     return p;
 }
 
@@ -185,14 +190,16 @@ void Ntl_ManFree( Ntl_Man_t * p )
             Ntl_ModelFree( pModel );
         Vec_PtrFree( p->vModels );
     }
-    if ( p->vCis )     Vec_PtrFree( p->vCis );
-    if ( p->vCos )     Vec_PtrFree( p->vCos );
-    if ( p->vNodes )   Vec_PtrFree( p->vNodes );
-    if ( p->vBox1Cos ) Vec_IntFree( p->vBox1Cos );
-    if ( p->pMemObjs ) Aig_MmFlexStop( p->pMemObjs, 0 );
-    if ( p->pMemSops ) Aig_MmFlexStop( p->pMemSops, 0 );
-    if ( p->pAig )     Aig_ManStop( p->pAig );
-    if ( p->pManTime ) Tim_ManStop( p->pManTime );
+    if ( p->vCis )      Vec_PtrFree( p->vCis );
+    if ( p->vCos )      Vec_PtrFree( p->vCos );
+    if ( p->vNodes )    Vec_PtrFree( p->vNodes );
+    if ( p->vBox1Cos )  Vec_IntFree( p->vBox1Cos );
+    if ( p->vLatchIns ) Vec_PtrFree( p->vLatchIns );
+    if ( p->pMemObjs )  Aig_MmFlexStop( p->pMemObjs, 0 );
+    if ( p->pMemSops )  Aig_MmFlexStop( p->pMemSops, 0 );
+    if ( p->pAig )      Aig_ManStop( p->pAig );
+    if ( p->pManTime )  Tim_ManStop( p->pManTime );
+    FREE( p->pModTable );
     free( p );
 }
 
@@ -239,7 +246,7 @@ int Ntl_ManLatchNum( Ntl_Man_t * p )
   SeeAlso     []
 
 ***********************************************************************/
-Ntl_Mod_t * Ntl_ManFindModel( Ntl_Man_t * p, char * pName )
+Ntl_Mod_t * Ntl_ManFindModel_old( Ntl_Man_t * p, char * pName )
 {
     Ntl_Mod_t * pModel;
     int i;
@@ -276,6 +283,8 @@ void Ntl_ManPrintStats( Ntl_Man_t * p )
     printf( "\n" );
     fflush( stdout );
     assert( Ntl_ModelLut1Num(pRoot) == Ntl_ModelCountLut1(pRoot) );
+    Ntl_ManPrintTypes( p );
+    fflush( stdout );
 }
 
 /**Function*************************************************************
@@ -296,6 +305,67 @@ Tim_Man_t * Ntl_ManReadTimeMan( Ntl_Man_t * p )
 
 /**Function*************************************************************
 
+  Synopsis    [Saves the model type.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Ntl_ManSaveBoxType( Ntl_Obj_t * pObj )
+{
+    Ntl_Mod_t * pModel = pObj->pImplem;
+    int Number = 0;
+    assert( Ntl_ObjIsBox(pObj) );
+    Number |= (pModel->attrWhite << 0);
+    Number |= (pModel->attrBox   << 1);
+    Number |= (pModel->attrComb  << 2);
+    Number |= (pModel->attrKeep  << 3);
+    pModel->pMan->BoxTypes[Number]++;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Saves the model type.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Ntl_ManPrintTypes( Ntl_Man_t * p )
+{
+    Ntl_Mod_t * pModel;
+    Ntl_Obj_t * pObj;
+    int i;
+    pModel = Ntl_ManRootModel( p );
+    if ( Ntl_ModelBoxNum(pModel) == 0 )
+        return;
+    printf( "BOX STATISTICS:\n" );
+    Ntl_ModelForEachBox( pModel, pObj, i )
+        Ntl_ManSaveBoxType( pObj );
+    for ( i = 0; i < 15; i++ )
+    {
+        if ( !p->BoxTypes[i] )
+            continue;
+        printf( "%5d :", p->BoxTypes[i] );
+        printf( " %s", ((i & 1) > 0)? "white": "black" );
+        printf( " %s", ((i & 2) > 0)? "box  ": "logic" );
+        printf( " %s", ((i & 4) > 0)? "comb ": "seq  " );
+        printf( " %s", ((i & 8) > 0)? "keep ": "sweep" );
+        printf( "\n" );
+    }
+    printf( "Total box instances = %6d.\n\n", Ntl_ModelBoxNum(pModel) );
+    for ( i = 0; i < 15; i++ )
+        p->BoxTypes[i] = 0;
+}
+
+/**Function*************************************************************
+
   Synopsis    [Allocates the model.]
 
   Description []
@@ -311,16 +381,25 @@ Ntl_Mod_t * Ntl_ModelAlloc( Ntl_Man_t * pMan, char * pName )
     // start the manager
     p = ALLOC( Ntl_Mod_t, 1 );
     memset( p, 0, sizeof(Ntl_Mod_t) );
+    p->attrBox   = 1;
+    p->attrComb  = 1;
+    p->attrWhite = 1;
+    p->attrKeep  = 0;
     p->pMan  = pMan;
     p->pName = Ntl_ManStoreName( p->pMan, pName );
-    Vec_PtrPush( pMan->vModels, p );
-    p->vObjs = Vec_PtrAlloc( 1000 );
-    p->vPis  = Vec_PtrAlloc( 100 );
-    p->vPos  = Vec_PtrAlloc( 100 );
+    p->vObjs = Vec_PtrAlloc( 100 );
+    p->vPis  = Vec_PtrAlloc( 10 );
+    p->vPos  = Vec_PtrAlloc( 10 ); 
     // start the table
-    p->nTableSize = Aig_PrimeCudd( 1000 );
+    p->nTableSize = Aig_PrimeCudd( 100 );
     p->pTable = ALLOC( Ntl_Net_t *, p->nTableSize );
     memset( p->pTable, 0, sizeof(Ntl_Net_t *) * p->nTableSize );
+    // add model to the table
+    if ( !Ntl_ManAddModel( pMan, p ) )
+    {
+        Ntl_ModelFree( p );
+        return NULL;
+    }
     return p;
 }
 
@@ -371,11 +450,14 @@ Ntl_Mod_t * Ntl_ModelStartFrom( Ntl_Man_t * pManNew, Ntl_Mod_t * pModelOld )
             if ( pNet->pCopy != NULL )
                 Ntl_ObjSetFanout( pObj->pCopy, pNet->pCopy, k );
         if ( Ntl_ObjIsLatch(pObj) )
+        {
             ((Ntl_Obj_t *)pObj->pCopy)->LatchId = pObj->LatchId;
+            ((Ntl_Obj_t *)pObj->pCopy)->pClock = pObj->pClock->pCopy;
+        }
     }
     pModelNew->vDelays = pModelOld->vDelays? Vec_IntDup( pModelOld->vDelays ) : NULL;
-    pModelNew->vArrivals = pModelOld->vArrivals? Vec_IntDup( pModelOld->vArrivals ) : NULL;
-    pModelNew->vRequireds = pModelOld->vRequireds? Vec_IntDup( pModelOld->vRequireds ) : NULL;
+    pModelNew->vTimeInputs = pModelOld->vTimeInputs? Vec_IntDup( pModelOld->vTimeInputs ) : NULL;
+    pModelNew->vTimeOutputs = pModelOld->vTimeOutputs? Vec_IntDup( pModelOld->vTimeOutputs ) : NULL;
     return pModelNew;
 }
 
@@ -397,11 +479,20 @@ Ntl_Mod_t * Ntl_ModelDup( Ntl_Man_t * pManNew, Ntl_Mod_t * pModelOld )
     Ntl_Obj_t * pObj;
     int i, k;
     pModelNew = Ntl_ModelAlloc( pManNew, pModelOld->pName );
+    pModelNew->attrWhite = pModelOld->attrWhite;
+    pModelNew->attrBox     = pModelOld->attrBox;
+    pModelNew->attrComb     = pModelOld->attrComb;
+    pModelNew->attrKeep     = pModelOld->attrKeep;
     Ntl_ModelForEachObj( pModelOld, pObj, i )
         pObj->pCopy = Ntl_ModelDupObj( pModelNew, pObj );
     Ntl_ModelForEachNet( pModelOld, pNet, i )
     {
         pNet->pCopy = Ntl_ModelFindOrCreateNet( pModelNew, pNet->pName );
+        if ( pNet->pDriver == NULL )
+        {
+            assert( !pModelOld->attrWhite );
+            continue;
+        }
         ((Ntl_Net_t *)pNet->pCopy)->pDriver = pNet->pDriver->pCopy;
         assert( pNet->pDriver->pCopy != NULL );
     }
@@ -412,13 +503,16 @@ Ntl_Mod_t * Ntl_ModelDup( Ntl_Man_t * pManNew, Ntl_Mod_t * pModelOld )
         Ntl_ObjForEachFanout( pObj, pNet, k )
             Ntl_ObjSetFanout( pObj->pCopy, pNet->pCopy, k );
         if ( Ntl_ObjIsLatch(pObj) )
+        {
             ((Ntl_Obj_t *)pObj->pCopy)->LatchId = pObj->LatchId;
+            ((Ntl_Obj_t *)pObj->pCopy)->pClock = pObj->pClock->pCopy;
+        }
         if ( Ntl_ObjIsNode(pObj) )
             ((Ntl_Obj_t *)pObj->pCopy)->pSop = Ntl_ManStoreSop( pManNew->pMemSops, pObj->pSop );
     }
     pModelNew->vDelays = pModelOld->vDelays? Vec_IntDup( pModelOld->vDelays ) : NULL;
-    pModelNew->vArrivals = pModelOld->vArrivals? Vec_IntDup( pModelOld->vArrivals ) : NULL;
-    pModelNew->vRequireds = pModelOld->vRequireds? Vec_IntDup( pModelOld->vRequireds ) : NULL;
+    pModelNew->vTimeInputs = pModelOld->vTimeInputs? Vec_IntDup( pModelOld->vTimeInputs ) : NULL;
+    pModelNew->vTimeOutputs = pModelOld->vTimeOutputs? Vec_IntDup( pModelOld->vTimeOutputs ) : NULL;
     return pModelNew;
 }
 
@@ -435,10 +529,10 @@ Ntl_Mod_t * Ntl_ModelDup( Ntl_Man_t * pManNew, Ntl_Mod_t * pModelOld )
 ***********************************************************************/
 void Ntl_ModelFree( Ntl_Mod_t * p )
 {
-    assert( Ntl_ManCheckNetsAreNotMarked(p) );
-    if ( p->vRequireds )  Vec_IntFree( p->vRequireds );
-    if ( p->vArrivals )   Vec_IntFree( p->vArrivals );
-    if ( p->vDelays )     Vec_IntFree( p->vDelays );
+    assert( Ntl_ModelCheckNetsAreNotMarked(p) );
+    if ( p->vTimeOutputs )  Vec_IntFree( p->vTimeOutputs );
+    if ( p->vTimeInputs )   Vec_IntFree( p->vTimeInputs );
+    if ( p->vDelays )       Vec_IntFree( p->vDelays );
     Vec_PtrFree( p->vObjs );
     Vec_PtrFree( p->vPis );
     Vec_PtrFree( p->vPos );
@@ -446,6 +540,45 @@ void Ntl_ModelFree( Ntl_Mod_t * p )
     free( p );
 }
 
+/**Function*************************************************************
+
+  Synopsis    [Create model equal to the latch with the given init value.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Ntl_Mod_t * Ntl_ManCreateLatchModel( Ntl_Man_t * pMan, int Init )
+{
+    char Name[100];
+    Ntl_Mod_t * pModel;
+    Ntl_Obj_t * pObj;
+    Ntl_Net_t * pNetLi, * pNetLo;
+    // create model
+    sprintf( Name, "%s%d", "latch", Init );
+    pModel = Ntl_ModelAlloc( pMan, Name );
+    pModel->attrWhite = 1;
+    pModel->attrBox   = 1;
+    pModel->attrComb  = 0;
+    pModel->attrKeep  = 0;
+    // create primary input
+    pObj = Ntl_ModelCreatePi( pModel );
+    pNetLi = Ntl_ModelFindOrCreateNet( pModel, "li" );
+    Ntl_ModelSetNetDriver( pObj, pNetLi );
+    // create latch 
+    pObj = Ntl_ModelCreateLatch( pModel );
+    pObj->LatchId.regInit = Init;
+    pObj->pFanio[0] = pNetLi;
+    // create primary output
+    pNetLo = Ntl_ModelFindOrCreateNet( pModel, "lo" );
+    Ntl_ModelSetNetDriver( pObj, pNetLo );
+    pObj = Ntl_ModelCreatePo( pModel, pNetLo );
+    return pModel;
+}
+
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/aig/ntl/ntlReadBlif.c b/src/aig/ntl/ntlReadBlif.c
index a291f8a0..ebfb2a80 100644
--- a/src/aig/ntl/ntlReadBlif.c
+++ b/src/aig/ntl/ntlReadBlif.c
@@ -38,8 +38,8 @@ struct Ioa_ReadMod_t_
     Vec_Ptr_t *          vNames;       // .names lines
     Vec_Ptr_t *          vSubckts;     // .subckt lines
     Vec_Ptr_t *          vDelays;      // .delay lines
-    Vec_Ptr_t *          vArrivals;    // .input_arrival lines
-    Vec_Ptr_t *          vRequireds;   // .output_required lines
+    Vec_Ptr_t *          vTimeInputs;  // .input_arrival/required lines
+    Vec_Ptr_t *          vTimeOutputs; // .output_required/arrival lines
     int                  fBlackBox;    // indicates blackbox model
     // the resulting network
     Ntl_Mod_t *          pNtk;   
@@ -249,14 +249,14 @@ static Ioa_ReadMod_t * Ioa_ReadModAlloc()
     Ioa_ReadMod_t * p;
     p = ALLOC( Ioa_ReadMod_t, 1 );
     memset( p, 0, sizeof(Ioa_ReadMod_t) );
-    p->vInputs  = Vec_PtrAlloc( 512 );
-    p->vOutputs = Vec_PtrAlloc( 512 );
-    p->vLatches = Vec_PtrAlloc( 512 );
-    p->vNames   = Vec_PtrAlloc( 512 );
-    p->vSubckts = Vec_PtrAlloc( 512 );
-    p->vDelays  = Vec_PtrAlloc( 512 );
-    p->vArrivals  = Vec_PtrAlloc( 512 );
-    p->vRequireds = Vec_PtrAlloc( 512 );
+    p->vInputs  = Vec_PtrAlloc( 8 );
+    p->vOutputs = Vec_PtrAlloc( 8 );
+    p->vLatches = Vec_PtrAlloc( 8 );
+    p->vNames   = Vec_PtrAlloc( 8 );
+    p->vSubckts = Vec_PtrAlloc( 8 );
+    p->vDelays  = Vec_PtrAlloc( 8 );
+    p->vTimeInputs  = Vec_PtrAlloc( 8 );
+    p->vTimeOutputs = Vec_PtrAlloc( 8 );
     return p;
 }
 
@@ -279,8 +279,8 @@ static void Ioa_ReadModFree( Ioa_ReadMod_t * p )
     Vec_PtrFree( p->vNames );
     Vec_PtrFree( p->vSubckts );
     Vec_PtrFree( p->vDelays );
-    Vec_PtrFree( p->vArrivals );
-    Vec_PtrFree( p->vRequireds );
+    Vec_PtrFree( p->vTimeInputs );
+    Vec_PtrFree( p->vTimeOutputs );
     free( p );
 }
 
@@ -509,10 +509,12 @@ static void Ioa_ReadReadPreparse( Ioa_ReadMan_t * p )
             Vec_PtrPush( p->pLatest->vSubckts, pCur );
         else if ( !strncmp(pCur, "delay", 5) )
             Vec_PtrPush( p->pLatest->vDelays, pCur );
-        else if ( !strncmp(pCur, "input_arrival", 13) )
-            Vec_PtrPush( p->pLatest->vArrivals, pCur );
-        else if ( !strncmp(pCur, "output_required", 15) )
-            Vec_PtrPush( p->pLatest->vRequireds, pCur );
+        else if ( !strncmp(pCur, "input_arrival", 13) ||
+                  !strncmp(pCur, "input_required", 14) )
+            Vec_PtrPush( p->pLatest->vTimeInputs, pCur );
+        else if ( !strncmp(pCur, "output_required", 14) ||
+                  !strncmp(pCur, "output_arrival", 13) )
+            Vec_PtrPush( p->pLatest->vTimeOutputs, pCur );
         else if ( !strncmp(pCur, "blackbox", 8) )
             p->pLatest->fBlackBox = 1;
         else if ( !strncmp(pCur, "model", 5) ) 
@@ -522,7 +524,12 @@ static void Ioa_ReadReadPreparse( Ioa_ReadMan_t * p )
             p->pLatest->pMan = p;
         }
         else if ( !strncmp(pCur, "attrib", 6) ) 
-            p->pLatest->pAttrib = pCur;
+        {
+            if ( p->pLatest->pAttrib != NULL )
+                fprintf( stdout, "Line %d: Skipping second .attrib line for this model.\n", Ioa_ReadGetLine(p, pCur) );
+            else
+                p->pLatest->pAttrib = pCur;
+        }
         else if ( !strncmp(pCur, "end", 3) )
         {
             if ( p->pLatest )
@@ -537,15 +544,6 @@ static void Ioa_ReadReadPreparse( Ioa_ReadMan_t * p )
         else if ( !strncmp(pCur, "no_merge", 8) ) 
         {
         }
-        else if ( !strncmp(pCur, "attribute", 9) ) 
-        {
-        }
-        else if ( !strncmp(pCur, "input_required", 14) ) 
-        {
-        }
-        else if ( !strncmp(pCur, "output_arrival", 14) ) 
-        {
-        }
         else
         {
             pCur--;
@@ -593,10 +591,10 @@ static int Ioa_ReadReadInterfaces( Ioa_ReadMan_t * p )
         Vec_PtrForEachEntry( pMod->vDelays, pLine, k )
             if ( !Ioa_ReadParseLineDelay( pMod, pLine ) )
                 return 0;
-        Vec_PtrForEachEntry( pMod->vArrivals, pLine, k )
+        Vec_PtrForEachEntry( pMod->vTimeInputs, pLine, k )
             if ( !Ioa_ReadParseLineTimes( pMod, pLine, 0 ) )
                 return 0;
-        Vec_PtrForEachEntry( pMod->vRequireds, pLine, k )
+        Vec_PtrForEachEntry( pMod->vTimeOutputs, pLine, k )
             if ( !Ioa_ReadParseLineTimes( pMod, pLine, 1 ) )
                 return 0;
     }
@@ -643,6 +641,8 @@ static Ntl_Man_t * Ioa_ReadParse( Ioa_ReadMan_t * p )
         return NULL;
     // update the design name
     pMod = Vec_PtrEntry( p->vModels, 0 );
+    if ( Ntl_ModelLatchNum(pMod->pNtk) > 0 )
+        Ntl_ModelTransformLatches( pMod->pNtk );
     p->pDesign->pName = Ntl_ManStoreName( p->pDesign, pMod->pNtk->pName );
     // return the network
     pDesign = p->pDesign;
@@ -674,6 +674,11 @@ static int Ioa_ReadParseLineModel( Ioa_ReadMod_t * p, char * pLine )
         return 0;
     }
     p->pNtk = Ntl_ModelAlloc( p->pMan->pDesign, Vec_PtrEntry(vTokens, 1) );
+    if ( p->pNtk == NULL )
+    {
+        sprintf( p->pMan->sError, "Line %d: Model %s already exists.", Ioa_ReadGetLine(p->pMan, pToken), Vec_PtrEntry(vTokens, 1) );
+        return 0;
+    }
     return 1;
 }
 
@@ -692,23 +697,33 @@ static int Ioa_ReadParseLineAttrib( Ioa_ReadMod_t * p, char * pLine )
 {
     Vec_Ptr_t * vTokens = p->pMan->vTokens;
     char * pToken;
+    int i;
     Ioa_ReadSplitIntoTokens( vTokens, pLine, '\0' );
     pToken = Vec_PtrEntry( vTokens, 0 );
     assert( !strncmp(pToken, "attrib", 6) );
-/*
-    if ( Vec_PtrSize(vTokens) != 2 )
-    {
-        sprintf( p->pMan->sError, "Line %d: The number of entries (%d) in .attrib line is different from two.", Ioa_ReadGetLine(p->pMan, pToken), Vec_PtrSize(vTokens) );
-        return 0;
-    }
-    if ( strcmp( Vec_PtrEntry(vTokens, 1), "keep" ) == 0 )
-        p->pNtk->fKeep = 1;
-    else
+    Vec_PtrForEachEntryStart( vTokens, pToken, i, 1 )
     {
-        sprintf( p->pMan->sError, "Line %d: Unknown attribute (%s) in the .attrib line of model %s.", Ioa_ReadGetLine(p->pMan, pToken), Vec_PtrEntry(vTokens, 1), p->pNtk->pName );
-        return 0;
+        pToken = Vec_PtrEntry( vTokens, i );
+        if ( strcmp( pToken, "white" ) == 0 )
+            p->pNtk->attrWhite = 1;
+        else if ( strcmp( pToken, "black" ) == 0 )
+            p->pNtk->attrWhite = 0;
+        else if ( strcmp( pToken, "box" ) == 0 )
+            p->pNtk->attrBox = 1;
+        else if ( strcmp( pToken, "white" ) == 0 )
+            p->pNtk->attrWhite = 1;
+        else if ( strcmp( pToken, "comb" ) == 0 )
+            p->pNtk->attrComb = 1;
+        else if ( strcmp( pToken, "seq" ) == 0 )
+            p->pNtk->attrComb = 0;
+        else if ( strcmp( pToken, "keep" ) == 0 )
+            p->pNtk->attrKeep = 1;
+        else 
+        {
+            sprintf( p->pMan->sError, "Line %d: Unknown attribute (%s) in the .attrib line of model %s.", Ioa_ReadGetLine(p->pMan, pToken), pToken, p->pNtk->pName );
+            return 0;
+        }
     }
-*/
     return 1;
 }
 
@@ -792,7 +807,6 @@ static int Ioa_ReadParseLineLatch( Ioa_ReadMod_t * p, char * pLine )
     Ntl_Net_t * pNetLi, * pNetLo;
     Ntl_Obj_t * pObj;
     char * pToken, * pNameLi, * pNameLo;
-    int Init, Class;
     Ioa_ReadSplitIntoTokens( vTokens, pLine, '\0' );
     pToken = Vec_PtrEntry(vTokens,0);
     assert( !strcmp(pToken, "latch") );
@@ -815,31 +829,47 @@ static int Ioa_ReadParseLineLatch( Ioa_ReadMod_t * p, char * pLine )
     }
     // get initial value
     if ( Vec_PtrSize(vTokens) > 3 )
-        Init = atoi( Vec_PtrEntry(vTokens,Vec_PtrSize(vTokens)-1) );
+        pObj->LatchId.regInit = atoi( Vec_PtrEntry(vTokens,Vec_PtrSize(vTokens)-1) );
     else
-        Init = 2;
-    if ( Init < 0 || Init > 2 )
+        pObj->LatchId.regInit = 2;
+    if ( pObj->LatchId.regInit < 0 || pObj->LatchId.regInit > 2 )
     {
         sprintf( p->pMan->sError, "Line %d: Initial state of the latch is incorrect \"%s\".", Ioa_ReadGetLine(p->pMan, pToken), Vec_PtrEntry(vTokens,3) );
         return 0;
     }
     // get the register class
     if ( Vec_PtrSize(vTokens) == 6 )
-        Class = atoi( Vec_PtrEntry(vTokens,3) );
-    else
-        Class = 0;
-    if ( Class < 0 || Class > (1<<24) )
     {
-        sprintf( p->pMan->sError, "Line %d: Class of the latch is incorrect \"%s\".", Ioa_ReadGetLine(p->pMan, pToken), Vec_PtrEntry(vTokens,4) );
+        pToken = Vec_PtrEntry(vTokens,3);
+        if ( strcmp( pToken, "fe" ) == 0 )
+            pObj->LatchId.regType = 1;
+        else if ( strcmp( pToken, "re" ) == 0 )
+            pObj->LatchId.regType = 2;
+        else if ( strcmp( pToken, "ah" ) == 0 )
+            pObj->LatchId.regType = 3;
+        else if ( strcmp( pToken, "al" ) == 0 )
+            pObj->LatchId.regType = 4;
+        else if ( strcmp( pToken, "as" ) == 0 )
+            pObj->LatchId.regType = 5;
+        else if ( pToken[0] >= '0' && pToken[0] <= '9' )
+            pObj->LatchId.regClass = atoi(pToken);
+        else
+        {
+            sprintf( p->pMan->sError, "Line %d: Type/class of the latch is incorrect \"%s\".", Ioa_ReadGetLine(p->pMan, pToken), pToken );
+            return 0;
+        }
+    }
+    if ( pObj->LatchId.regClass < 0 || pObj->LatchId.regClass > (1<<24) )
+    {
+        sprintf( p->pMan->sError, "Line %d: Class of the latch is incorrect \"%s\".", Ioa_ReadGetLine(p->pMan, pToken), Vec_PtrEntry(vTokens,3) );
         return 0;
     }
-    pObj->LatchId = (Class << 2) | Init;
     // get the clock
     if ( Vec_PtrSize(vTokens) == 5 || Vec_PtrSize(vTokens) == 6 )
     {
         pToken = Vec_PtrEntry(vTokens,Vec_PtrSize(vTokens)-2);
         pNetLi = Ntl_ModelFindOrCreateNet( p->pNtk, pToken );
-//        pObj->pFanio[1] = pNetLi;
+        pObj->pClock = pNetLi;
     }
     return 1;
 }
@@ -984,7 +1014,7 @@ static int Ioa_ReadParseLineDelay( Ioa_ReadMod_t * p, char * pLine )
     RetValue1 = 0; Number1 = -1;
     if ( Vec_PtrSize(vTokens) > 2 )
     {
-        RetValue1 = Ntl_ModelFindPioNumber( p->pNtk, Vec_PtrEntry(vTokens, 1), &Number1 );
+        RetValue1 = Ntl_ModelFindPioNumber( p->pNtk, 0, 0, Vec_PtrEntry(vTokens, 1), &Number1 );
         if ( RetValue1 == 0 )
         {
             sprintf( p->pMan->sError, "Line %d: Cannot find signal \"%s\" among PIs/POs.", Ioa_ReadGetLine(p->pMan, pToken), Vec_PtrEntry(vTokens, 1) );
@@ -994,7 +1024,7 @@ static int Ioa_ReadParseLineDelay( Ioa_ReadMod_t * p, char * pLine )
     RetValue2 = 0; Number2 = -1;
     if ( Vec_PtrSize(vTokens) > 3 )
     {
-        RetValue2 = Ntl_ModelFindPioNumber( p->pNtk, Vec_PtrEntry(vTokens, 2), &Number2 );
+        RetValue2 = Ntl_ModelFindPioNumber( p->pNtk, 0, 0, Vec_PtrEntry(vTokens, 2), &Number2 );
         if ( RetValue2 == 0 )
         {
             sprintf( p->pMan->sError, "Line %d: Cannot find signal \"%s\" among PIs/POs.", Ioa_ReadGetLine(p->pMan, pToken), Vec_PtrEntry(vTokens, 2) );
@@ -1037,19 +1067,19 @@ static int Ioa_ReadParseLineDelay( Ioa_ReadMod_t * p, char * pLine )
 static int Ioa_ReadParseLineTimes( Ioa_ReadMod_t * p, char * pLine, int fOutput )
 {
     Vec_Ptr_t * vTokens = p->pMan->vTokens;
-    int RetValue, Number;
+    int RetValue, Number = -1;
     char * pToken, * pTokenNum;
     float Delay;
     assert( sizeof(float) == sizeof(int) );
     Ioa_ReadSplitIntoTokens( vTokens, pLine, '\0' );
     pToken = Vec_PtrEntry(vTokens,0);
     if ( fOutput )
-        assert( !strcmp(pToken, "output_required") );
+        assert( !strncmp(pToken, "output_", 7) );
     else
-        assert( !strcmp(pToken, "input_arrival") );
-    if ( Vec_PtrSize(vTokens) != 3 )
+        assert( !strncmp(pToken, "input_", 6) );
+    if ( Vec_PtrSize(vTokens) != 2 && Vec_PtrSize(vTokens) != 3 )
     {
-        sprintf( p->pMan->sError, "Line %d: Delay line does not have a valid number of parameters (3).", Ioa_ReadGetLine(p->pMan, pToken) );
+        sprintf( p->pMan->sError, "Line %d: Delay line does not have a valid number of parameters (2 or 3).", Ioa_ReadGetLine(p->pMan, pToken) );
         return 0;
     }
     // find the delay number
@@ -1068,31 +1098,37 @@ static int Ioa_ReadParseLineTimes( Ioa_ReadMod_t * p, char * pLine, int fOutput
     // find the PI/PO numbers
     if ( fOutput )
     {
-        RetValue = Ntl_ModelFindPioNumber( p->pNtk, Vec_PtrEntry(vTokens, 1), &Number );
-        if ( RetValue == 0 )
+        if ( Vec_PtrSize(vTokens) == 3 )
         {
-            sprintf( p->pMan->sError, "Line %d: Cannot find signal \"%s\" among POs.", Ioa_ReadGetLine(p->pMan, pToken), Vec_PtrEntry(vTokens, 1) );
-            return 0;
+            RetValue = Ntl_ModelFindPioNumber( p->pNtk, 0, 1, Vec_PtrEntry(vTokens, 1), &Number );
+            if ( RetValue == 0 )
+            {
+                sprintf( p->pMan->sError, "Line %d: Cannot find signal \"%s\" among POs.", Ioa_ReadGetLine(p->pMan, pToken), Vec_PtrEntry(vTokens, 1) );
+                return 0;
+            }
         }
         // store the values
-        if ( p->pNtk->vRequireds == NULL )
-            p->pNtk->vRequireds = Vec_IntAlloc( 100 );
-        Vec_IntPush( p->pNtk->vRequireds, Number );
-        Vec_IntPush( p->pNtk->vRequireds, Aig_Float2Int(Delay) );        
+        if ( p->pNtk->vTimeOutputs == NULL )
+            p->pNtk->vTimeOutputs = Vec_IntAlloc( 100 );
+        Vec_IntPush( p->pNtk->vTimeOutputs, Number );
+        Vec_IntPush( p->pNtk->vTimeOutputs, Aig_Float2Int(Delay) );        
     }
     else
     {
-        RetValue = Ntl_ModelFindPioNumber( p->pNtk, Vec_PtrEntry(vTokens, 1), &Number );
-        if ( RetValue == 0 )
+        if ( Vec_PtrSize(vTokens) == 3 )
         {
-            sprintf( p->pMan->sError, "Line %d: Cannot find signal \"%s\" among PIs.", Ioa_ReadGetLine(p->pMan, pToken), Vec_PtrEntry(vTokens, 1) );
-            return 0;
+            RetValue = Ntl_ModelFindPioNumber( p->pNtk, 1, 0, Vec_PtrEntry(vTokens, 1), &Number );
+            if ( RetValue == 0 )
+            {
+                sprintf( p->pMan->sError, "Line %d: Cannot find signal \"%s\" among PIs.", Ioa_ReadGetLine(p->pMan, pToken), Vec_PtrEntry(vTokens, 1) );
+                return 0;
+            }
         }
         // store the values
-        if ( p->pNtk->vArrivals == NULL )
-            p->pNtk->vArrivals = Vec_IntAlloc( 100 );
-        Vec_IntPush( p->pNtk->vArrivals, Number );
-        Vec_IntPush( p->pNtk->vArrivals, Aig_Float2Int(Delay) );        
+        if ( p->pNtk->vTimeInputs == NULL )
+            p->pNtk->vTimeInputs = Vec_IntAlloc( 100 );
+        Vec_IntPush( p->pNtk->vTimeInputs, Number );
+        Vec_IntPush( p->pNtk->vTimeInputs, Aig_Float2Int(Delay) );        
     }
     return 1;
 }
diff --git a/src/aig/ntl/ntlSweep.c b/src/aig/ntl/ntlSweep.c
index 8309e1b3..991d701a 100644
--- a/src/aig/ntl/ntlSweep.c
+++ b/src/aig/ntl/ntlSweep.c
@@ -79,7 +79,7 @@ void Ntl_ManSweepMark( Ntl_Man_t * p )
         Ntl_ManSweepMark_rec( p, pObj );
     // start from the persistant boxes
     Ntl_ModelForEachBox( pRoot, pObj, i )
-        if ( pObj->pImplem->fKeep )
+        if ( pObj->pImplem->attrKeep )
             Ntl_ManSweepMark_rec( p, pObj );
 }
 
diff --git a/src/aig/ntl/ntlTable.c b/src/aig/ntl/ntlTable.c
index c3acc0b1..fe58e2f8 100644
--- a/src/aig/ntl/ntlTable.c
+++ b/src/aig/ntl/ntlTable.c
@@ -189,7 +189,7 @@ Ntl_Net_t * Ntl_ModelFindOrCreateNet( Ntl_Mod_t * p, char * pName )
   SeeAlso     []
 
 ***********************************************************************/
-int Ntl_ModelFindPioNumber( Ntl_Mod_t * p, char * pName, int * pNumber )
+int Ntl_ModelFindPioNumber( Ntl_Mod_t * p, int fPiOnly, int fPoOnly, char * pName, int * pNumber )
 {
     Ntl_Net_t * pNet;
     Ntl_Obj_t * pObj;
@@ -198,6 +198,30 @@ int Ntl_ModelFindPioNumber( Ntl_Mod_t * p, char * pName, int * pNumber )
     pNet = Ntl_ModelFindNet( p, pName );
     if ( pNet == NULL )
         return 0;
+    if ( fPiOnly )
+    {
+        Ntl_ModelForEachPi( p, pObj, i )
+        {
+            if ( Ntl_ObjFanout0(pObj) == pNet )
+            {
+                *pNumber = i;
+                return -1;
+            }
+        }
+        return 0;
+    }
+    if ( fPoOnly )
+    {
+        Ntl_ModelForEachPo( p, pObj, i )
+        {
+            if ( Ntl_ObjFanin0(pObj) == pNet )
+            {
+                *pNumber = i;
+                return 1;
+            }
+        }
+        return 0;
+    }
     Ntl_ModelForEachPo( p, pObj, i )
     {
         if ( Ntl_ObjFanin0(pObj) == pNet )
@@ -281,6 +305,97 @@ int Ntl_ModelCountNets( Ntl_Mod_t * p )
     return Counter;
 }
 
+
+
+
+/**Function*************************************************************
+
+  Synopsis    [Resizes the table.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Ntl_ManModelTableResize( Ntl_Man_t * p )
+{
+    Ntl_Mod_t ** pModTableNew, ** ppSpot, * pEntry, * pEntry2;
+    int nModTableSizeNew, Counter, e, clk;
+clk = clock();
+    // get the new table size
+    nModTableSizeNew = Aig_PrimeCudd( 3 * p->nModTableSize ); 
+    // allocate a new array
+    pModTableNew = ALLOC( Ntl_Mod_t *, nModTableSizeNew );
+    memset( pModTableNew, 0, sizeof(Ntl_Mod_t *) * nModTableSizeNew );
+    // rehash entries 
+    Counter = 0;
+    for ( e = 0; e < p->nModTableSize; e++ )
+        for ( pEntry = p->pModTable[e], pEntry2 = pEntry? pEntry->pNext : NULL; 
+              pEntry; pEntry = pEntry2, pEntry2 = pEntry? pEntry->pNext : NULL )
+            {
+                ppSpot = pModTableNew + Ntl_HashString( pEntry->pName, nModTableSizeNew );
+                pEntry->pNext = *ppSpot;
+                *ppSpot = pEntry;
+                Counter++;
+            }
+    assert( Counter == p->nModEntries );
+//    printf( "Increasing the structural table size from %6d to %6d. ", p->nTableSize, nTableSizeNew );
+//    PRT( "Time", clock() - clk );
+    // replace the table and the parameters
+    free( p->pModTable );
+    p->pModTable = pModTableNew;
+    p->nModTableSize = nModTableSizeNew;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Finds or creates the net.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Ntl_ManAddModel( Ntl_Man_t * p, Ntl_Mod_t * pModel )
+{
+    Ntl_Mod_t * pEnt;
+    unsigned Key = Ntl_HashString( pModel->pName, p->nModTableSize );
+    for ( pEnt = p->pModTable[Key]; pEnt; pEnt = pEnt->pNext )
+        if ( !strcmp( pEnt->pName, pModel->pName ) )
+            return 0;
+    pModel->pNext = p->pModTable[Key];
+    p->pModTable[Key] = pModel;
+    if ( ++p->nModEntries > 2 * p->nModTableSize )
+        Ntl_ManModelTableResize( p );
+    Vec_PtrPush( p->vModels, pModel );
+    return 1;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Finds or creates the net.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Ntl_Mod_t * Ntl_ManFindModel( Ntl_Man_t * p, char * pName )
+{
+    Ntl_Mod_t * pEnt;
+    unsigned Key = Ntl_HashString( pName, p->nModTableSize );
+    for ( pEnt = p->pModTable[Key]; pEnt; pEnt = pEnt->pNext )
+        if ( !strcmp( pEnt->pName, pName ) )
+            return pEnt;
+    return NULL;
+}
+
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/aig/ntl/ntlTime.c b/src/aig/ntl/ntlTime.c
index 94691ab8..c23a4e24 100644
--- a/src/aig/ntl/ntlTime.c
+++ b/src/aig/ntl/ntlTime.c
@@ -88,13 +88,27 @@ Tim_Man_t * Ntl_ManCreateTiming( Ntl_Man_t * p )
     // start the timing manager
     pMan = Tim_ManStart( Aig_ManPiNum(p->pAig), Aig_ManPoNum(p->pAig) );
     // unpack the data in the arrival times
-    if ( pRoot->vArrivals )
-        Vec_IntForEachEntry( pRoot->vArrivals, Entry, i )
-            Tim_ManInitCiArrival( pMan, Entry, Aig_Int2Float(Vec_IntEntry(pRoot->vArrivals,++i)) );
+    if ( pRoot->vTimeInputs )
+    {
+        Vec_IntForEachEntry( pRoot->vTimeInputs, Entry, i )
+        {
+            if ( Entry == -1 )
+                Tim_ManSetCiArrivalAll( pMan, Aig_Int2Float(Vec_IntEntry(pRoot->vTimeInputs,++i)) );
+            else
+                Tim_ManInitCiArrival( pMan, Entry, Aig_Int2Float(Vec_IntEntry(pRoot->vTimeInputs,++i)) );
+        }
+    }
     // unpack the data in the required times
-    if ( pRoot->vRequireds )
-        Vec_IntForEachEntry( pRoot->vRequireds, Entry, i )
-            Tim_ManInitCoRequired( pMan, Entry, Aig_Int2Float(Vec_IntEntry(pRoot->vRequireds,++i)) );
+    if ( pRoot->vTimeOutputs )
+    {
+        Vec_IntForEachEntry( pRoot->vTimeOutputs, Entry, i )
+        {
+            if ( Entry == -1 )
+                Tim_ManSetCoRequiredAll( pMan, Aig_Int2Float(Vec_IntEntry(pRoot->vTimeOutputs,++i)) );
+            else
+                Tim_ManInitCoRequired( pMan, Entry, Aig_Int2Float(Vec_IntEntry(pRoot->vTimeOutputs,++i)) );
+        }
+    }
     // derive timing tables
     vDelayTables = Vec_PtrAlloc( Vec_PtrSize(p->vModels) );
     Ntl_ManForEachModel( p, pModel, i )
@@ -106,7 +120,7 @@ Tim_Man_t * Ntl_ManCreateTiming( Ntl_Man_t * p )
     Tim_ManSetDelayTables( pMan, vDelayTables );
     // set up the boxes
     iBox = 0;
-    curPi = Ntl_ModelCiNum(pRoot);
+    curPi = p->iLastCi;
     Ntl_ManForEachBox( p, pObj, i )
     {
         Tim_ManCreateBoxFirst( pMan, Vec_IntEntry(p->vBox1Cos, iBox), Ntl_ObjFaninNum(pObj), curPi, Ntl_ObjFanoutNum(pObj), pObj->pImplem->pDelayTable );
diff --git a/src/aig/ntl/ntlUtil.c b/src/aig/ntl/ntlUtil.c
index 6849889d..c9ef2dc4 100644
--- a/src/aig/ntl/ntlUtil.c
+++ b/src/aig/ntl/ntlUtil.c
@@ -238,26 +238,6 @@ void Ntl_ManUnmarkCiCoNets( Ntl_Man_t * p )
 
 /**Function*************************************************************
 
-  Synopsis    [Unmarks the CI/CO nets.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-int Ntl_ManCheckNetsAreNotMarked( Ntl_Mod_t * pModel )
-{
-    Ntl_Net_t * pNet;
-    int i;
-    Ntl_ModelForEachNet( pModel, pNet, i )
-        assert( pNet->fMark == 0 );
-    return 1;
-}
-
-/**Function*************************************************************
-
   Synopsis    [Convert initial values of registers to be zero.]
 
   Description []
@@ -274,7 +254,7 @@ void Ntl_ManSetZeroInitValues( Ntl_Man_t * p )
     int i;
     pRoot = Ntl_ManRootModel(p);
     Ntl_ModelForEachLatch( pRoot, pObj, i )
-        pObj->LatchId &= ~3;
+        pObj->LatchId.regInit = 0;
 }
 
 /**Function*************************************************************
@@ -296,7 +276,7 @@ void Ntl_ManAddInverters( Ntl_Obj_t * pObj )
     Ntl_Net_t * pNetLo, * pNetLi, * pNetLoInv, * pNetLiInv;
     Ntl_Obj_t * pNode;
     int nLength, RetValue;
-    assert( (pObj->LatchId & 3) == 1 );
+    assert( Ntl_ObjIsInit1( pObj ) );
     // get the nets
     pNetLi = Ntl_ObjFanin0(pObj);
     pNetLo = Ntl_ObjFanout0(pObj);
@@ -362,11 +342,132 @@ void Ntl_ManTransformInitValues( Ntl_Man_t * p )
     pRoot = Ntl_ManRootModel(p);
     Ntl_ModelForEachLatch( pRoot, pObj, i )
     {
-        if ( (pObj->LatchId & 3) == 1 )
+        if ( Ntl_ObjIsInit1( pObj ) )
             Ntl_ManAddInverters( pObj );
-        pObj->LatchId &= ~3;
+        pObj->LatchId.regInit = 0;
     }
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Counts the number of CIs in the model.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Ntl_ModelCombLeafNum( Ntl_Mod_t * p )
+{
+    Ntl_Obj_t * pObj;
+    int i, Counter = 0;
+    Ntl_ModelForEachCombLeaf( p, pObj, i )
+        Counter += Ntl_ObjFanoutNum( pObj );
+    return Counter;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Counts the number of COs in the model.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Ntl_ModelCombRootNum( Ntl_Mod_t * p )
+{
+    Ntl_Obj_t * pObj;
+    int i, Counter = 0;
+    Ntl_ModelForEachCombRoot( p, pObj, i )
+        Counter += Ntl_ObjFaninNum( pObj );
+    return Counter;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Counts the number of CIs in the model.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Ntl_ModelSeqLeafNum( Ntl_Mod_t * p )
+{
+    Ntl_Obj_t * pObj;
+    int i, Counter = 0;
+    Ntl_ModelForEachSeqLeaf( p, pObj, i )
+        Counter += Ntl_ObjFanoutNum( pObj );
+    return Counter;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Counts the number of COs in the model.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Ntl_ModelSeqRootNum( Ntl_Mod_t * p )
+{
+    Ntl_Obj_t * pObj;
+    int i, Counter = 0;
+    Ntl_ModelForEachSeqRoot( p, pObj, i )
+        Counter += Ntl_ObjFaninNum( pObj );
+    return Counter;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Unmarks the CI/CO nets.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Ntl_ModelCheckNetsAreNotMarked( Ntl_Mod_t * pModel )
+{
+    Ntl_Net_t * pNet;
+    int i;
+    Ntl_ModelForEachNet( pModel, pNet, i )
+        assert( pNet->fMark == 0 );
+    return 1;
+}
+
+/**Function*************************************************************
 
+  Synopsis    [Unmarks the CI/CO nets.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Ntl_ModelClearNets( Ntl_Mod_t * pModel )
+{
+    Ntl_Net_t * pNet;
+    int i;
+    Ntl_ModelForEachNet( pModel, pNet, i )
+    {
+        pNet->nVisits = 0;
+        pNet->pCopy = NULL;
+    }
 }
 
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/aig/ntl/ntlWriteBlif.c b/src/aig/ntl/ntlWriteBlif.c
index 51d41c26..f93e3fa1 100644
--- a/src/aig/ntl/ntlWriteBlif.c
+++ b/src/aig/ntl/ntlWriteBlif.c
@@ -40,15 +40,22 @@
   SeeAlso     []
 
 ***********************************************************************/
-void Ioa_WriteBlifModel( FILE * pFile, Ntl_Mod_t * pModel )
+void Ioa_WriteBlifModel( FILE * pFile, Ntl_Mod_t * pModel, int fMain )
 {
     Ntl_Obj_t * pObj;
     Ntl_Net_t * pNet;
     float Delay;
-    int i, k, fClockAdded = 0;
+    int i, k;
     fprintf( pFile, ".model %s\n", pModel->pName );
-    if ( pModel->fKeep )
-        fprintf( pFile, ".attrib keep\n" );
+    if ( pModel->attrWhite || pModel->attrBox || pModel->attrComb || pModel->attrKeep )
+    {
+        fprintf( pFile, ".attrib" );
+        fprintf( pFile, " %s", pModel->attrWhite? "white": "black" );
+        fprintf( pFile, " %s", pModel->attrBox?   "box"  : "logic" );
+        fprintf( pFile, " %s", pModel->attrComb?  "comb" : "seq"   );
+//        fprintf( pFile, " %s", pModel->attrKeep?  "keep" : "sweep" );
+        fprintf( pFile, "\n" );
+    }
     fprintf( pFile, ".inputs" );
     Ntl_ModelForEachPi( pModel, pObj, i )
         fprintf( pFile, " %s", Ntl_ObjFanout0(pObj)->pName );
@@ -63,19 +70,25 @@ void Ioa_WriteBlifModel( FILE * pFile, Ntl_Mod_t * pModel )
         for ( i = 0; i < Vec_IntSize(pModel->vDelays); i += 3 )
         {
             fprintf( pFile, ".delay" );
-            fprintf( pFile, " %s", Ntl_ObjFanout0(Ntl_ModelPi(pModel, Vec_IntEntry(pModel->vDelays,i)))->pName );
-            fprintf( pFile, " %s", Ntl_ObjFanin0(Ntl_ModelPo(pModel, Vec_IntEntry(pModel->vDelays,i+1)))->pName );
+            if ( Vec_IntEntry(pModel->vDelays,i) != -1 )
+                fprintf( pFile, " %s", Ntl_ObjFanout0(Ntl_ModelPi(pModel, Vec_IntEntry(pModel->vDelays,i)))->pName );
+            if ( Vec_IntEntry(pModel->vDelays,i+1) != -1 )
+                fprintf( pFile, " %s", Ntl_ObjFanin0(Ntl_ModelPo(pModel, Vec_IntEntry(pModel->vDelays,i+1)))->pName );
             fprintf( pFile, " %.3f", Aig_Int2Float(Vec_IntEntry(pModel->vDelays,i+2)) );
             fprintf( pFile, "\n" );
         }
     }
-    if ( pModel->vArrivals )
+    if ( pModel->vTimeInputs )
     {
-        for ( i = 0; i < Vec_IntSize(pModel->vArrivals); i += 2 )
+        for ( i = 0; i < Vec_IntSize(pModel->vTimeInputs); i += 2 )
         {
-            fprintf( pFile, ".input_arrival" );
-            fprintf( pFile, " %s", Ntl_ObjFanout0(Ntl_ModelPi(pModel, Vec_IntEntry(pModel->vArrivals,i)))->pName );
-            Delay = Aig_Int2Float(Vec_IntEntry(pModel->vArrivals,i+1));
+            if ( fMain )
+                fprintf( pFile, ".input_arrival" );
+            else
+                fprintf( pFile, ".input_required" );
+            if ( Vec_IntEntry(pModel->vTimeInputs,i) != -1 )
+                fprintf( pFile, " %s", Ntl_ObjFanout0(Ntl_ModelPi(pModel, Vec_IntEntry(pModel->vTimeInputs,i)))->pName );
+            Delay = Aig_Int2Float(Vec_IntEntry(pModel->vTimeInputs,i+1));
             if ( Delay == -TIM_ETERNITY )
                 fprintf( pFile, " -inf" );
             else if ( Delay == TIM_ETERNITY )
@@ -85,13 +98,17 @@ void Ioa_WriteBlifModel( FILE * pFile, Ntl_Mod_t * pModel )
             fprintf( pFile, "\n" );
         }
     }
-    if ( pModel->vRequireds )
+    if ( pModel->vTimeOutputs )
     {
-        for ( i = 0; i < Vec_IntSize(pModel->vRequireds); i += 2 )
+        for ( i = 0; i < Vec_IntSize(pModel->vTimeOutputs); i += 2 )
         {
-            fprintf( pFile, ".output_required" );
-            fprintf( pFile, " %s", Ntl_ObjFanin0(Ntl_ModelPo(pModel, Vec_IntEntry(pModel->vRequireds,i)))->pName );
-            Delay = Aig_Int2Float(Vec_IntEntry(pModel->vRequireds,i+1));
+            if ( fMain )
+                fprintf( pFile, ".output_required" );
+            else
+                fprintf( pFile, ".output_arrival" );
+            if ( Vec_IntEntry(pModel->vTimeOutputs,i) != -1 )
+                fprintf( pFile, " %s", Ntl_ObjFanin0(Ntl_ModelPo(pModel, Vec_IntEntry(pModel->vTimeOutputs,i)))->pName );
+            Delay = Aig_Int2Float(Vec_IntEntry(pModel->vTimeOutputs,i+1));
             if ( Delay == -TIM_ETERNITY )
                 fprintf( pFile, " -inf" );
             else if ( Delay == TIM_ETERNITY )
@@ -117,13 +134,27 @@ void Ioa_WriteBlifModel( FILE * pFile, Ntl_Mod_t * pModel )
             fprintf( pFile, ".latch" );
             fprintf( pFile, " %s", Ntl_ObjFanin0(pObj)->pName );
             fprintf( pFile, " %s", Ntl_ObjFanout0(pObj)->pName );
-            if ( pObj->LatchId >> 2 )
-                fprintf( pFile, " %d", pObj->LatchId >> 2 );
-            if ( Ntl_ObjFanin(pObj, 1) != NULL )
-                fprintf( pFile, " %s", Ntl_ObjFanin(pObj, 1)->pName );
-            else if ( pObj->LatchId >> 2 )
-                fprintf( pFile, " clock99" ), fClockAdded = 1;
-            fprintf( pFile, " %d", pObj->LatchId & 3 );
+            assert( pObj->LatchId.regType == 0 || pObj->LatchId.regClass == 0 );
+            if ( pObj->LatchId.regType )
+            {
+                if ( pObj->LatchId.regType == 1 )
+                    fprintf( pFile, " fe" );
+                else if ( pObj->LatchId.regType == 2 )
+                    fprintf( pFile, " re" );
+                else if ( pObj->LatchId.regType == 3 )
+                    fprintf( pFile, " ah" );
+                else if ( pObj->LatchId.regType == 4 )
+                    fprintf( pFile, " al" );
+                else if ( pObj->LatchId.regType == 5 )
+                    fprintf( pFile, " as" );
+                else
+                    assert( 0 );
+            }
+            else if ( pObj->LatchId.regClass )
+                fprintf( pFile, " %d", pObj->LatchId.regClass );
+            if ( pObj->pClock )
+                fprintf( pFile, " %s", pObj->pClock->pName );
+            fprintf( pFile, " %d", pObj->LatchId.regInit );
             fprintf( pFile, "\n" );
         }
         else if ( Ntl_ObjIsBox(pObj) )
@@ -136,8 +167,6 @@ void Ioa_WriteBlifModel( FILE * pFile, Ntl_Mod_t * pModel )
             fprintf( pFile, "\n" );
         }
     }
-    if ( fClockAdded )
-        fprintf( pFile, ".names clock99\n 0\n" );
     fprintf( pFile, ".end\n\n" );
 }
 
@@ -167,7 +196,7 @@ void Ioa_WriteBlif( Ntl_Man_t * p, char * pFileName )
     fprintf( pFile, "# Benchmark \"%s\" written by ABC-8 on %s\n", p->pName, Ioa_TimeStamp() );
     // write the models
     Ntl_ManForEachModel( p, pModel, i )
-        Ioa_WriteBlifModel( pFile, pModel );
+        Ioa_WriteBlifModel( pFile, pModel, i==0 );
     // close the file
     fclose( pFile );
 }