Version abc80611

17 files changed, 644 insertions, 222 deletions

diff --git a/abctestlib.dsw b/abctestlib.dsw
new file mode 100644
index 00000000..7ae6cac9
--- /dev/null
+++ b/abctestlib.dsw
@@ -0,0 +1,29 @@
+Microsoft Developer Studio Workspace File, Format Version 6.00
+# WARNING: DO NOT EDIT OR DELETE THIS WORKSPACE FILE!
+
+###############################################################################
+
+Project: "abctestlib"=.\abctestlib.dsp - Package Owner=<4>
+
+Package=<5>
+{{{
+}}}
+
+Package=<4>
+{{{
+}}}
+
+###############################################################################
+
+Global:
+
+Package=<5>
+{{{
+}}}
+
+Package=<3>
+{{{
+}}}
+
+###############################################################################
+
diff --git a/src/aig/aig/aig.h b/src/aig/aig/aig.h
index 745de35d..1f101584 100644
--- a/src/aig/aig/aig.h
+++ b/src/aig/aig/aig.h
@@ -152,7 +152,8 @@ struct Aig_Man_t_
     Vec_Ptr_t *      vOnehots;
     Aig_Man_t *      pManHaig;
     int              fCreatePios;
-    Vec_Int_t *      vEquPairs;      
+    Vec_Int_t *      vEquPairs;   
+    Vec_Vec_t *      vClockDoms; 
     // timing statistics
     int              time1;
     int              time2;
diff --git a/src/aig/aig/aigMan.c b/src/aig/aig/aigMan.c
index 9877fdae..dae7e42b 100644
--- a/src/aig/aig/aigMan.c
+++ b/src/aig/aig/aigMan.c
@@ -209,6 +209,7 @@ void Aig_ManStop( Aig_Man_t * p )
     if ( p->vFlopReprs)Vec_IntFree( p->vFlopReprs );
     if ( p->pManExdc ) Aig_ManStop( p->pManExdc );
     if ( p->vOnehots ) Vec_VecFree( (Vec_Vec_t *)p->vOnehots );
+    if ( p->vClockDoms)Vec_VecFree( p->vClockDoms );
     FREE( p->pData );
     FREE( p->pSeqModel );
     FREE( p->pName );
diff --git a/src/aig/aig/aigPartReg.c b/src/aig/aig/aigPartReg.c
index 3a008d12..145d2029 100644
--- a/src/aig/aig/aigPartReg.c
+++ b/src/aig/aig/aigPartReg.c
@@ -473,7 +473,7 @@ Vec_Ptr_t * Aig_ManRegPartitionSimple( Aig_Man_t * pAig, int nPartSize, int nOve
     int i, Counter;
     if ( nOverSize >= nPartSize )
     {
-        printf( "Overlap size (%d) if more or equal to the partition size (%d).\n", nOverSize, nPartSize );
+        printf( "Overlap size (%d) is more or equal than the partition size (%d).\n", nOverSize, nPartSize );
         printf( "Adjusting it to be equal to half of the partition size.\n" );
         nOverSize = nPartSize/2;
     }
diff --git a/src/aig/aig/aigScl.c b/src/aig/aig/aigScl.c
index 2c779c40..153ac421 100644
--- a/src/aig/aig/aigScl.c
+++ b/src/aig/aig/aigScl.c
@@ -627,7 +627,7 @@ Aig_Man_t * Aig_ManScl( Aig_Man_t * pAig, int fLatchConst, int fLatchEqual, int
     pAigNew = Aig_ManDupRepr( pAigInit, 0 );
     Aig_ManSeqCleanup( pAigNew );
 
-    Saig_ManReportUselessRegisters( pAigNew );
+//    Saig_ManReportUselessRegisters( pAigNew );
     if ( Aig_ManRegNum(pAigNew) == 0 )
         return pAigNew;
 //    nRegs = Saig_ManReportComplements( pAigNew );
diff --git a/src/aig/ntl/ntl.h b/src/aig/ntl/ntl.h
index b496cb13..44a9f97c 100644
--- a/src/aig/ntl/ntl.h
+++ b/src/aig/ntl/ntl.h
@@ -73,12 +73,12 @@ struct Ntl_Man_t_
     // extracted representation
     Vec_Ptr_t *        vCis;           // the primary inputs of the extracted part
     Vec_Ptr_t *        vCos;           // the primary outputs of the extracted part 
-    Vec_Ptr_t *        vNodes;         // the nodes of the abstracted part
-    Vec_Int_t *        vBox1Cos;       // the first COs of the boxes
+    Vec_Ptr_t *        vVisNodes;      // the nodes of the abstracted part
+    Vec_Int_t *        vBox1Cios;      // the first COs of the boxes
+    Vec_Int_t *        vRegClasses;    // the classes of registers in the AIG
     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
@@ -146,7 +146,11 @@ struct Ntl_Net_t_
 {
     Ntl_Net_t *        pNext;          // next net in the hash table
     void *             pCopy;          // the copy of this object
-    void *             pCopy2;         // the copy of this object
+    union {
+        void *         pCopy2;         // the copy of this object
+        int            iTemp;          // other data
+        float          dTemp;          // other data
+    };
     Ntl_Obj_t *        pDriver;        // driver of the net
     char               nVisits;        // the number of times the net is visited
     char               fMark;          // temporary mark
@@ -240,12 +244,6 @@ static inline int         Ntl_ObjIsSeqRoot( Ntl_Obj_t * p )       { return Ntl_O
     Vec_PtrForEachEntry( p->vCis, pNet, i )
 #define Ntl_ManForEachCoNet( p, pNet, i )                                       \
     Vec_PtrForEachEntry( p->vCos, pNet, 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 )                                         \
-    for ( i = 0; (i < Vec_PtrSize(p->vNodes)) && (((pObj) = Vec_PtrEntry(p->vNodes, i)), 1); i++ ) \
-        if ( (pObj) == NULL || !Ntl_ObjIsBox(pObj) ) {} else
 
 #define Ntl_ModelForEachPi( pNwk, pObj, i )                                     \
     for ( i = 0; (i < Vec_PtrSize(pNwk->vPis)) && (((pObj) = (Ntl_Obj_t*)Vec_PtrEntry(pNwk->vPis, i)), 1); i++ )
@@ -299,10 +297,12 @@ static inline int         Ntl_ObjIsSeqRoot( Ntl_Obj_t * p )       { return Ntl_O
 extern ABC_DLL int             Ntl_ManInsertTest( Ntl_Man_t * p, Aig_Man_t * pAig );
 extern ABC_DLL int             Ntl_ManInsertTestIf( Ntl_Man_t * p, Aig_Man_t * pAig );
 /*=== ntlEc.c ==========================================================*/
-extern ABC_DLL void            Ntl_ManPrepareCec( char * pFileName1, char * pFileName2, Aig_Man_t ** ppMan1, Aig_Man_t ** ppMan2 );
+extern ABC_DLL void            Ntl_ManPrepareCecMans( Ntl_Man_t * pMan1, Ntl_Man_t * pMan2, Aig_Man_t ** ppAig1, Aig_Man_t ** ppAig2 );
+extern ABC_DLL void            Ntl_ManPrepareCec( char * pFileName1, char * pFileName2, Aig_Man_t ** ppAig1, Aig_Man_t ** ppAig2 );
 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_ManCollapseComb( Ntl_Man_t * p );
 extern ABC_DLL Aig_Man_t *     Ntl_ManCollapseSeq( Ntl_Man_t * p );
 /*=== ntlInsert.c ==========================================================*/
@@ -320,8 +320,6 @@ extern ABC_DLL void            Ntl_ManCleanup( Ntl_Man_t * p );
 extern ABC_DLL Ntl_Man_t *     Ntl_ManStartFrom( Ntl_Man_t * p );
 extern ABC_DLL Ntl_Man_t *     Ntl_ManDup( Ntl_Man_t * p );
 extern ABC_DLL void            Ntl_ManFree( Ntl_Man_t * p );
-extern ABC_DLL int             Ntl_ManIsComb( Ntl_Man_t * p );
-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 );
@@ -377,6 +375,9 @@ extern ABC_DLL void            Ntl_ManMarkCiCoNets( Ntl_Man_t * p );
 extern ABC_DLL void            Ntl_ManUnmarkCiCoNets( Ntl_Man_t * p );
 extern ABC_DLL void            Ntl_ManSetZeroInitValues( Ntl_Man_t * p );
 extern ABC_DLL void            Ntl_ManTransformInitValues( Ntl_Man_t * p );
+extern ABC_DLL Vec_Vec_t *     Ntl_ManTransformRegClasses( Ntl_Man_t * pMan, int nSizeMax, int fVerbose );
+extern ABC_DLL int             Ntl_ManLatchNum( Ntl_Man_t * p );
+extern ABC_DLL int             Ntl_ManIsComb( 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 );
diff --git a/src/aig/ntl/ntlCheck.c b/src/aig/ntl/ntlCheck.c
index d3aecc8d..b4125804 100644
--- a/src/aig/ntl/ntlCheck.c
+++ b/src/aig/ntl/ntlCheck.c
@@ -31,6 +31,61 @@
 
 /**Function*************************************************************
 
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Ntl_ModelCheckCombPoPaths_rec( Ntl_Mod_t * pModel, Ntl_Net_t * pNet )
+{
+    Ntl_Net_t * pFanin;
+    int i;
+    // skip visited nets
+    if ( pNet->nVisits == 2 ) 
+        return 1;
+    pNet->nVisits = 2;
+    // process PIs
+    if ( Ntl_ObjIsPi(pNet->pDriver) )
+        return 0;
+    // process registers
+    if ( Ntl_ObjIsLatch(pNet->pDriver) )
+        return 1;
+    assert( Ntl_ObjIsNode(pNet->pDriver) );
+    // call recursively
+    Ntl_ObjForEachFanin( pNet->pDriver, pFanin, i )
+        if ( !Ntl_ModelCheckCombPoPaths_rec( pModel, pFanin ) )
+            return 0;
+    return 1;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Checks the existence of combinational paths from POs to PIs.]
+
+  Description [Returns 0 if the path is found.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Ntl_ModelCheckCombPoPaths( Ntl_Mod_t * pModel )
+{
+    Ntl_Obj_t * pObj;
+    int i;
+    Ntl_ModelClearNets( pModel );
+    Ntl_ModelForEachPo( pModel, pObj, i )
+        if ( !Ntl_ModelCheckCombPoPaths_rec( pModel, Ntl_ObjFanin0(pObj) ) )
+            return 0;
+    return 1;
+}
+
+/**Function*************************************************************
+
   Synopsis    [Checks one model.]
 
   Description []
@@ -91,14 +146,14 @@ int Ntl_ModelCheck( Ntl_Mod_t * pModel, int fMain )
             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) );        
+            Vec_IntPush( pModel->vTimeInputs, Aig_Float2Int(0.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 );
+//            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) );        
+            Vec_IntPush( pModel->vTimeOutputs, Aig_Float2Int(0.0) );        
         }
     }
 
@@ -122,12 +177,22 @@ int Ntl_ModelCheck( Ntl_Mod_t * pModel, int fMain )
         // 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 );
+            printf( "Model %s is a comb white box, yet it has no nodes.\n", pModel->pName );
+            fStatus = 0;
+        }
+        if ( pModel->attrComb && Ntl_ModelLatchNum(pModel) > 0 )
+        {
+            printf( "Model %s is a comb white box, yet it has registers.\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 );
+            printf( "Model %s is a seq white box, yet it has no registers.\n", pModel->pName );
+            fStatus = 0;
+        }
+        if ( !pModel->attrComb && !Ntl_ModelCheckCombPoPaths(pModel) )
+        {
+            printf( "Model %s is a seq white box with comb paths from PIs to POs.\n", pModel->pName );
             fStatus = 0;
         }
     }
@@ -292,7 +357,7 @@ void Ntl_ModelTransformLatches( Ntl_Mod_t * pModel )
         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) );
+    printf( "In the main model \"%s\", %d latches are transformed into white seq boxes.\n", pModel->pName, Ntl_ModelLatchNum(pModel) );
     pModel->nObjs[NTL_OBJ_BOX] += Ntl_ModelLatchNum(pModel);
     pModel->nObjs[NTL_OBJ_LATCH] = 0;
 }
diff --git a/src/aig/ntl/ntlEc.c b/src/aig/ntl/ntlEc.c
index 3ed6556d..4850f647 100644
--- a/src/aig/ntl/ntlEc.c
+++ b/src/aig/ntl/ntlEc.c
@@ -170,7 +170,6 @@ void Ntl_ManDeriveCommonCos( Ntl_Man_t * pMan1, Ntl_Man_t * pMan2, int fSeq )
     Vec_PtrClear( pMan2->vCos );
     if ( fSeq ) 
     {
-        assert( Ntl_ModelSeqRootNum(p1) == Ntl_ModelSeqRootNum(p2) );
         Ntl_ModelForEachSeqRoot( p1, pObj, i )
         {
             Ntl_ObjForEachFanin( pObj, pNext, k )
@@ -189,7 +188,6 @@ void Ntl_ManDeriveCommonCos( Ntl_Man_t * pMan1, Ntl_Man_t * pMan2, int fSeq )
     }
     else
     {
-        assert( Ntl_ModelCombRootNum(p1) == Ntl_ModelCombRootNum(p2) );
         Ntl_ModelForEachCombRoot( p1, pObj, i )
         {
             Ntl_ObjForEachFanin( pObj, pNext, k )
@@ -219,22 +217,11 @@ void Ntl_ManDeriveCommonCos( Ntl_Man_t * pMan1, Ntl_Man_t * pMan2, int fSeq )
   SeeAlso     []
 
 ***********************************************************************/
-void Ntl_ManPrepareCec( char * pFileName1, char * pFileName2, Aig_Man_t ** ppMan1, Aig_Man_t ** ppMan2 )
+void Ntl_ManPrepareCecMans( Ntl_Man_t * pMan1, Ntl_Man_t * pMan2, Aig_Man_t ** ppAig1, Aig_Man_t ** ppAig2 )
 {
-    Ntl_Man_t * pMan1, * pMan2;
     Ntl_Mod_t * pModel1, * pModel2;
-    *ppMan1 = NULL;
-    *ppMan2 = NULL;
-    // read the netlists
-    pMan1 = Ioa_ReadBlif( pFileName1, 1 );
-    pMan2 = Ioa_ReadBlif( pFileName2, 1 );
-    if ( !pMan1 || !pMan2 )
-    {
-        if ( pMan1 )  Ntl_ManFree( pMan1 );
-        if ( pMan2 )  Ntl_ManFree( pMan2 );
-        printf( "Ntl_ManPrepareCec(): Reading designs from file has failed.\n" );
-        return;
-    }
+    *ppAig1 = NULL;
+    *ppAig2 = NULL;
     // make sure they are compatible
     pModel1 = Ntl_ManRootModel( pMan1 );
     pModel2 = Ntl_ManRootModel( pMan2 );
@@ -267,8 +254,35 @@ void Ntl_ManPrepareCec( char * pFileName1, char * pFileName2, Aig_Man_t ** ppMan
         return;
     }
     // derive AIGs
-    *ppMan1 = Ntl_ManCollapseComb( pMan1 );
-    *ppMan2 = Ntl_ManCollapseComb( pMan2 );
+    *ppAig1 = Ntl_ManCollapse( pMan1, 0 );
+    *ppAig2 = Ntl_ManCollapse( pMan2, 0 );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Prepares AIGs for combinational equivalence checking.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Ntl_ManPrepareCec( char * pFileName1, char * pFileName2, Aig_Man_t ** ppAig1, Aig_Man_t ** ppAig2 )
+{
+    Ntl_Man_t * pMan1, * pMan2;
+    // read the netlists
+    pMan1 = Ioa_ReadBlif( pFileName1, 1 );
+    pMan2 = Ioa_ReadBlif( pFileName2, 1 );
+    if ( !pMan1 || !pMan2 )
+    {
+        if ( pMan1 )  Ntl_ManFree( pMan1 );
+        if ( pMan2 )  Ntl_ManFree( pMan2 );
+        printf( "Ntl_ManPrepareCec(): Reading designs from file has failed.\n" );
+        return;
+    }
+    Ntl_ManPrepareCecMans( pMan1, pMan2, ppAig1, ppAig2 );
     // cleanup 
     Ntl_ManFree( pMan1 );
     Ntl_ManFree( pMan2 );
@@ -303,15 +317,15 @@ Aig_Man_t * Ntl_ManPrepareSec( char * pFileName1, char * pFileName2 )
         return NULL;
     }
     // make sure they are compatible
-    pModel1 = Ntl_ManRootModel( pMan1 );
-    pModel2 = Ntl_ManRootModel( pMan2 );
-    if ( Ntl_ModelLatchNum(pModel1) == 0 || Ntl_ModelLatchNum(pModel2) == 0 )
+    if ( Ntl_ManLatchNum(pMan1) == 0 || Ntl_ManLatchNum(pMan2) == 0 )
     {
         if ( pMan1 )  Ntl_ManFree( pMan1 );
         if ( pMan2 )  Ntl_ManFree( pMan2 );
         printf( "Ntl_ManPrepareSec(): The designs have no latches. Use combinational command \"*cec\".\n" );
         return NULL;
     }
+    pModel1 = Ntl_ManRootModel( pMan1 );
+    pModel2 = Ntl_ManRootModel( pMan2 );
     if ( Ntl_ModelSeqLeafNum(pModel1) != Ntl_ModelSeqLeafNum(pModel2) )
     {
         printf( "Warning: The number of inputs in the designs is different (%d and %d).\n", 
@@ -334,8 +348,8 @@ Aig_Man_t * Ntl_ManPrepareSec( char * pFileName1, char * pFileName2 )
         return NULL;
     }
     // derive AIGs
-    pAig1 = Ntl_ManCollapseSeq( pMan1 );
-    pAig2 = Ntl_ManCollapseSeq( pMan2 );
+    pAig1 = Ntl_ManCollapse( pMan1, 1 );
+    pAig2 = Ntl_ManCollapse( pMan2, 1 );
     pAig = Saig_ManCreateMiter( pAig1, pAig2, 0 );
     Aig_ManStop( pAig1 );
     Aig_ManStop( pAig2 );
diff --git a/src/aig/ntl/ntlExtract.c b/src/aig/ntl/ntlExtract.c
index a552f949..d6cbfab0 100644
--- a/src/aig/ntl/ntlExtract.c
+++ b/src/aig/ntl/ntlExtract.c
@@ -181,7 +181,7 @@ int Ntl_ManExtract_rec( Ntl_Man_t * p, Ntl_Net_t * pNet )
         assert( Ntl_BoxIsComb(pObj) );
         assert( Ntl_ModelLatchNum(pObj->pImplem) == 0 );
         assert( pObj->pImplem->vDelays != NULL );
-        Vec_IntPush( p->vBox1Cos, Aig_ManPoNum(p->pAig) );
+        Vec_IntPush( p->vBox1Cios, Aig_ManPoNum(p->pAig) );
         Ntl_ObjForEachFanin( pObj, pNetFanin, i )
         {
             LevelCur = Aig_ObjLevel( Aig_Regular(pNetFanin->pCopy) );
@@ -196,7 +196,7 @@ int Ntl_ManExtract_rec( Ntl_Man_t * p, Ntl_Net_t * pNet )
             Aig_ObjSetLevel( pNetFanin->pCopy, LevelMax + 1 );
         }
     }
-    Vec_PtrPush( p->vNodes, pObj );
+    Vec_PtrPush( p->vVisNodes, pObj );
     if ( Ntl_ObjIsNode(pObj) )
         pNet->pCopy = Ntl_ManBuildNodeAig( pObj );
     pNet->nVisits = 2;
@@ -223,10 +223,10 @@ Aig_Man_t * Ntl_ManExtract( Ntl_Man_t * p )
     Ntl_Net_t * pNet;
     int i, k, nUselessObjects;
     Ntl_ManCleanup( p );
-    assert( Vec_PtrSize(p->vCis) == 0 );
-    assert( Vec_PtrSize(p->vCos) == 0 );
-    assert( Vec_PtrSize(p->vNodes) == 0 );
-    assert( Vec_IntSize(p->vBox1Cos) == 0 );
+    Vec_PtrClear( p->vCis );
+    Vec_PtrClear( p->vCos );
+    Vec_PtrClear( p->vVisNodes );
+    Vec_IntClear( p->vBox1Cios );
     // start the AIG manager
     assert( p->pAig == NULL );
     p->pAig = Aig_ManStart( 10000 );
@@ -279,9 +279,9 @@ Aig_Man_t * Ntl_ManExtract( Ntl_Man_t * p )
         }
     }
     // report the number of dangling objects
-    nUselessObjects = Ntl_ModelNodeNum(pRoot) + Ntl_ModelLut1Num(pRoot) + Ntl_ModelBoxNum(pRoot) - Vec_PtrSize(p->vNodes);
+    nUselessObjects = Ntl_ModelNodeNum(pRoot) + Ntl_ModelLut1Num(pRoot) + Ntl_ModelBoxNum(pRoot) - Vec_PtrSize(p->vVisNodes);
 //    if ( nUselessObjects )
-//        printf( "The number of nodes that do not feed into POs = %d.\n", nUselessObjects );
+//        printf( "The number of dangling objects = %d.\n", nUselessObjects );
     // cleanup the AIG
     Aig_ManCleanup( p->pAig );
     // extract the timing manager
@@ -307,7 +307,7 @@ Aig_Man_t * Ntl_ManExtract( Ntl_Man_t * p )
   SeeAlso     []
 
 ***********************************************************************/
-int Ntl_ManCollapseBox_rec( Ntl_Man_t * p, Ntl_Obj_t * pBox, int fSeq )
+int Ntl_ManCollapseBoxComb_rec( Ntl_Man_t * p, Ntl_Obj_t * pBox, int fSeq )
 {
     extern int Ntl_ManCollapse_rec( Ntl_Man_t * p, Ntl_Net_t * pNet, int fSeq );
     Ntl_Mod_t * pModel = pBox->pImplem;
@@ -326,17 +326,51 @@ int Ntl_ManCollapseBox_rec( Ntl_Man_t * p, Ntl_Obj_t * pBox, int fSeq )
         pNet->pCopy = pNetBox->pCopy;
         pNet->nVisits = 2;
     }
-    // check if there are registers
-    if ( Ntl_ModelLatchNum(pModel) )
+    // compute AIG for the internal nodes
+    Ntl_ModelForEachPo( pModel, pObj, i )
     {
-        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;
-        }
+        pNet = Ntl_ObjFanin0(pObj);
+        if ( !Ntl_ManCollapse_rec( p, pNet, fSeq ) )
+            return 0;
+        pNetBox = Ntl_ObjFanout( pBox, i );
+        pNetBox->pCopy = pNet->pCopy;
+    }
+    return 1;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Collects the nodes in a topological order.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Ntl_ManCollapseBoxSeq1_rec( Ntl_Man_t * p, Ntl_Obj_t * pBox, int fSeq )
+{
+    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;
+    int i;
+    assert( Ntl_ModelLatchNum(pModel) > 0 );
+    assert( Ntl_ObjFaninNum(pBox) == Ntl_ModelPiNum(pModel) );
+    assert( Ntl_ObjFanoutNum(pBox) == Ntl_ModelPoNum(pModel) );
+    // clear net visited flags
+    Ntl_ModelClearNets( pModel );
+    // initialize the registers
+    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;
+        // remember the class of this register
+        Vec_IntPush( p->vRegClasses, pObj->LatchId.regClass );
     }
     // compute AIG for the internal nodes
     Ntl_ModelForEachPo( pModel, pObj, i )
@@ -347,19 +381,59 @@ int Ntl_ManCollapseBox_rec( Ntl_Man_t * p, Ntl_Obj_t * pBox, int fSeq )
         pNetBox = Ntl_ObjFanout( pBox, i );
         pNetBox->pCopy = pNet->pCopy;
     }
+    return 1;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Collects the nodes in a topological order.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Ntl_ManCollapseBoxSeq2_rec( Ntl_Man_t * p, Ntl_Obj_t * pBox, int fSeq, int iFirstPi )
+{
+    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;
+    int i;
+    assert( Ntl_ModelLatchNum(pModel) > 0 );
+    assert( Ntl_ObjFaninNum(pBox) == Ntl_ModelPiNum(pModel) );
+    assert( Ntl_ObjFanoutNum(pBox) == Ntl_ModelPoNum(pModel) );
+    // clear net visited flags
+    Ntl_ModelClearNets( pModel );
+    // transfer from the box to the PIs of the model
+    Ntl_ModelForEachPi( pModel, pObj, i )
+    {
+        pNet = Ntl_ObjFanout0(pObj);
+        pNetBox = Ntl_ObjFanin( pBox, i );
+        pNet->pCopy = pNetBox->pCopy;
+        pNet->nVisits = 2;
+    }
+    // initialize the registers
+    Ntl_ModelForEachLatch( pModel, pObj, i )
+    {
+        pNet = Ntl_ObjFanout0(pObj);
+        pNet->pCopy = Aig_ManPi( p->pAig, iFirstPi++ );
+        if ( fSeq && Ntl_ObjIsInit1( pObj ) )
+            pNet->pCopy = Aig_Not(pNet->pCopy);
+        pNet->nVisits = 2;
+    }
     // compute AIGs for the registers
-    if ( Ntl_ModelLatchNum(pModel) )
+    Ntl_ModelForEachLatch( pModel, pObj, i )
     {
-        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 );
-        }
+        pNet = Ntl_ObjFanin0(pObj);
+        if ( !Ntl_ManCollapse_rec( p, pNet, fSeq ) )
+            return 0;
+        if ( fSeq && Ntl_ObjIsInit1( pObj ) )
+            Aig_ObjCreatePo( p->pAig, Aig_Not(pNet->pCopy) );
+        else
+            Aig_ObjCreatePo( p->pAig, pNet->pCopy );
     }
     return 1;
 }
@@ -398,8 +472,8 @@ int Ntl_ManCollapse_rec( Ntl_Man_t * p, Ntl_Net_t * pNet, int fSeq )
     // add box inputs/outputs to COs/CIs
     if ( Ntl_ObjIsBox(pObj) )
     {
-        assert( Ntl_BoxIsWhite(pObj) );
-        if ( !Ntl_ManCollapseBox_rec( p, pObj, fSeq ) )
+        assert( Ntl_BoxIsWhite(pObj) && Ntl_BoxIsComb(pObj) );
+        if ( !Ntl_ManCollapseBoxComb_rec( p, pObj, fSeq ) )
             return 0;
     }
     if ( Ntl_ObjIsNode(pObj) )
@@ -423,17 +497,18 @@ int Ntl_ManCollapse_rec( Ntl_Man_t * p, Ntl_Net_t * pNet, int fSeq )
 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 * pBox;
     Ntl_Net_t * pNet;
-    int i;
+    int i, k, nTruePis, nTruePos, iBox = 0;
     assert( Vec_PtrSize(p->vCis) != 0 );
     assert( Vec_PtrSize(p->vCos) != 0 );
-    assert( Vec_PtrSize(p->vLatchIns) == 0 );
+    Vec_IntClear( p->vBox1Cios );
+    Vec_IntClear( p->vRegClasses );
     // clear net visited flags
     pRoot = Ntl_ManRootModel(p);
-    Ntl_ModelClearNets( pRoot );
     assert( Ntl_ModelLatchNum(pRoot) == 0 );
+    Ntl_ModelClearNets( pRoot );
     // create the manager
     p->pAig = Aig_ManStart( 10000 );
     p->pAig->pName = Aig_UtilStrsav( p->pName );
@@ -444,26 +519,56 @@ Aig_Man_t * Ntl_ManCollapse( Ntl_Man_t * p, int fSeq )
         pNet->pCopy = Aig_ObjCreatePi( p->pAig );
         if ( pNet->nVisits )
         {
-            printf( "Ntl_ManCollapseForCec(): Primary input appears twice in the list.\n" );
+            printf( "Ntl_ManCollapse(): Primary input appears twice in the list.\n" );
             return 0;
         }
         pNet->nVisits = 2;
     }
+    nTruePis = Aig_ManPiNum(p->pAig);
+    // create inputs of seq boxes
+    if ( fSeq )
+    Ntl_ModelForEachBox( pRoot, pBox, i )
+    {
+        if ( !(Ntl_BoxIsSeq(pBox) && Ntl_BoxIsWhite(pBox)) )
+            continue;
+        Vec_IntPush( p->vBox1Cios, Aig_ManPiNum(p->pAig) );
+        Ntl_ManCollapseBoxSeq1_rec( p, pBox, fSeq );
+        Ntl_ObjForEachFanout( pBox, pNet, k )
+            pNet->nVisits = 2;
+    }
     // derive the outputs
     Ntl_ManForEachCoNet( p, pNet, i )
     {
         if ( !Ntl_ManCollapse_rec( p, pNet, fSeq ) )
         {
-            printf( "Ntl_ManCollapseForCec(): Error: Combinational loop is detected.\n" );
+            printf( "Ntl_ManCollapse(): Error: Combinational loop is detected.\n" );
             return 0;
         }
         Aig_ObjCreatePo( p->pAig, pNet->pCopy );
     }
-    // add the latch inputs
-    Vec_PtrForEachEntry( p->vLatchIns, pTemp, i )
-        Aig_ObjCreatePo( p->pAig, pTemp );
+    nTruePos = Aig_ManPoNum(p->pAig);
+    // create outputs of seq boxes
+    if ( fSeq )
+    Ntl_ModelForEachBox( pRoot, pBox, i )
+    {
+        if ( !(Ntl_BoxIsSeq(pBox) && Ntl_BoxIsWhite(pBox)) )
+            continue;
+        Ntl_ObjForEachFanin( pBox, pNet, k )
+            if ( !Ntl_ManCollapse_rec( p, pNet, fSeq ) )
+            {
+                printf( "Ntl_ManCollapse(): Error: Combinational loop is detected.\n" );
+                return 0;
+            }
+        Ntl_ManCollapseBoxSeq2_rec( p, pBox, fSeq, Vec_IntEntry(p->vBox1Cios, iBox++) );
+    }
+    // make sure registers are added correctly
+    if ( Aig_ManPiNum(p->pAig) - nTruePis != Aig_ManPoNum(p->pAig) - nTruePos )
+    {
+        printf( "Ntl_ManCollapse(): Error: Registers are created incorrectly.\n" );
+        return 0;
+    }
     // cleanup the AIG
-    Aig_ManSetRegNum( p->pAig, Vec_PtrSize(p->vLatchIns) );
+    Aig_ManSetRegNum( p->pAig, Aig_ManPiNum(p->pAig) - nTruePis );
     Aig_ManCleanup( p->pAig );
     pAig = p->pAig; p->pAig = NULL;
     return pAig;    
@@ -490,7 +595,6 @@ Aig_Man_t * Ntl_ManCollapseComb( Ntl_Man_t * p )
     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
@@ -519,13 +623,13 @@ Aig_Man_t * Ntl_ManCollapseComb( Ntl_Man_t * p )
 ***********************************************************************/
 Aig_Man_t * Ntl_ManCollapseSeq( Ntl_Man_t * p )
 {
+    Aig_Man_t * pAig;
     Ntl_Mod_t * pRoot;
     Ntl_Obj_t * pObj;
     Ntl_Net_t * pNet;
     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
@@ -537,7 +641,17 @@ Aig_Man_t * Ntl_ManCollapseSeq( Ntl_Man_t * p )
         Ntl_ObjForEachFanin( pObj, pNet, k )
             Vec_PtrPush( p->vCos, pNet );
     // perform the traversal
-    return Ntl_ManCollapse( p, 1 );
+    pAig = Ntl_ManCollapse( p, 1 );
+    // check if there are register classes
+    pAig->vClockDoms = Ntl_ManTransformRegClasses( p, 100, 1 );
+    if ( pAig->vClockDoms )
+    {
+        if ( Vec_VecSize(pAig->vClockDoms) == 0 )
+            printf( "Clock domains are small. Seq synthesis is not performed.\n" );
+        else
+            printf( "Performing seq synthesis for %d clock domains.\n", Vec_VecSize(pAig->vClockDoms) );
+    }
+    return pAig;
 }
 
 
@@ -577,13 +691,13 @@ Nwk_Obj_t * Ntl_ManExtractNwk_rec( Ntl_Man_t * p, Ntl_Net_t * pNet, Nwk_Man_t *
     Nwk_Obj_t * pNode;
     int i;
     if ( pNet->fMark )
-        return pNet->pCopy;
+        return pNet->pCopy2;
     pNet->fMark = 1;
     pNode = Nwk_ManCreateNode( pNtk, Ntl_ObjFaninNum(pNet->pDriver), (int)(long)pNet->pCopy );
     Ntl_ObjForEachFanin( pNet->pDriver, pFaninNet, i )
     {
         Ntl_ManExtractNwk_rec( p, pFaninNet, pNtk, vCover, vMemory );
-        Nwk_ObjAddFanin( pNode, pFaninNet->pCopy );
+        Nwk_ObjAddFanin( pNode, pFaninNet->pCopy2 );
     }
     if ( Ntl_ObjFaninNum(pNet->pDriver) == 0 )
         pNode->pFunc = Hop_NotCond( Hop_ManConst1(pNtk->pManHop), Kit_PlaIsConst0(pNet->pDriver->pSop) );
@@ -594,7 +708,7 @@ Nwk_Obj_t * Ntl_ManExtractNwk_rec( Ntl_Man_t * p, Ntl_Net_t * pNet, Nwk_Man_t *
         if ( Kit_PlaIsComplement(pNet->pDriver->pSop) )
             pNode->pFunc = Hop_Not(pNode->pFunc);
     }
-    return pNet->pCopy = pNode;
+    return pNet->pCopy2 = pNode;
 }
 
 /**Function*************************************************************
@@ -653,37 +767,31 @@ Nwk_Man_t * Ntl_ManExtractNwk( Ntl_Man_t * p, Aig_Man_t * pAig, Tim_Man_t * pMan
     pNtk = Nwk_ManAlloc();
     pNtk->pName = Aig_UtilStrsav( pAig->pName );
     pNtk->pSpec = Aig_UtilStrsav( pAig->pSpec );
-//    Aig_ManSetPioNumbers( pAig );
     Aig_ManForEachObj( pAig, pAnd, i )
     {
         if ( Aig_ObjIsPi(pAnd) )
         {
-//            pObj = Ntl_ModelPi( pRoot, Aig_ObjPioNum(pAnd) );
-//            pNet = Ntl_ObjFanout0(pObj);
             pNet = pAnd->pData;
             pNet->fMark = 1;
-            pNet->pCopy = Nwk_ManCreateCi( pNtk, (int)(long)pNet->pCopy ); 
+            pNet->pCopy2 = Nwk_ManCreateCi( pNtk, (int)(long)pNet->pCopy ); 
         }
         else if ( Aig_ObjIsPo(pAnd) )
         {
-//            pObj = Ntl_ModelPo( pRoot, Aig_ObjPioNum(pAnd) );
-//            pNet = Ntl_ObjFanin0(pObj);
             pNet = pAnd->pData;
             pNode = Nwk_ManCreateCo( pNtk );
             if ( (pNetSimple = Ntl_ModelFindSimpleNet( pNet )) )
             {
-                pNetSimple->pCopy = Ntl_ManExtractNwk_rec( p, pNetSimple, pNtk, vCover, vMemory ); 
-                Nwk_ObjAddFanin( pNode, pNetSimple->pCopy );
+                pNetSimple->pCopy2 = Ntl_ManExtractNwk_rec( p, pNetSimple, pNtk, vCover, vMemory ); 
+                Nwk_ObjAddFanin( pNode, pNetSimple->pCopy2 );
                 pNode->fInvert = Kit_PlaIsInv( pNet->pDriver->pSop );
             }
             else
             {
-                pNet->pCopy = Ntl_ManExtractNwk_rec( p, pNet, pNtk, vCover, vMemory ); 
-                Nwk_ObjAddFanin( pNode, pNet->pCopy );
+                pNet->pCopy2 = Ntl_ManExtractNwk_rec( p, pNet, pNtk, vCover, vMemory ); 
+                Nwk_ObjAddFanin( pNode, pNet->pCopy2 );
             }
         }
     }
-//    Aig_ManCleanPioNumbers( pAig );
     Ntl_ModelClearNets( pRoot );
     Vec_IntFree( vCover );
     Vec_IntFree( vMemory );
diff --git a/src/aig/ntl/ntlFraig.c b/src/aig/ntl/ntlFraig.c
index cdc1323b..6dce3645 100644
--- a/src/aig/ntl/ntlFraig.c
+++ b/src/aig/ntl/ntlFraig.c
@@ -117,7 +117,7 @@ Aig_Obj_t ** Ntl_ManFraigDeriveClasses( Aig_Man_t * pAig, Ntl_Man_t * pNew, Aig_
 
 /**Function*************************************************************
 
-  Synopsis    [Uses equivalences in the AID to reduce the design.]
+  Synopsis    [Uses equivalences in the AIG to reduce the design.]
 
   Description [The AIG (pAig) was extracted from the netlist and still 
   points to it (pObj->pData is the pointer to the nets in the netlist).
@@ -138,7 +138,6 @@ void Ntl_ManReduce( Ntl_Man_t * p, Aig_Man_t * pAig )
     int i, fCompl, Counter = 0;
     assert( pAig->pReprs );
     pRoot = Ntl_ManRootModel( p );
-
     Aig_ManForEachObj( pAig, pObj, i )
     {
         pObjRepr = Aig_ObjRepr( pAig, pObj );
@@ -146,6 +145,9 @@ void Ntl_ManReduce( Ntl_Man_t * p, Aig_Man_t * pAig )
             continue;
         assert( pObj != pObjRepr );
         pNet = pObj->pData;
+        // do not reduce the net if it is driven by a multi-output box
+        if ( Ntl_ObjIsBox(pNet->pDriver) && Ntl_ObjFanoutNum(pNet->pDriver) > 1 )
+            continue;
         pNetRepr = pObjRepr->pData;
         if ( pNetRepr == NULL )
         {
@@ -310,9 +312,9 @@ Ntl_Man_t * Ntl_ManScl( Ntl_Man_t * p, int fLatchConst, int fLatchEqual, int fVe
     pAig = Ntl_ManExtract( p );
     pNew = Ntl_ManInsertAig( p, pAig );
     pAigCol = Ntl_ManCollapseSeq( pNew );
+//Saig_ManDumpBlif( pAigCol, "1s.blif" );
 
     // perform SCL for the given design
-    Aig_ManSetRegNum( pAigCol, Ntl_ModelLatchNum(Ntl_ManRootModel(p)) );
     pTemp = Aig_ManScl( pAigCol, fLatchConst, fLatchEqual, fVerbose );
     Aig_ManStop( pTemp );
 
@@ -346,7 +348,6 @@ Ntl_Man_t * Ntl_ManLcorr( Ntl_Man_t * p, int nConfMax, int fVerbose )
     pAigCol = Ntl_ManCollapseSeq( pNew );
 
     // perform SCL for the given design
-    Aig_ManSetRegNum( pAigCol, Ntl_ModelLatchNum(Ntl_ManRootModel(p)) );
     pTemp = Fra_FraigLatchCorrespondence( pAigCol, 0, nConfMax, 0, fVerbose, NULL, 0 );
     Aig_ManStop( pTemp );
 
@@ -380,7 +381,6 @@ Ntl_Man_t * Ntl_ManSsw( Ntl_Man_t * p, Fra_Ssw_t * pPars )
     pAigCol = Ntl_ManCollapseSeq( pNew );
 
     // perform SCL for the given design
-    Aig_ManSetRegNum( pAigCol, Ntl_ModelLatchNum(Ntl_ManRootModel(p)) );
     pTemp = Fra_FraigInduction( pAigCol, pPars );
     Aig_ManStop( pTemp );
 
@@ -555,7 +555,6 @@ Ntl_Man_t * Ntl_ManSsw2( Ntl_Man_t * p, Fra_Ssw_t * pPars )
     Aig_Man_t * pAigRed, * pAigCol;
     // collapse the AIG
     pAigCol = Ntl_ManCollapseSeq( p );
-    Aig_ManSetRegNum( pAigCol, Ntl_ModelLatchNum(Ntl_ManRootModel(p)) );
     // transform the collapsed AIG
     pAigRed = Fra_FraigInduction( pAigCol, pPars );
     Aig_ManStop( pAigRed );
diff --git a/src/aig/ntl/ntlInsert.c b/src/aig/ntl/ntlInsert.c
index 9675eb28..52f76151 100644
--- a/src/aig/ntl/ntlInsert.c
+++ b/src/aig/ntl/ntlInsert.c
@@ -279,10 +279,9 @@ Ntl_Man_t * Ntl_ManInsertNtk( Ntl_Man_t * p, Nwk_Man_t * pNtk )
     vTruth = Vec_IntAlloc( 1 << 16 );
     vCover = Vec_IntAlloc( 1 << 16 );
     nDigits = Aig_Base10Log( Nwk_ManNodeNum(pNtk) );
-//    Nwk_ManForEachObj( pNtk, pObj, i )
+    // go through the nodes in the topological order
     vObjs = Nwk_ManDfs( pNtk );
     Vec_PtrForEachEntry( vObjs, pObj, i )
-//    Nwk_ManForEachNode( pNtk, pObj, i )
     {
         if ( !Nwk_ObjIsNode(pObj) )
             continue;
diff --git a/src/aig/ntl/ntlMan.c b/src/aig/ntl/ntlMan.c
index 0083e04c..cee0bf6c 100644
--- a/src/aig/ntl/ntlMan.c
+++ b/src/aig/ntl/ntlMan.c
@@ -48,9 +48,9 @@ Ntl_Man_t * Ntl_ManAlloc()
     p->vModels = Vec_PtrAlloc( 1000 );
     p->vCis = Vec_PtrAlloc( 1000 );
     p->vCos = Vec_PtrAlloc( 1000 );
-    p->vNodes = Vec_PtrAlloc( 1000 );
-    p->vBox1Cos = Vec_IntAlloc( 1000 );
-    p->vLatchIns = Vec_PtrAlloc( 1000 );
+    p->vVisNodes = Vec_PtrAlloc( 1000 );
+    p->vBox1Cios = Vec_IntAlloc( 1000 );
+    p->vRegClasses = Vec_IntAlloc( 1000 );
     // start the manager
     p->pMemObjs = Aig_MmFlexStart();
     p->pMemSops = Aig_MmFlexStart();
@@ -74,10 +74,6 @@ Ntl_Man_t * Ntl_ManAlloc()
 ***********************************************************************/
 void Ntl_ManCleanup( Ntl_Man_t * p )
 {
-    Vec_PtrClear( p->vCis );
-    Vec_PtrClear( p->vCos );
-    Vec_PtrClear( p->vNodes );
-    Vec_IntClear( p->vBox1Cos );
     if ( p->pAig )
     {
         Aig_ManStop( p->pAig );
@@ -190,74 +186,21 @@ 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->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 );
+    if ( p->vCis )       Vec_PtrFree( p->vCis );
+    if ( p->vCos )       Vec_PtrFree( p->vCos );
+    if ( p->vVisNodes )  Vec_PtrFree( p->vVisNodes );
+    if ( p->vRegClasses) Vec_IntFree( p->vRegClasses );
+    if ( p->vBox1Cios )  Vec_IntFree( p->vBox1Cios );
+    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 );
 }
 
 /**Function*************************************************************
 
-  Synopsis    [Returns 1 if the design is combinational.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-int Ntl_ManIsComb( Ntl_Man_t * p )          
-{ 
-    return Ntl_ModelLatchNum(Ntl_ManRootModel(p)) == 0; 
-} 
-
-/**Function*************************************************************
-
-  Synopsis    [Returns the number of registers.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-int Ntl_ManLatchNum( Ntl_Man_t * p )          
-{ 
-    return Ntl_ModelLatchNum(Ntl_ManRootModel(p)); 
-} 
-
-/**Function*************************************************************
-
-  Synopsis    [Find the model with the given name.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-Ntl_Mod_t * Ntl_ManFindModel_old( Ntl_Man_t * p, char * pName )
-{
-    Ntl_Mod_t * pModel;
-    int i;
-    Vec_PtrForEachEntry( p->vModels, pModel, i )
-        if ( !strcmp( pModel->pName, pName ) )
-            return pModel;
-    return NULL;
-}
-
-/**Function*************************************************************
-
   Synopsis    [Deallocates the netlist manager.]
 
   Description []
@@ -505,7 +448,7 @@ Ntl_Mod_t * Ntl_ModelDup( Ntl_Man_t * pManNew, Ntl_Mod_t * pModelOld )
         if ( Ntl_ObjIsLatch(pObj) )
         {
             ((Ntl_Obj_t *)pObj->pCopy)->LatchId = pObj->LatchId;
-            ((Ntl_Obj_t *)pObj->pCopy)->pClock = pObj->pClock->pCopy;
+            ((Ntl_Obj_t *)pObj->pCopy)->pClock = pObj->pClock? pObj->pClock->pCopy : NULL;
         }
         if ( Ntl_ObjIsNode(pObj) )
             ((Ntl_Obj_t *)pObj->pCopy)->pSop = Ntl_ManStoreSop( pManNew->pMemSops, pObj->pSop );
@@ -576,9 +519,17 @@ Ntl_Mod_t * Ntl_ManCreateLatchModel( Ntl_Man_t * pMan, int Init )
     pNetLo = Ntl_ModelFindOrCreateNet( pModel, "lo" );
     Ntl_ModelSetNetDriver( pObj, pNetLo );
     pObj = Ntl_ModelCreatePo( pModel, pNetLo );
+    // set timing information
+    pModel->vTimeInputs = Vec_IntAlloc( 2 );
+    Vec_IntPush( pModel->vTimeInputs, -1 );
+    Vec_IntPush( pModel->vTimeInputs, Aig_Float2Int(0.0) );        
+    pModel->vTimeOutputs = Vec_IntAlloc( 2 );
+    Vec_IntPush( pModel->vTimeOutputs, -1 );
+    Vec_IntPush( pModel->vTimeOutputs, Aig_Float2Int(0.0) );        
     return pModel;
 }
 
+
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/aig/ntl/ntlTime.c b/src/aig/ntl/ntlTime.c
index c23a4e24..53603cee 100644
--- a/src/aig/ntl/ntlTime.c
+++ b/src/aig/ntl/ntlTime.c
@@ -67,6 +67,96 @@ float * Ntl_ManCreateDelayTable( Vec_Int_t * vDelays, int nIns, int nOuts )
 
 /**Function*************************************************************
 
+  Synopsis    [Records the arrival times for the map leaves.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Ntl_ManUnpackLeafTiming( Ntl_Man_t * p, Tim_Man_t * pMan )
+{
+    Vec_Int_t * vTimes;
+    Ntl_Mod_t * pRoot;
+    Ntl_Obj_t * pObj;
+    Ntl_Net_t * pNet;
+    float dTime;
+    int i, k, v, Entry, Counter;
+    // clean the place
+    pRoot = Ntl_ManRootModel( p );
+    Ntl_ModelForEachMapLeaf( pRoot, pObj, i )
+        Ntl_ObjForEachFanout( pObj, pNet, k )
+            pNet->dTemp = 0;
+    // store the PI timing
+    vTimes = pRoot->vTimeInputs;
+    Vec_IntForEachEntry( vTimes, Entry, i )
+    {
+        dTime = Aig_Int2Float( Vec_IntEntry(vTimes,++i) );
+        if ( Entry == -1 )
+        {
+            Ntl_ModelForEachPi( pRoot, pObj, v )
+                Ntl_ObjFanout0(pObj)->dTemp = dTime;
+        }
+        else
+        {
+            pObj = Ntl_ModelPi( pRoot, Entry );
+            Ntl_ObjFanout0(pObj)->dTemp = dTime;
+        }
+    }
+    // store box timing
+    Ntl_ModelForEachMapLeaf( pRoot, pObj, k )
+    {
+        if ( !(Ntl_ObjIsBox(pObj) && Ntl_BoxIsSeq(pObj)) )
+            continue;
+        vTimes = pObj->pImplem->vTimeOutputs;
+        if ( vTimes == NULL )
+            continue;
+        Vec_IntForEachEntry( vTimes, Entry, i )
+        {
+            dTime = Aig_Int2Float( Vec_IntEntry(vTimes,++i) );
+            if ( Entry == -1 )
+            {
+                Ntl_ObjForEachFanout( pObj, pNet, v )
+                    pNet->dTemp = dTime;
+            }
+            else
+            {
+                pNet = Ntl_ObjFanout( pObj, Entry );
+                pNet->dTemp = dTime;
+            }
+        }
+    }
+    // load them into the timing manager
+    Counter = 0;
+    Ntl_ModelForEachMapLeaf( pRoot, pObj, i )
+        Ntl_ObjForEachFanout( pObj, pNet, k )
+        {
+            if ( pNet->dTemp == TIM_ETERNITY )
+                pNet->dTemp = -TIM_ETERNITY;
+            Tim_ManInitCiArrival( pMan, Counter++, pNet->dTemp );
+        }
+    assert( Counter == p->iLastCi );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Records the required times for the map leaves.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Ntl_ManUnpackRootTiming( Ntl_Man_t * p, Tim_Man_t * pMan )
+{
+}
+
+/**Function*************************************************************
+
   Synopsis    []
 
   Description []
@@ -87,7 +177,10 @@ Tim_Man_t * Ntl_ManCreateTiming( Ntl_Man_t * p )
     pRoot = Ntl_ManRootModel( p );
     // start the timing manager
     pMan = Tim_ManStart( Aig_ManPiNum(p->pAig), Aig_ManPoNum(p->pAig) );
-    // unpack the data in the arrival times
+    // unpack the timing data
+    Ntl_ManUnpackLeafTiming( p, pMan );
+//    Ntl_ManUnpackRootTiming( p, pMan );
+/*
     if ( pRoot->vTimeInputs )
     {
         Vec_IntForEachEntry( pRoot->vTimeInputs, Entry, i )
@@ -109,7 +202,8 @@ Tim_Man_t * Ntl_ManCreateTiming( Ntl_Man_t * p )
                 Tim_ManInitCoRequired( pMan, Entry, Aig_Int2Float(Vec_IntEntry(pRoot->vTimeOutputs,++i)) );
         }
     }
-    // derive timing tables
+*/
+    // derive timing tables for the whilte comb boxes
     vDelayTables = Vec_PtrAlloc( Vec_PtrSize(p->vModels) );
     Ntl_ManForEachModel( p, pModel, i )
     {
@@ -121,9 +215,11 @@ Tim_Man_t * Ntl_ManCreateTiming( Ntl_Man_t * p )
     // set up the boxes
     iBox = 0;
     curPi = p->iLastCi;
-    Ntl_ManForEachBox( p, pObj, i )
+    Vec_PtrForEachEntry( p->vVisNodes, pObj, i )
     {
-        Tim_ManCreateBoxFirst( pMan, Vec_IntEntry(p->vBox1Cos, iBox), Ntl_ObjFaninNum(pObj), curPi, Ntl_ObjFanoutNum(pObj), pObj->pImplem->pDelayTable );
+        if ( !Ntl_ObjIsBox(pObj) )
+            continue;
+        Tim_ManCreateBoxFirst( pMan, Vec_IntEntry(p->vBox1Cios, iBox), Ntl_ObjFaninNum(pObj), curPi, Ntl_ObjFanoutNum(pObj), pObj->pImplem->pDelayTable );
         curPi += Ntl_ObjFanoutNum(pObj);
         iBox++;
     }
diff --git a/src/aig/ntl/ntlUtil.c b/src/aig/ntl/ntlUtil.c
index c9ef2dc4..1fb9f1c6 100644
--- a/src/aig/ntl/ntlUtil.c
+++ b/src/aig/ntl/ntlUtil.c
@@ -350,6 +350,132 @@ void Ntl_ManTransformInitValues( Ntl_Man_t * p )
 
 /**Function*************************************************************
 
+  Synopsis    [Transforms register classes.]
+
+  Description [Returns the vector of vectors containing the numbers
+  of registers belonging to the same class. Skips classes containing
+  less than the given number of registers.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Vec_Vec_t * Ntl_ManTransformRegClasses( Ntl_Man_t * pMan, int nSizeMax, int fVerbose )
+{
+    Vec_Ptr_t * vParts;
+    Vec_Int_t * vPart;
+    int * pClassNums, nClasses;
+    int Class, ClassMax, i, k;
+    if ( Vec_IntSize(pMan->vRegClasses) == 0 )
+    {
+        printf( "Ntl_ManReportRegClasses(): Register classes are not defined.\n" );
+        return NULL;
+    }
+    // find the largest class
+    ClassMax = -1;
+    Vec_IntForEachEntry( pMan->vRegClasses, Class, k )
+    {
+        if ( Class < 0 )
+        {
+            printf( "Ntl_ManReportRegClasses(): Register class (%d) is negative.\n", Class );
+            return NULL;
+        }
+        if ( ClassMax < Class )
+            ClassMax = Class;
+    }
+    if ( ClassMax > 1000000 )
+    {
+        printf( "Ntl_ManReportRegClasses(): The largest number of a register class (%d) is too large (> 1000000).\n", ClassMax );
+        return NULL;
+    }
+    // count the number of classes
+    pClassNums = CALLOC( int, ClassMax + 1 );
+    Vec_IntForEachEntry( pMan->vRegClasses, Class, k )
+        pClassNums[Class]++;
+    // count the number of classes
+    nClasses = 0;
+    for ( i = 0; i <= ClassMax; i++ )
+        nClasses += (int)(pClassNums[i] > 0);
+    // report the classes
+    if ( fVerbose && nClasses > 1 )
+    {
+        printf( "The number of register clases = %d.\n", nClasses );
+        for ( i = 0; i <= ClassMax; i++ )
+            printf( "%d:%d  ", Class, pClassNums[i] );
+        printf( "\n" );
+    }
+    // skip if there is only one class
+    if ( nClasses == 1 )
+    {
+        free( pClassNums );
+        return NULL;
+    }
+    // create classes
+    vParts = Vec_PtrAlloc( 100 );
+    for ( i = 0; i <= ClassMax; i++ )
+    {
+        if ( pClassNums[i] < nSizeMax )
+            continue;
+        vPart = Vec_IntAlloc( pClassNums[i] );
+        Vec_IntForEachEntry( pMan->vRegClasses, Class, k )
+            if ( Class == i )
+                Vec_IntPush( vPart, k );
+        assert( Vec_IntSize(vPart) == pClassNums[i] );
+        Vec_PtrPush( vParts, vPart );
+    }
+    free( pClassNums );
+    // report the selected classes
+    if ( fVerbose )
+    {
+        printf( "The number of selected register clases = %d.\n", Vec_PtrSize(vParts) );
+        Vec_PtrForEachEntry( vParts, vPart, i )
+            printf( "%d:%d  ", i, Vec_IntSize(vPart) );
+        printf( "\n" );
+    }
+    return (Vec_Vec_t *)vParts;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Counts the number of CIs in the model.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Ntl_ManLatchNum( Ntl_Man_t * p )
+{
+    Ntl_Mod_t * pRoot;
+    Ntl_Obj_t * pObj;
+    int i, Counter = 0;
+    pRoot = Ntl_ManRootModel(p);
+    Ntl_ModelForEachBox( pRoot, pObj, i )
+        Counter += Ntl_ModelLatchNum( pObj->pImplem );
+    return Counter;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Returns 1 if the design is combinational.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Ntl_ManIsComb( Ntl_Man_t * p )          
+{ 
+    return Ntl_ManLatchNum(p) == 0; 
+} 
+
+/**Function*************************************************************
+
   Synopsis    [Counts the number of CIs in the model.]
 
   Description []
@@ -465,8 +591,8 @@ void Ntl_ModelClearNets( Ntl_Mod_t * pModel )
     int i;
     Ntl_ModelForEachNet( pModel, pNet, i )
     {
-        pNet->nVisits = 0;
-        pNet->pCopy = NULL;
+        pNet->nVisits = pNet->fMark = 0;
+        pNet->pCopy = pNet->pCopy2 = NULL;
     }
 }
 
diff --git a/src/aig/saig/saigMiter.c b/src/aig/saig/saigMiter.c
index fc721154..0c547257 100644
--- a/src/aig/saig/saigMiter.c
+++ b/src/aig/saig/saigMiter.c
@@ -70,11 +70,12 @@ Aig_Man_t * Saig_ManCreateMiter( Aig_Man_t * p1, Aig_Man_t * p2, int Oper )
     Saig_ManForEachPo( p1, pObj, i )
     {
         if ( Oper == 0 ) // XOR
-            pObj = Aig_Exor( pNew, Aig_ObjChild0Copy(pObj), Aig_ObjChild0Copy(Aig_ManPo(p2,0)) );
+            pObj = Aig_Exor( pNew, Aig_ObjChild0Copy(pObj), Aig_ObjChild0Copy(Aig_ManPo(p2,i)) );
         else if ( Oper == 1 ) // implication is PO(p1) -> PO(p2)  ...  complement is PO(p1) & !PO(p2) 
-            pObj = Aig_And( pNew, Aig_ObjChild0Copy(pObj), Aig_Not(Aig_ObjChild0Copy(Aig_ManPo(p2,0))) );
+            pObj = Aig_And( pNew, Aig_ObjChild0Copy(pObj), Aig_Not(Aig_ObjChild0Copy(Aig_ManPo(p2,i))) );
         else
             assert( 0 );
+        Aig_ObjCreatePo( pNew, pObj );
     }
     // create register inputs
     Saig_ManForEachLi( p1, pObj, i )
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index 450a245f..db8d7327 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -32,6 +32,7 @@
 #include "mfs.h"
 #include "mfx.h"
 #include "fra.h"
+#include "saig.h"
 
 ////////////////////////////////////////////////////////////////////////
 ///                        DECLARATIONS                              ///
@@ -15812,23 +15813,29 @@ int Abc_CommandAbc8Write( Abc_Frame_t * pAbc, int argc, char ** argv )
     char * pFileName;
     void * pTemp;
     int fAig;
+    int fCollapsed;
     int c;
     extern void Ioa_WriteBlif( void * p, char * pFileName );
     extern void * Ntl_ManInsertNtk( void * p, void * pNtk );
     extern void * Ntl_ManInsertAig( void * p, Aig_Man_t * pAig );
     extern void * Ntl_ManDup( void * pOld );
     extern void Ntl_ManFree( void * p );
+    extern Aig_Man_t * Ntl_ManCollapseSeq( void * p );
 
     // set defaults
     fAig = 0;
+    fCollapsed = 0;
     Extra_UtilGetoptReset();
-    while ( ( c = Extra_UtilGetopt( argc, argv, "ah" ) ) != EOF )
+    while ( ( c = Extra_UtilGetopt( argc, argv, "ach" ) ) != EOF )
     {
         switch ( c )
         {
         case 'a':
             fAig ^= 1;
             break;
+        case 'c':
+            fCollapsed ^= 1;
+            break;
         case 'h':
             goto usage;
         default:
@@ -15844,21 +15851,30 @@ int Abc_CommandAbc8Write( Abc_Frame_t * pAbc, int argc, char ** argv )
     pFileName = argv[globalUtilOptind];
     if ( fAig )
     {
-        if ( pAbc->pAbc8Aig != NULL )
+        if ( fCollapsed )
         {
-            pTemp = Ntl_ManInsertAig( pAbc->pAbc8Ntl, pAbc->pAbc8Aig );
-            if ( pTemp == NULL )
-            {
-                printf( "Abc_CommandAbc8Write(): Inserting AIG has failed.\n" );
-                return 1;
-            }
-            Ioa_WriteBlif( pTemp, pFileName );
-            Ntl_ManFree( pTemp );
+            pTemp = Ntl_ManCollapseSeq( pAbc->pAbc8Ntl );
+            Saig_ManDumpBlif( pTemp, pFileName );
+            Aig_ManStop( pTemp );
         }
         else
         {
-            printf( "There is no AIG to write.\n" );
-            return 1;
+            if ( pAbc->pAbc8Aig != NULL )
+            {
+                pTemp = Ntl_ManInsertAig( pAbc->pAbc8Ntl, pAbc->pAbc8Aig );
+                if ( pTemp == NULL )
+                {
+                    printf( "Abc_CommandAbc8Write(): Inserting AIG has failed.\n" );
+                    return 1;
+                }
+                Ioa_WriteBlif( pTemp, pFileName );
+                Ntl_ManFree( pTemp );
+            }
+            else
+            {
+                printf( "There is no AIG to write.\n" );
+                return 1;
+            }
         }
     }
     else 
@@ -15884,9 +15900,10 @@ int Abc_CommandAbc8Write( Abc_Frame_t * pAbc, int argc, char ** argv )
     return 0;
 
 usage:
-    fprintf( stdout, "usage: *w [-ah]\n" );
+    fprintf( stdout, "usage: *w [-ach]\n" );
     fprintf( stdout, "\t        write the design with whiteboxes\n" );
     fprintf( stdout, "\t-a    : toggle writing mapped network or AIG [default = %s]\n", fAig? "AIG": "mapped" );
+    fprintf( stdout, "\t-c    : toggle writing collapsed sequential AIG [default = %s]\n", fCollapsed? "yes": "no" );
     fprintf( stdout, "\t-h    : print the command usage\n");
     return 1;
 }
@@ -17810,7 +17827,7 @@ usage:
 int Abc_CommandAbc8Cec( Abc_Frame_t * pAbc, int argc, char ** argv )
 {
     Aig_Man_t * pAig1, * pAig2;
-    void * pTemp;
+    void * pTemp1, * pTemp2;
     char ** pArgvNew;
     int nArgcNew;
     int c;
@@ -17823,6 +17840,7 @@ int Abc_CommandAbc8Cec( Abc_Frame_t * pAbc, int argc, char ** argv )
     extern void Ntl_ManFree( void * p );
     extern void * Ntl_ManInsertNtk( void * p, void * pNtk );
 
+    extern void  Ntl_ManPrepareCecMans( void * pMan1, void * pMan2, Aig_Man_t ** ppAig1, Aig_Man_t ** ppAig2 );
     extern void Ntl_ManPrepareCec( char * pFileName1, char * pFileName2, Aig_Man_t ** ppMan1, Aig_Man_t ** ppMan2 );
     extern int Fra_FraigCecTop( Aig_Man_t * pMan1, Aig_Man_t * pMan2, int nConfLimit, int nPartSize, int fSmart, int fVerbose );
 
@@ -17897,25 +17915,25 @@ int Abc_CommandAbc8Cec( Abc_Frame_t * pAbc, int argc, char ** argv )
         printf( "Abc_CommandAbc8Cec(): There is no mapped network to verify.\n" );
         return 1;
     }
+//    printf( "Currently *cec works only for two designs given on command line.\n" );
 
-    printf( "Currently *cec works only for two designs given on command line.\n" );
-/*
-    // derive AIGs
-    pAig1 = Ntl_ManCollapse( pAbc->pAbc8Ntl, 0 );
-    pTemp = Ntl_ManInsertNtk( pAbc->pAbc8Ntl, pAbc->pAbc8Nwk );
-    if ( pTemp == NULL )
+    // insert the mapped network
+    pTemp1 = Ntl_ManDup( pAbc->pAbc8Ntl );
+    pTemp2 = Ntl_ManInsertNtk( pAbc->pAbc8Ntl, pAbc->pAbc8Nwk );
+    if ( pTemp2 == NULL )
     {
+        Ntl_ManFree( pTemp1 );
         printf( "Abc_CommandAbc8Cec(): Inserting the design has failed.\n" );
         return 1;
     }
-    pAig2 = Ntl_ManCollapse( pTemp, 0 );
-    Ntl_ManFree( pTemp );
-
-    // perform verification
+    Ntl_ManPrepareCecMans( pTemp1, pTemp2, &pAig1, &pAig2 );
+    Ntl_ManFree( pTemp1 );
+    Ntl_ManFree( pTemp2 );
+    if ( !pAig1 || !pAig2 )
+        return 1;
     Fra_FraigCecTop( pAig1, pAig2, nConfLimit, nPartSize, fSmart, fVerbose );
     Aig_ManStop( pAig1 );
     Aig_ManStop( pAig2 );
-*/
     return 0;
 
 usage:
@@ -17958,7 +17976,7 @@ int Abc_CommandAbc8DSec( Abc_Frame_t * pAbc, int argc, char ** argv )
 
     // set defaults
     Fra_SecSetDefaultParams( pSecPar );
-    pSecPar->nFramesMax     = 2;
+    pSecPar->nFramesMax     = 4;
     pSecPar->fPhaseAbstract = 0;
     pSecPar->fRetimeFirst   = 0;
     pSecPar->fRetimeRegs    = 0;
diff --git a/src/base/io/ioReadBlifMv.c b/src/base/io/ioReadBlifMv.c
index 68602e63..b5fb632f 100644
--- a/src/base/io/ioReadBlifMv.c
+++ b/src/base/io/ioReadBlifMv.c
@@ -180,7 +180,7 @@ Abc_Ntk_t * Io_ReadBlifMv( char * pFileName, int fBlifMv, int fCheck )
         {
             if ( !Abc_NtkCheckRead( pNtk ) )
             {
-                printf( "Io_ReadBlifMv: The network check has failed for network %s.\n", pNtk->pName );
+                printf( "Io_ReadBlifMv: The network check has failed for model %s.\n", pNtk->pName );
                 Abc_LibFree( pDesign, NULL );
                 return NULL;
             }
@@ -624,11 +624,15 @@ static void Io_MvReadPreparse( Io_MvMan_t * p )
             fprintf( stdout, "Line %d: Skipping EXDC network.\n", Io_MvGetLine(p, pCur) );
             break;
         }
+        else if ( !strncmp(pCur, "attrib", 6) )
+        {}
         else if ( !strncmp(pCur, "delay", 5) )
         {}
-        else if ( !strncmp(pCur, "input_arrival", 13) )
+        else if ( !strncmp(pCur, "input_", 6) )
+        {}
+        else if ( !strncmp(pCur, "output_", 7) )
         {}
-        else if ( !strncmp(pCur, "output_required", 15) )
+        else if ( !strncmp(pCur, "no_merge", 8) )
         {}
         else
         {
@@ -747,6 +751,14 @@ static Abc_Lib_t * Io_MvParse( Io_MvMan_t * p )
         Vec_PtrForEachEntry( pMod->vSubckts, pLine, k )
             if ( !Io_MvParseLineSubckt( pMod, pLine ) )
                 return NULL;
+
+        // allow for blackboxes without .blackbox line
+        if ( Abc_NtkLatchNum(pMod->pNtk) == 0 && Abc_NtkNodeNum(pMod->pNtk) == 0 )
+        {
+            if ( pMod->pNtk->ntkFunc == ABC_FUNC_SOP )
+                pMod->pNtk->ntkFunc = ABC_FUNC_BLACKBOX;
+        }
+
         // finalize the network
         Abc_NtkFinalizeRead( pMod->pNtk );
         // read the one-hotness lines
@@ -824,9 +836,10 @@ static int Io_MvParseLineModel( Io_MvMod_t * p, char * pLine )
         p->pNtk = Abc_NtkAlloc( ABC_NTK_NETLIST, ABC_FUNC_BLIFMV, 1 );
     else 
         p->pNtk = Abc_NtkAlloc( ABC_NTK_NETLIST, ABC_FUNC_SOP, 1 );
-    for ( pPivot = pToken = Vec_PtrEntry(vTokens, 1); *pToken; pToken++ )
-        if ( *pToken == '/' || *pToken == '\\' )
-            pPivot = pToken+1;
+//    for ( pPivot = pToken = Vec_PtrEntry(vTokens, 1); *pToken; pToken++ )
+//        if ( *pToken == '/' || *pToken == '\\' )
+//            pPivot = pToken+1;
+    pPivot = pToken = Vec_PtrEntry(vTokens, 1);
     p->pNtk->pName = Extra_UtilStrsav( pPivot );
     return 1;
 }