Version abc90714

committer: Baruch Sterin <baruchs@gmail.com>

8 files changed, 645 insertions, 40 deletions

diff --git a/src/aig/ntl/module.make b/src/aig/ntl/module.make
index 7f885a90..2af0f4e0 100644
--- a/src/aig/ntl/module.make
+++ b/src/aig/ntl/module.make
@@ -6,6 +6,7 @@ SRC +=    src/aig/ntl/ntlCheck.c \
     src/aig/ntl/ntlInsert.c \
     src/aig/ntl/ntlMan.c \
     src/aig/ntl/ntlMap.c \
+    src/aig/ntl/ntlNames.c \
     src/aig/ntl/ntlObj.c \
     src/aig/ntl/ntlReadBlif.c \
     src/aig/ntl/ntlSweep.c \
diff --git a/src/aig/ntl/ntl.h b/src/aig/ntl/ntl.h
index a82b4d6c..0955214e 100644
--- a/src/aig/ntl/ntl.h
+++ b/src/aig/ntl/ntl.h
@@ -76,6 +76,7 @@ struct Ntl_Man_t_
     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
+    Vec_Int_t *        vRstClasses;    // the classes of reset registers in the AIG
     Aig_Man_t *        pAig;           // the extracted AIG
     Tim_Man_t *        pManTime;       // the timing manager
     int                iLastCi;        // the last true CI
@@ -83,6 +84,7 @@ struct Ntl_Man_t_
     void (*pNalF)(void *);             // additional data
     void (*pNalD)(void *,void *);      // additional data
     void (*pNalW)(void *,void *);      // additional data
+    void (*pNalR)(void *);             // additional data
     // hashing names into models
     Ntl_Mod_t **       pModTable;      // the hash table of names into models
     int                nModTableSize;  // the allocated table size
@@ -112,6 +114,9 @@ struct Ntl_Mod_t_
     // clocks of the model
     Vec_Ptr_t *        vClocks;        // the clock signals
     Vec_Vec_t *        vClockFlops;    // the flops of each clock
+    // resets of the model
+    Vec_Ptr_t *        vResets;        // the reset signals
+    Vec_Vec_t *        vResetFlops;    // the ASYNC flops of each reset
     // delay information
     Vec_Int_t *        vDelays;
     Vec_Int_t *        vTimeInputs;
@@ -121,7 +126,7 @@ struct Ntl_Mod_t_
     Ntl_Mod_t *        pNext;
     void *             pCopy;
     int                nUsed, nRems;
-}; 
+};  
 
 struct Ntl_Reg_t_
 {
@@ -139,6 +144,7 @@ struct Ntl_Obj_t_
     unsigned           Id     : 28;    // object ID
     int                nFanins;        // the number of fanins
     int                nFanouts;       // the number of fanouts
+    int                Reset;          // reset of the flop
     union {                            // functionality
         Ntl_Mod_t *    pImplem;        // model (for boxes)
         char *         pSop;           // SOP (for logic nodes)
@@ -162,9 +168,10 @@ struct Ntl_Net_t_
         int            iTemp;          // other data
     };
     Ntl_Obj_t *        pDriver;        // driver of the net
-    unsigned           NetId     : 28; // unique ID of the net
+    unsigned           NetId     : 27; // unique ID of the net
     unsigned           nVisits   :  2; // the number of times the net is visted
     unsigned           fMark     :  1; // temporary mark
+    unsigned           fMark2    :  1; // temporary mark
     unsigned           fFixed    :  1; // the fixed net
     char               pName[0];       // the name of this net
 };
@@ -329,11 +336,18 @@ extern ABC_DLL void            Ntl_ManFree( Ntl_Man_t * p );
 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 int             Ntl_ManCompareClockClasses( Vec_Ptr_t ** pp1, Vec_Ptr_t ** pp2 );
+extern ABC_DLL void            Ntl_ManPrintClocks( Ntl_Man_t * p );
+extern ABC_DLL void            Ntl_ManPrintResets( 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 );
+extern ABC_DLL int             Ntl_ModelCountLut0( Ntl_Mod_t * p );
+extern ABC_DLL int             Ntl_ModelCountLut1( Ntl_Mod_t * p );
+extern ABC_DLL int             Ntl_ModelCountBuf( Ntl_Mod_t * p );
+extern ABC_DLL int             Ntl_ModelCountInv( Ntl_Mod_t * p );
 /*=== 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 );
@@ -350,6 +364,7 @@ extern ABC_DLL Ntl_Obj_t *     Ntl_ModelCreatePiWithName( Ntl_Mod_t * pModel, ch
 extern ABC_DLL char *          Ntl_ManStoreName( Ntl_Man_t * p, char * pName );
 extern ABC_DLL char *          Ntl_ManStoreSop( Aig_MmFlex_t * pMan, char * pSop );
 extern ABC_DLL char *          Ntl_ManStoreFileName( Ntl_Man_t * p, char * pFileName );
+extern ABC_DLL int             Ntl_ManObjWhichFanout( Ntl_Obj_t * pNode, Ntl_Net_t * pFanout );
 /*=== ntlSweep.c ==========================================================*/
 extern ABC_DLL int             Ntl_ManSweep( Ntl_Man_t * p, int fVerbose );
 /*=== ntlTable.c ==========================================================*/
@@ -374,7 +389,6 @@ extern ABC_DLL Ntl_Man_t *     Ioa_ReadBlif( char * pFileName, int fCheck );
 extern ABC_DLL void            Ioa_WriteBlif( Ntl_Man_t * p, char * pFileName );
 extern ABC_DLL void            Ioa_WriteBlifLogic( Nwk_Man_t * pNtk, Ntl_Man_t * p, char * pFileName );
 /*=== ntlUtil.c ==========================================================*/
-extern ABC_DLL int             Ntl_ModelCountLut1( Ntl_Mod_t * pRoot );
 extern ABC_DLL int             Ntl_ModelGetFaninMax( Ntl_Mod_t * pRoot );
 extern ABC_DLL Ntl_Net_t *     Ntl_ModelFindSimpleNet( Ntl_Net_t * pNetCo );
 extern ABC_DLL int             Ntl_ManCountSimpleCoDrivers( Ntl_Man_t * p );
diff --git a/src/aig/ntl/ntlExtract.c b/src/aig/ntl/ntlExtract.c
index 6afeba26..55a961df 100644
--- a/src/aig/ntl/ntlExtract.c
+++ b/src/aig/ntl/ntlExtract.c
@@ -371,6 +371,7 @@ int Ntl_ManCollapseBoxSeq1_rec( Ntl_Man_t * p, Ntl_Obj_t * pBox, int fSeq )
         pNet->nVisits = 2;
         // remember the class of this register
         Vec_IntPush( p->vRegClasses, p->pNal ? pBox->iTemp : pObj->LatchId.regClass );
+        Vec_IntPush( p->vRstClasses, p->pNal ? pBox->Reset : -1 );
     }
     // compute AIG for the internal nodes
     Ntl_ModelForEachPo( pModel, pObj, i )
@@ -505,6 +506,7 @@ Aig_Man_t * Ntl_ManCollapse( Ntl_Man_t * p, int fSeq )
     assert( Vec_PtrSize(p->vCos) != 0 );
     Vec_IntClear( p->vBox1Cios );
     Vec_IntClear( p->vRegClasses );
+    Vec_IntClear( p->vRstClasses );
     // clear net visited flags
     pRoot = Ntl_ManRootModel(p);
     assert( Ntl_ModelLatchNum(pRoot) == 0 );
@@ -797,6 +799,7 @@ Nwk_Man_t * Ntl_ManExtractNwk( Ntl_Man_t * p, Aig_Man_t * pAig, Tim_Man_t * pMan
             {
                 pNet->pCopy2 = Ntl_ManExtractNwk_rec( p, pNet, pNtk, vCover, vMemory ); 
                 Nwk_ObjAddFanin( pNode, pNet->pCopy2 );
+                pNode->fInvert = (Nwk_ObjFanin0(pNode)->pFunc == Hop_ManConst0(pNtk->pManHop)); // fixed on June 7, 2009
             }
         }
     }
diff --git a/src/aig/ntl/ntlFraig.c b/src/aig/ntl/ntlFraig.c
index e98a3b46..64af98f4 100644
--- a/src/aig/ntl/ntlFraig.c
+++ b/src/aig/ntl/ntlFraig.c
@@ -423,6 +423,171 @@ Ntl_Man_t * Ntl_ManFraig( Ntl_Man_t * p, int nPartSize, int nConfLimit, int nLev
 
 /**Function*************************************************************
 
+  Synopsis    [Counts the number of resets.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Ntl_ManAigCountResets( Ntl_Man_t * pNtl )
+{
+    Ntl_Mod_t * pModel = Ntl_ManRootModel(pNtl);
+    Ntl_Obj_t * pBox;
+    int i, Counter = -1;
+    Ntl_ModelForEachObj( pModel, pBox, i )
+        Counter = ABC_MAX( Counter, pBox->Reset );
+    return Counter + 1;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Transforms sequential AIG to allow for async reset.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Aig_Man_t * Ntl_ManAigToRst( Ntl_Man_t * pNtl, Aig_Man_t * p )
+{
+    Ntl_Mod_t * pModel = Ntl_ManRootModel(pNtl);
+    Aig_Man_t * pNew;
+    Aig_Obj_t * pObj;
+    int i, iRegNum, iRstNum, Counter = 0;
+    int nResets = Ntl_ManAigCountResets( pNtl );
+    assert( pNtl->pNal != NULL );
+    assert( Aig_ManRegNum(p) > 0 );
+    assert( Vec_IntSize(pNtl->vRstClasses) == Aig_ManRegNum(p) );
+//printf( "Number of resets before synthesis = %d.\n", nResets );
+    // create the PIs
+    Aig_ManCleanData( p );
+    Aig_ManSetPioNumbers( p );
+    // create the new manager
+    pNew = Aig_ManStart( Aig_ManObjNumMax(p) );
+    pNew->pName = Aig_UtilStrsav( p->pName );
+    pNew->pSpec = Aig_UtilStrsav( p->pSpec );
+    // create special PIs
+    for ( i = 0; i < nResets; i++ )
+        Aig_ObjCreatePi( pNew );
+    // duplicate internal nodes
+    Aig_ManForEachPi( p, pObj, i )
+        pObj->pData = Aig_ObjCreatePi( pNew );
+    Aig_ManForEachObj( p, pObj, i )
+    {
+        if ( Aig_ObjIsNode(pObj) )
+            pObj->pData = Aig_And( pNew, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) );
+        else if ( Aig_ObjIsPo(pObj) )
+            pObj->pData = Aig_ObjCreatePo( pNew, Aig_ObjChild0Copy(pObj) );
+        else if ( Aig_ObjIsPi(pObj) )
+        {
+//            pObj->pData = Aig_ObjCreatePi( pNew );
+            iRegNum = Aig_ObjPioNum(pObj) - (Aig_ManPiNum(p) - Aig_ManRegNum(p));
+            if ( iRegNum < 0 )
+                continue;
+            iRstNum = Vec_IntEntry(pNtl->vRstClasses, iRegNum);
+            if ( iRstNum < 0 )
+                continue;
+            assert( iRstNum < nResets );
+            pObj->pData = Aig_And( pNew, pObj->pData, Aig_ManPi(pNew, iRstNum) ); // could be NOT(pi)
+            Counter++;
+        }
+        else if ( Aig_ObjIsConst1(pObj) )
+            pObj->pData = Aig_ManConst1(pNew);
+        else
+            assert( 0 );
+    }
+    assert( Aig_ManNodeNum(p) + Counter == Aig_ManNodeNum(pNew) );
+    if ( (Counter = Aig_ManCleanup( pNew )) )
+        printf( "Aig_ManDupOrdered(): Cleanup after AIG duplication removed %d nodes.\n", Counter );
+    Aig_ManSetRegNum( pNew, Aig_ManRegNum(p) );
+    return pNew;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Remaps equivalence classes from the new nodes to the old ones.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Ntl_ManRemapClassesLcorr( Ntl_Man_t * pNtl, Aig_Man_t * p, Aig_Man_t * pNew )
+{
+    Ntl_Mod_t * pModel = Ntl_ManRootModel(pNtl);
+    Aig_Obj_t * pObj, * pObjRepr, * pObjNew, * pObjNewRepr;
+    int i, nResets = Ntl_ManAigCountResets( pNtl );
+    int nTruePis = Aig_ManPiNum(p) - Aig_ManRegNum(p);
+    assert( pNew->pReprs != NULL );
+    assert( nResets == Aig_ManPiNum(pNew) - Aig_ManPiNum(p) );
+    Aig_ManReprStart( p, Aig_ManObjNumMax(p) );
+    Aig_ManForEachLoSeq( pNew, pObjNew, i )
+    {
+        pObj = Aig_ManPi( p, i - nResets );
+        pObjNewRepr = pNew->pReprs[pObjNew->Id];
+        if ( pObjNewRepr == NULL )
+            continue;
+        if ( pObjNewRepr == Aig_ManConst1(pNew) )
+        {
+            Aig_ObjCreateRepr( p, Aig_ManConst1(p), pObj );
+            continue;
+        }
+        assert( Aig_ObjIsPi(pObjNewRepr) );
+        // find the corresponding representative node
+        pObjRepr = Aig_ManPi( p, Aig_ObjPioNum(pObjNewRepr) - nResets );
+        // if they belong to different domains, quit
+        if ( Vec_IntEntry( pNtl->vRstClasses, Aig_ObjPioNum(pObj) - nTruePis ) != 
+             Vec_IntEntry( pNtl->vRstClasses, Aig_ObjPioNum(pObjRepr) - nTruePis ) )
+            continue;
+        Aig_ObjCreateRepr( p, pObjRepr, pObj );
+    }
+} 
+
+/**Function*************************************************************
+
+  Synopsis    [Remaps equivalence classes from the new nodes to the old ones.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Ntl_ManRemapClassesScorr( Ntl_Man_t * pNtl, Aig_Man_t * p, Aig_Man_t * pNew )
+{
+    Aig_Obj_t * pObj, * pObjRepr, * pObjNew, * pObjNewRepr;
+    int i;
+    // map things back
+    Aig_ManForEachObj( p, pObj, i )
+    {
+        pObjNew = pObj->pData;
+        assert( pObjNew != NULL && !Aig_IsComplement(pObjNew) );
+        pObjNew->pData = pObj;
+    }
+    // remap the classes
+    Aig_ManForEachObj( pNew, pObjNew, i )
+    {
+        pObjNewRepr = pNew->pReprs[pObjNew->Id];
+        if ( pObjNewRepr == NULL )
+            continue;
+        pObj = pObjNew->pData;
+        pObjRepr = pObjNewRepr->pData;    
+        assert( Aig_ObjId(pObjRepr) < Aig_ObjId(pObj) );
+        Aig_ObjCreateRepr( p, pObjRepr, pObj );
+    }
+}
+
+
+/**Function*************************************************************
+
   Synopsis    [Performs sequential cleanup.]
 
   Description []
@@ -451,9 +616,21 @@ Ntl_Man_t * Ntl_ManScl( Ntl_Man_t * p, int fLatchConst, int fLatchEqual, int fVe
 //Ntl_ManPrintStats( pNew );
 //Aig_ManPrintStats( pAigCol );
 
-    // perform SCL for the given design
-    pTemp = Aig_ManScl( pAigCol, fLatchConst, fLatchEqual, fVerbose );
-    Aig_ManStop( pTemp );
+    // perform SCL
+    if ( p->pNal )
+    {
+        Aig_Man_t * pAigRst;
+        pAigRst = Ntl_ManAigToRst( pNew, pAigCol );
+        pTemp = Aig_ManScl( pAigRst, fLatchConst, fLatchEqual, fVerbose );
+        Aig_ManStop( pTemp );
+        Ntl_ManRemapClassesLcorr( pNew, pAigCol, pAigRst );
+        Aig_ManStop( pAigRst );
+    }
+    else
+    {
+        pTemp = Aig_ManScl( pAigCol, fLatchConst, fLatchEqual, fVerbose );
+        Aig_ManStop( pTemp );
+    }
 
     // finalize the transformation
     pNew = Ntl_ManFinalize( pAux = pNew, pAig, pAigCol, fVerbose );
@@ -493,11 +670,23 @@ Ntl_Man_t * Ntl_ManLcorr( Ntl_Man_t * p, int nConfMax, int fScorrGia, int fUseCS
         return pNew;
     }
 
-    // perform LCORR for the given design
+    // perform LCORR
     pPars->fScorrGia = fScorrGia;
     pPars->fUseCSat  = fUseCSat;
-    pTemp = Ssw_LatchCorrespondence( pAigCol, pPars );
-    Aig_ManStop( pTemp );
+    if ( p->pNal )
+    {
+        Aig_Man_t * pAigRst;
+        pAigRst = Ntl_ManAigToRst( pNew, pAigCol );
+        pTemp = Ssw_LatchCorrespondence( pAigRst, pPars );
+        Aig_ManStop( pTemp );
+        Ntl_ManRemapClassesLcorr( pNew, pAigCol, pAigRst );
+        Aig_ManStop( pAigRst );
+    }
+    else
+    {
+        pTemp = Ssw_LatchCorrespondence( pAigCol, pPars );
+        Aig_ManStop( pTemp );
+    }
 
     // finalize the transformation
     pNew = Ntl_ManFinalize( pAux = pNew, pAig, pAigCol, fVerbose );
@@ -522,6 +711,7 @@ Ntl_Man_t * Ntl_ManSsw( Ntl_Man_t * p, Fra_Ssw_t * pPars )
 {
     Ntl_Man_t * pNew, * pAux;
     Aig_Man_t * pAig, * pAigCol, * pTemp;
+    assert( 0 ); // not updated for nal
 
     // collapse the AIG
     pAig = Ntl_ManExtract( p );
@@ -571,9 +761,21 @@ Ntl_Man_t * Ntl_ManScorr( Ntl_Man_t * p, Ssw_Pars_t * pPars )
         return pNew;
     }
 
-    // perform SCL for the given design
-    pTemp = Ssw_SignalCorrespondence( pAigCol, pPars );
-    Aig_ManStop( pTemp );
+    // perform SCL
+    if ( p->pNal )
+    {
+        Aig_Man_t * pAigRst;
+        pAigRst = Ntl_ManAigToRst( pNew, pAigCol );
+        pTemp = Ssw_SignalCorrespondence( pAigRst, pPars );
+        Aig_ManStop( pTemp );
+        Ntl_ManRemapClassesLcorr( pNew, pAigCol, pAigRst );
+        Aig_ManStop( pAigRst );
+    }
+    else
+    {
+        pTemp = Ssw_SignalCorrespondence( pAigCol, pPars );
+        Aig_ManStop( pTemp );
+    }
 
     // finalize the transformation
     pNew = Ntl_ManFinalize( pAux = pNew, pAig, pAigCol, pPars->fVerbose );
diff --git a/src/aig/ntl/ntlInsert.c b/src/aig/ntl/ntlInsert.c
index eb967bdc..750eb8f7 100644
--- a/src/aig/ntl/ntlInsert.c
+++ b/src/aig/ntl/ntlInsert.c
@@ -290,6 +290,190 @@ void Ntl_ManFindDriver( Ntl_Man_t * p, char * pName )
   SeeAlso     []
 
 ***********************************************************************/
+Ntl_Man_t * Ntl_ManInsertNtk2( Ntl_Man_t * p, Nwk_Man_t * pNtk )
+{
+    int fWriteConstants = 1;
+    char Buffer[1000]; 
+    Vec_Ptr_t * vObjs;
+    Vec_Int_t * vTruth;
+    Vec_Int_t * vCover;
+    Ntl_Mod_t * pRoot;
+    Ntl_Obj_t * pNode;
+    Ntl_Net_t * pNet, * pNetCo;
+    Nwk_Obj_t * pObj, * pFanin;
+    int i, k, nDigits;
+    unsigned * pTruth;
+    assert( Vec_PtrSize(p->vCis) == Nwk_ManCiNum(pNtk) );
+    assert( Vec_PtrSize(p->vCos) == Nwk_ManCoNum(pNtk) );
+    p = Ntl_ManStartFrom( p );
+    pRoot = Ntl_ManRootModel( p );
+    assert( Ntl_ModelNodeNum(pRoot) == 0 );
+    // set the correspondence between the PI/PO nodes
+    Ntl_ManForEachCiNet( p, pNet, i )
+        Nwk_ManCi( pNtk, i )->pCopy = pNet;
+    // create a new node for each LUT
+    vTruth  = Vec_IntAlloc( 1 << 16 );
+    vCover  = Vec_IntAlloc( 1 << 16 );
+    nDigits = Aig_Base10Log( Nwk_ManNodeNum(pNtk) );
+    // go through the nodes in the topological order
+    vObjs = Nwk_ManDfs( pNtk );
+    Vec_PtrForEachEntry( vObjs, pObj, i )
+    {
+        if ( !Nwk_ObjIsNode(pObj) )
+            continue;
+/*
+        if ( fWriteConstants && Nwk_ObjFaninNum(pObj) == 0 )
+        {
+            pObj->pCopy = NULL;
+            continue;
+        }
+*/
+        // skip constant drivers if they only drive COs
+        if ( fWriteConstants && Nwk_ObjFaninNum(pObj) == 0 )
+        {
+            Nwk_Obj_t * pFanout;
+            int i;
+            Nwk_ObjForEachFanout( pObj, pFanout, i )
+                if ( Nwk_ObjIsNode(pFanout) )
+                    break;
+            if ( i == Nwk_ObjFanoutNum(pObj) )
+            {
+                pObj->pCopy = NULL;
+                continue;
+            }
+        }
+
+        pNode = Ntl_ModelCreateNode( pRoot, Nwk_ObjFaninNum(pObj) );
+        pTruth = Hop_ManConvertAigToTruth( pNtk->pManHop, Hop_Regular(pObj->pFunc), Nwk_ObjFaninNum(pObj), vTruth, 0 );
+        if ( Hop_IsComplement(pObj->pFunc) )
+            Kit_TruthNot( pTruth, pTruth, Nwk_ObjFaninNum(pObj) );
+        if ( !Kit_TruthIsConst0(pTruth, Nwk_ObjFaninNum(pObj)) && !Kit_TruthIsConst1(pTruth, Nwk_ObjFaninNum(pObj)) )
+        {
+            Nwk_ObjForEachFanin( pObj, pFanin, k )
+            {
+                pNet = pFanin->pCopy;
+                if ( pNet == NULL )
+                {
+                    printf( "Ntl_ManInsertNtk(): Internal error: Net not found.\n" );
+                    return 0;
+                }
+                Ntl_ObjSetFanin( pNode, pNet, k );
+            }
+        }
+        else if ( Kit_TruthIsConst0(pTruth, Nwk_ObjFaninNum(pObj)) )
+        {
+            pObj->pFunc = Hop_ManConst0(pNtk->pManHop);
+            pNode->nFanins = 0;
+        }
+        else if ( Kit_TruthIsConst1(pTruth, Nwk_ObjFaninNum(pObj)) )
+        {
+            pObj->pFunc = Hop_ManConst1(pNtk->pManHop);
+            pNode->nFanins = 0;
+        }
+        pNode->pSop = Kit_PlaFromTruth( p->pMemSops, pTruth, Nwk_ObjFaninNum(pObj), vCover );
+        sprintf( Buffer, "lut%0*d", nDigits, i );
+        if ( (pNet = Ntl_ModelFindNet( pRoot, Buffer )) )
+        {
+            printf( "Ntl_ManInsertNtk(): Internal error: Intermediate net name is not unique.\n" );
+            return 0;
+        }
+        pNet = Ntl_ModelFindOrCreateNet( pRoot, Buffer );
+        if ( !Ntl_ModelSetNetDriver( pNode, pNet ) )
+        {
+            printf( "Ntl_ManInsertNtk(): Internal error: Net has more than one fanin.\n" );
+            return 0;
+        }
+        pObj->pCopy = pNet;
+    }
+    Vec_PtrFree( vObjs );
+    Vec_IntFree( vCover );
+    Vec_IntFree( vTruth );
+    // mark the nets driving special boxes
+    if ( p->pNalR )
+        p->pNalR( p );
+    // mark CIs and outputs of the registers
+    Ntl_ManForEachCiNet( p, pNetCo, i )
+        pNetCo->fMark = 1;
+    // update the CO pointers
+    Ntl_ManForEachCoNet( p, pNetCo, i )
+    {
+        if ( pNetCo->fMark )
+            continue; 
+        pNetCo->fMark = 1;
+        // get the corresponding PO and its driver
+        pObj = Nwk_ManCo( pNtk, i );
+        pFanin = Nwk_ObjFanin0( pObj );
+        // get the net driving this PO
+        pNet = pFanin->pCopy; 
+        if ( pNet == NULL ) // constant net
+        {
+            assert( fWriteConstants );
+            pNode = Ntl_ModelCreateNode( pRoot, 0 );
+            pNode->pSop = pObj->fInvert? Ntl_ManStoreSop( p->pMemSops, " 0\n" ) : Ntl_ManStoreSop( p->pMemSops, " 1\n" );
+        }
+        else 
+        if ( Nwk_ObjFanoutNum(pFanin) == 1 && Ntl_ObjIsNode(pNet->pDriver) && !pNet->fMark2 )
+        {
+            pNode = pNet->pDriver;
+            if ( !Ntl_ModelClearNetDriver( pNode, pNet ) )
+            {
+                printf( "Ntl_ManInsertNtk(): Internal error! Net already has no driver.\n" );
+                return NULL;
+            }
+            // remove this net 
+            Ntl_ModelDeleteNet( pRoot, pNet );
+            Vec_PtrWriteEntry( pRoot->vNets, pNet->NetId, NULL );
+            // update node's function
+            if ( pObj->fInvert )
+                Kit_PlaComplement( pNode->pSop );
+        }
+        else
+        {
+/*
+            if ( fWriteConstants && Ntl_ObjFaninNum(pNet->pDriver) == 0 )
+            {
+                pNode = Ntl_ModelCreateNode( pRoot, 0 );
+                pNode->pSop = pObj->fInvert? Ntl_ManStoreSop( p->pMemSops, " 0\n" ) : Ntl_ManStoreSop( p->pMemSops, " 1\n" );
+            }
+            else
+*/
+            {
+//                assert( Ntl_ObjFaninNum(pNet->pDriver) != 0 );
+                pNode = Ntl_ModelCreateNode( pRoot, 1 );
+                pNode->pSop = pObj->fInvert? Ntl_ManStoreSop( p->pMemSops, "0 1\n" ) : Ntl_ManStoreSop( p->pMemSops, "1 1\n" );
+                Ntl_ObjSetFanin( pNode, pNet, 0 );
+            }
+        }
+        // update the CO driver net
+        assert( pNetCo->pDriver == NULL );
+        if ( !Ntl_ModelSetNetDriver( pNode, pNetCo ) )
+        {
+            printf( "Ntl_ManInsertNtk(): Internal error: PO net has more than one fanin.\n" );
+            return NULL;
+        }
+    }
+    // clean CI/CO marks
+    Ntl_ManUnmarkCiCoNets( p );
+    if ( !Ntl_ManCheck( p ) )
+    {
+        printf( "Ntl_ManInsertNtk: The check has failed for design %s.\n", p->pName );
+        return NULL;
+    }
+    return p;
+}
+
+
+/**Function*************************************************************
+
+  Synopsis    [Inserts the given mapping into the netlist.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
 Ntl_Man_t * Ntl_ManInsertNtk( Ntl_Man_t * p, Nwk_Man_t * pNtk )
 {
     char Buffer[1000]; 
@@ -418,7 +602,6 @@ Ntl_Man_t * Ntl_ManInsertNtk( Ntl_Man_t * p, Nwk_Man_t * pNtk )
     return p;
 }
 
-
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/aig/ntl/ntlMan.c b/src/aig/ntl/ntlMan.c
index da7e2317..a95c2352 100644
--- a/src/aig/ntl/ntlMan.c
+++ b/src/aig/ntl/ntlMan.c
@@ -51,6 +51,7 @@ Ntl_Man_t * Ntl_ManAlloc()
     p->vVisNodes = Vec_PtrAlloc( 1000 );
     p->vBox1Cios = Vec_IntAlloc( 1000 );
     p->vRegClasses = Vec_IntAlloc( 1000 );
+    p->vRstClasses = Vec_IntAlloc( 1000 );
     // start the manager
     p->pMemObjs = Aig_MmFlexStart();
     p->pMemSops = Aig_MmFlexStart();
@@ -123,6 +124,7 @@ Ntl_Man_t * Ntl_ManStartFrom( Ntl_Man_t * pOld )
         {
             ((Ntl_Obj_t *)pBox->pCopy)->pImplem = pBox->pImplem->pCopy;
             ((Ntl_Obj_t *)pBox->pCopy)->iTemp = pBox->iTemp;
+            ((Ntl_Obj_t *)pBox->pCopy)->Reset = pBox->Reset;
         }
     Ntl_ManForEachCiNet( pOld, pNet, i )
         Vec_PtrPush( pNew->vCis, pNet->pCopy );
@@ -197,6 +199,7 @@ void Ntl_ManFree( Ntl_Man_t * p )
     if ( p->vCos )       Vec_PtrFree( p->vCos );
     if ( p->vVisNodes )  Vec_PtrFree( p->vVisNodes );
     if ( p->vRegClasses) Vec_IntFree( p->vRegClasses );
+    if ( p->vRstClasses) Vec_IntFree( p->vRstClasses );
     if ( p->vBox1Cios )  Vec_IntFree( p->vBox1Cios );
     if ( p->pMemObjs )   Aig_MmFlexStop( p->pMemObjs, 0 );
     if ( p->pMemSops )   Aig_MmFlexStop( p->pMemSops, 0 );
@@ -294,14 +297,14 @@ void Nwk_ManPrintStatsShort( Ntl_Man_t * p, Aig_Man_t * pAig, Nwk_Man_t * pNtk )
   SeeAlso     []
 
 ***********************************************************************/
-int Nwk_ManStatsRegs( Ntl_Man_t * p )
+int Ntl_ManStatsRegs( 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 )
-        if ( strcmp(pObj->pImplem->pName, "dff") == 0 )
+        if ( strcmp(pObj->pImplem->pName, "m_dff") == 0 )
             Counter++;
     return Counter;
 }
@@ -317,6 +320,22 @@ int Nwk_ManStatsRegs( Ntl_Man_t * p )
   SeeAlso     []
 
 ***********************************************************************/
+int Ntl_ManStatsLuts( Ntl_Man_t * p )
+{
+    return Ntl_ModelLut1Num( Ntl_ManRootModel(p) ) + Ntl_ModelNodeNum( Ntl_ManRootModel(p) );
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
 int Nwk_ManStatsLuts( Nwk_Man_t * pNtk )
 {
     return pNtk ? Nwk_ManNodeNum(pNtk) : -1;
@@ -353,13 +372,13 @@ int Nwk_ManStatsLevs( Nwk_Man_t * pNtk )
 void Nwk_ManPrintStatsUpdate( Ntl_Man_t * p, Aig_Man_t * pAig, Nwk_Man_t * pNtk,
      int nRegInit, int nLutInit, int nLevInit, int Time )
 {
-    printf( "FF =%7d (%4.1f%%)  ",  Nwk_ManStatsRegs(p),    100.0*(nRegInit-Nwk_ManStatsRegs(p))/nRegInit );
+    printf( "FF =%7d (%5.1f%%)  ",  Ntl_ManStatsRegs(p),    nRegInit ? (100.0*(nRegInit-Ntl_ManStatsRegs(p))/nRegInit) : 0.0 );
     if ( pNtk == NULL )
-        printf( "Mapping is not available.                  " );
+        printf( "Mapping is not available.                    " );
     else
     {
-        printf( "Lut =%7d (%4.1f%%)  ", Nwk_ManStatsLuts(pNtk), 100.0*(nLutInit-Nwk_ManStatsLuts(pNtk))/nLutInit );
-        printf( "Lev =%4d (%4.1f%%)    ", Nwk_ManStatsLevs(pNtk), 100.0*(nLevInit-Nwk_ManStatsLevs(pNtk))/nLevInit );
+        printf( "Lut =%7d (%5.1f%%)  ", Ntl_ManStatsLuts(p), nLutInit ? (100.0*(nLutInit-Ntl_ManStatsLuts(p))/nLutInit) : 0.0 );
+        printf( "Lev =%4d (%5.1f%%)    ", Nwk_ManStatsLevs(pNtk), nLevInit ? (100.0*(nLevInit-Nwk_ManStatsLevs(pNtk))/nLevInit) : 0.0 );
     }
     ABC_PRT( "Time", clock() - Time );
 }
@@ -461,6 +480,101 @@ void Ntl_ManPrintTypes( Ntl_Man_t * p )
 
 /**Function*************************************************************
 
+  Synopsis    [Procedure used for sorting the nodes in decreasing order of levels.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Ntl_ManCompareClockClasses( Vec_Ptr_t ** pp1, Vec_Ptr_t ** pp2 )
+{
+    int Diff = Vec_PtrSize(*pp1) - Vec_PtrSize(*pp2);
+    if ( Diff > 0 )
+        return -1;
+    if ( Diff < 0 ) 
+        return 1;
+    return 0; 
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Saves the model type.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Ntl_ManPrintClocks( Ntl_Man_t * p )
+{
+    Vec_Ptr_t * vFlops;
+    Ntl_Net_t * pNet;
+    Ntl_Mod_t * pModel;
+    int i;
+    pModel = Ntl_ManRootModel( p );
+    if ( Ntl_ModelBoxNum(pModel) == 0 )
+        return;
+    if ( pModel->vClockFlops )
+    {
+        printf( "CLOCK STATISTICS:\n" );
+        Vec_VecForEachLevel( pModel->vClockFlops, vFlops, i )
+        {
+            pNet = Vec_PtrEntry( pModel->vClocks, i );
+            printf( "Clock %2d :  Name = %30s   Flops = %6d.\n", i+1, pNet->pName, Vec_PtrSize(vFlops) );
+            if ( i == 10 )
+            {
+                printf( "Skipping... (the total is %d)\n", Vec_VecSize(pModel->vClockFlops) );
+                break;
+            }
+        }
+    }
+//    printf( "\n" );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Saves the model type.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Ntl_ManPrintResets( Ntl_Man_t * p )
+{
+    Vec_Ptr_t * vFlops;
+    Ntl_Net_t * pNet;
+    Ntl_Mod_t * pModel;
+    int i;
+    pModel = Ntl_ManRootModel( p );
+    if ( Ntl_ModelBoxNum(pModel) == 0 )
+        return;
+    if ( pModel->vResetFlops )
+    {
+        printf( "RESET STATISTICS:\n" );
+        Vec_VecForEachLevel( pModel->vResetFlops, vFlops, i )
+        {
+            pNet = Vec_PtrEntry( pModel->vResets, i );
+            printf( "Reset %2d :  Name = %30s   Flops = %6d.\n", i+1, pNet->pName, Vec_PtrSize(vFlops) );
+            if ( i == 10 )
+            {
+                printf( "Skipping... (the total is %d)\n", Vec_VecSize(pModel->vResetFlops) );
+                break;
+            }
+        }
+    }
+//    printf( "\n" );
+}
+
+/**Function*************************************************************
+
   Synopsis    [Allocates the model.]
 
   Description []
@@ -643,6 +757,8 @@ void Ntl_ModelFree( Ntl_Mod_t * p )
     if ( p->vDelays )       Vec_IntFree( p->vDelays );
     if ( p->vClocks )       Vec_PtrFree( p->vClocks );
     if ( p->vClockFlops )   Vec_VecFree( p->vClockFlops );
+    if ( p->vResets )       Vec_PtrFree( p->vResets );
+    if ( p->vResetFlops )   Vec_VecFree( p->vResetFlops );
     Vec_PtrFree( p->vNets );
     Vec_PtrFree( p->vObjs );
     Vec_PtrFree( p->vPis );
@@ -699,6 +815,90 @@ Ntl_Mod_t * Ntl_ManCreateLatchModel( Ntl_Man_t * pMan, int Init )
 }
 
 
+/**Function*************************************************************
+
+  Synopsis    [Count constant nodes.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Ntl_ModelCountLut0( Ntl_Mod_t * p )
+{
+    Ntl_Obj_t * pNode;
+    int i, Counter = 0;
+    Ntl_ModelForEachNode( p, pNode, i )
+        if ( Ntl_ObjFaninNum(pNode) == 0 )
+            Counter++;
+    return Counter;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Count single-output nodes.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Ntl_ModelCountLut1( Ntl_Mod_t * p )
+{
+    Ntl_Obj_t * pNode;
+    int i, Counter = 0;
+    Ntl_ModelForEachNode( p, pNode, i )
+        if ( Ntl_ObjFaninNum(pNode) == 1 )
+            Counter++;
+    return Counter;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Count buffers]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Ntl_ModelCountBuf( Ntl_Mod_t * p )
+{
+    Ntl_Obj_t * pNode;
+    int i, Counter = 0;
+    Ntl_ModelForEachNode( p, pNode, i )
+        if ( Ntl_ObjFaninNum(pNode) == 1 && pNode->pSop[0] == '1' )
+            Counter++;
+    return Counter;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Count inverters.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Ntl_ModelCountInv( Ntl_Mod_t * p )
+{
+    Ntl_Obj_t * pNode;
+    int i, Counter = 0;
+    Ntl_ModelForEachNode( p, pNode, i )
+        if ( Ntl_ObjFaninNum(pNode) == 1 && pNode->pSop[0] == '0' )
+            Counter++;
+    return Counter;
+}
+
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/aig/ntl/ntlObj.c b/src/aig/ntl/ntlObj.c
index 55924db9..4946c4e3 100644
--- a/src/aig/ntl/ntlObj.c
+++ b/src/aig/ntl/ntlObj.c
@@ -160,6 +160,7 @@ Ntl_Obj_t * Ntl_ModelCreateBox( Ntl_Mod_t * pModel, int nFanins, int nFanouts )
     p->Type     = NTL_OBJ_BOX;
     p->nFanins  = nFanins;
     p->nFanouts = nFanouts;
+    p->Reset    = -1;
     pModel->nObjs[NTL_OBJ_BOX]++;
     return p;
 }
@@ -285,6 +286,27 @@ char * Ntl_ManStoreFileName( Ntl_Man_t * p, char * pFileName )
 }
 
 
+/**Function*************************************************************
+
+  Synopsis    [Returns the index of the fanin in the fanin list of the fanout.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Ntl_ManObjWhichFanout( Ntl_Obj_t * pNode, Ntl_Net_t * pFanout )
+{
+    Ntl_Net_t * pObj;
+    int i;
+    Ntl_ObjForEachFanout( pNode, pObj, i )
+        if ( pObj == pFanout )
+            return i;
+    return -1;
+}
+
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/aig/ntl/ntlUtil.c b/src/aig/ntl/ntlUtil.c
index 6d1b6c83..6a4b18d5 100644
--- a/src/aig/ntl/ntlUtil.c
+++ b/src/aig/ntl/ntlUtil.c
@@ -30,27 +30,6 @@
 
 /**Function*************************************************************
 
-  Synopsis    [Counts COs that are connected to the internal nodes through invs/bufs.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-int Ntl_ModelCountLut1( Ntl_Mod_t * pRoot )
-{
-    Ntl_Obj_t * pObj;
-    int i, Counter = 0;
-    Ntl_ModelForEachNode( pRoot, pObj, i )
-        if ( Ntl_ObjFaninNum(pObj) == 1 )
-            Counter++;
-    return Counter;
-}
-
-/**Function*************************************************************
-
   Synopsis    [Reads the maximum number of fanins.]
 
   Description []
@@ -370,6 +349,7 @@ Vec_Vec_t * Ntl_ManTransformRegClasses( Ntl_Man_t * pMan, int nSizeMax, int fVer
     if ( Vec_IntSize(pMan->vRegClasses) == 0 )
     {
         printf( "Ntl_ManReportRegClasses(): Register classes are not defined.\n" );
+//        return (Vec_Vec_t *)Vec_PtrAlloc(0);
         return NULL;
     }
     // find the largest class