Version abc61111

author: Alan Mishchenko <alanmi@berkeley.edu> 2006-11-11 08:01:00 -0800
committer: Alan Mishchenko <alanmi@berkeley.edu> 2006-11-11 08:01:00 -0800
commit: da5e0785dfb98335bd49a13bf9e86e736fb931be (patch)
tree: 3e88084f64093c8394fddf2d96b522a4df183981 /src/base
parent: faf1265bb82f934cc14b6106ccce89e37203efbd (diff)
download: abc-da5e0785dfb98335bd49a13bf9e86e736fb931be.tar.gz
abc-da5e0785dfb98335bd49a13bf9e86e736fb931be.tar.bz2
abc-da5e0785dfb98335bd49a13bf9e86e736fb931be.zip
30 files changed, 1006 insertions, 138 deletions
diff --git a/src/base/abc/abc.h b/src/base/abc/abc.h
index 33345577..f44a8022 100644
--- a/src/base/abc/abc.h
+++ b/src/base/abc/abc.h
@@ -344,8 +344,8 @@ static inline bool        Abc_ObjIsPo( Abc_Obj_t * pObj )            { return pO
 static inline bool        Abc_ObjIsBi( Abc_Obj_t * pObj )            { return pObj->Type == ABC_OBJ_BI;      }
 static inline bool        Abc_ObjIsBo( Abc_Obj_t * pObj )            { return pObj->Type == ABC_OBJ_BO;      }
 static inline bool        Abc_ObjIsAssert( Abc_Obj_t * pObj )        { return pObj->Type == ABC_OBJ_ASSERT;  }
-static inline bool        Abc_ObjIsCi( Abc_Obj_t * pObj )            { return pObj->Type == ABC_OBJ_PI || pObj->Type == ABC_OBJ_BI; }
-static inline bool        Abc_ObjIsCo( Abc_Obj_t * pObj )            { return pObj->Type == ABC_OBJ_PO || pObj->Type == ABC_OBJ_BO || pObj->Type == ABC_OBJ_ASSERT; }
+static inline bool        Abc_ObjIsCi( Abc_Obj_t * pObj )            { return pObj->Type == ABC_OBJ_PI || pObj->Type == ABC_OBJ_BO; }
+static inline bool        Abc_ObjIsCo( Abc_Obj_t * pObj )            { return pObj->Type == ABC_OBJ_PO || pObj->Type == ABC_OBJ_BI || pObj->Type == ABC_OBJ_ASSERT; }
 static inline bool        Abc_ObjIsTerm( Abc_Obj_t * pObj )          { return Abc_ObjIsCi(pObj) || Abc_ObjIsCo(pObj); }
 static inline bool        Abc_ObjIsNet( Abc_Obj_t * pObj )           { return pObj->Type == ABC_OBJ_NET;     }
 static inline bool        Abc_ObjIsNode( Abc_Obj_t * pObj )          { return pObj->Type == ABC_OBJ_NODE;    }
@@ -547,6 +547,7 @@ extern void               Abc_ObjPatchFanin( Abc_Obj_t * pObj, Abc_Obj_t * pFani
 extern Abc_Obj_t *        Abc_ObjInsertBetween( Abc_Obj_t * pNodeIn, Abc_Obj_t * pNodeOut, Abc_ObjType_t Type );
 extern void               Abc_ObjTransferFanout( Abc_Obj_t * pObjOld, Abc_Obj_t * pObjNew );
 extern void               Abc_ObjReplace( Abc_Obj_t * pObjOld, Abc_Obj_t * pObjNew );
+extern int                Abc_ObjFanoutFaninNum( Abc_Obj_t * pFanout, Abc_Obj_t * pFanin );
 /*=== abcFraig.c ==========================================================*/
 extern Abc_Ntk_t *        Abc_NtkFraig( Abc_Ntk_t * pNtk, void * pParams, int fAllNodes, int fExdc );
 extern void *             Abc_NtkToFraig( Abc_Ntk_t * pNtk, void * pParams, int fAllNodes, int fExdc );
@@ -573,6 +574,7 @@ extern bool               Abc_NtkLatchIsSelfFeed( Abc_Obj_t * pLatch );
 extern int                Abc_NtkCountSelfFeedLatches( Abc_Ntk_t * pNtk );
 extern int                Abc_NtkRemoveSelfFeedLatches( Abc_Ntk_t * pNtk );
 extern Vec_Int_t *        Abc_NtkCollectLatchValues( Abc_Ntk_t * pNtk );
+extern void               Abc_NtkInsertLatchValues( Abc_Ntk_t * pNtk, Vec_Int_t * vValues );
  /*=== abcLib.c ==========================================================*/
 extern Abc_Lib_t *        Abc_LibCreate( char * pName );
 extern void               Abc_LibFree( Abc_Lib_t * pLib );
@@ -599,6 +601,7 @@ extern void               Abc_ObjRecycle( Abc_Obj_t * pObj );
 extern Abc_Obj_t *        Abc_NtkCreateObj( Abc_Ntk_t * pNtk, Abc_ObjType_t Type );
 extern void               Abc_NtkDeleteObj( Abc_Obj_t * pObj );
 extern void               Abc_NtkDeleteObj_rec( Abc_Obj_t * pObj, int fOnlyNodes );
+extern void               Abc_NtkDeleteAll_rec( Abc_Obj_t * pObj );
 extern Abc_Obj_t *        Abc_NtkDupObj( Abc_Ntk_t * pNtkNew, Abc_Obj_t * pObj, int fCopyName );
 extern Abc_Obj_t *        Abc_NtkDupBox( Abc_Ntk_t * pNtkNew, Abc_Obj_t * pBox, int fCopyName );
 extern Abc_Obj_t *        Abc_NtkCloneObj( Abc_Obj_t * pNode );
@@ -808,6 +811,7 @@ extern Abc_Obj_t *        Abc_NodeRecognizeMux( Abc_Obj_t * pNode, Abc_Obj_t **
 extern int                Abc_NtkPrepareTwoNtks( FILE * pErr, Abc_Ntk_t * pNtk, char ** argv, int argc, Abc_Ntk_t ** ppNtk1, Abc_Ntk_t ** ppNtk2, int * pfDelete1, int * pfDelete2 );
 extern void               Abc_NodeCollectFanins( Abc_Obj_t * pNode, Vec_Ptr_t * vNodes );
 extern void               Abc_NodeCollectFanouts( Abc_Obj_t * pNode, Vec_Ptr_t * vNodes );
+extern Vec_Ptr_t *        Abc_NtkCollectLatches( Abc_Ntk_t * pNtk );
 extern int                Abc_NodeCompareLevelsIncrease( Abc_Obj_t ** pp1, Abc_Obj_t ** pp2 );
 extern int                Abc_NodeCompareLevelsDecrease( Abc_Obj_t ** pp1, Abc_Obj_t ** pp2 );
 extern Vec_Int_t *        Abc_NtkFanoutCounts( Abc_Ntk_t * pNtk );
diff --git a/src/base/abc/abcCheck.c b/src/base/abc/abcCheck.c
index d0c1deef..eb5a8400 100644
--- a/src/base/abc/abcCheck.c
+++ b/src/base/abc/abcCheck.c
@@ -20,7 +20,7 @@
 
 #include "abc.h"
 #include "main.h"
-#include "seq.h"
+//#include "seq.h"
 
 ////////////////////////////////////////////////////////////////////////
 ///                        DECLARATIONS                              ///
diff --git a/src/base/abc/abcDfs.c b/src/base/abc/abcDfs.c
index d9985737..a8edfbeb 100644
--- a/src/base/abc/abcDfs.c
+++ b/src/base/abc/abcDfs.c
@@ -638,6 +638,10 @@ int Abc_NtkGetLevelNum_rec( Abc_Obj_t * pNode )
     Abc_Obj_t * pFanin;
     int i, Level;
     assert( !Abc_ObjIsNet(pNode) );
+    if ( pNode->Id == 27278 )
+    {
+        int x = 0;        
+    }
     // skip the PI
     if ( Abc_ObjIsCi(pNode) )
         return 0;
diff --git a/src/base/abc/abcFanio.c b/src/base/abc/abcFanio.c
index 0581b35d..a988062f 100644
--- a/src/base/abc/abcFanio.c
+++ b/src/base/abc/abcFanio.c
@@ -19,7 +19,7 @@
 ***********************************************************************/
 
 #include "abc.h"
-#include "seqInt.h"
+//#include "seqInt.h"
 
 ////////////////////////////////////////////////////////////////////////
 ///                        DECLARATIONS                              ///
@@ -128,7 +128,7 @@ void Abc_ObjRemoveFanins( Abc_Obj_t * pObj )
 void Abc_ObjPatchFanin( Abc_Obj_t * pObj, Abc_Obj_t * pFaninOld, Abc_Obj_t * pFaninNew )
 {
     Abc_Obj_t * pFaninNewR = Abc_ObjRegular(pFaninNew);
-    int iFanin, nLats;//, fCompl;
+    int iFanin;//, nLats;//, fCompl;
     assert( !Abc_ObjIsComplement(pObj) );
     assert( !Abc_ObjIsComplement(pFaninOld) );
     assert( pFaninOld != pFaninNewR );
@@ -153,8 +153,8 @@ void Abc_ObjPatchFanin( Abc_Obj_t * pObj, Abc_Obj_t * pFaninOld, Abc_Obj_t * pFa
     if ( Abc_ObjIsComplement(pFaninNew) )
         Abc_ObjXorFaninC( pObj, iFanin );
 
-    if ( Abc_NtkIsSeq(pObj->pNtk) && (nLats = Seq_ObjFaninL(pObj, iFanin)) )
-        Seq_ObjSetFaninL( pObj, iFanin, nLats );
+//    if ( Abc_NtkIsSeq(pObj->pNtk) && (nLats = Seq_ObjFaninL(pObj, iFanin)) )
+//        Seq_ObjSetFaninL( pObj, iFanin, nLats );
     // update the fanout of the fanin
     if ( !Vec_IntRemove( &pFaninOld->vFanouts, pObj->Id ) )
     {
@@ -223,8 +223,7 @@ void Abc_ObjTransferFanout( Abc_Obj_t * pNodeFrom, Abc_Obj_t * pNodeTo )
     int nFanoutsOld, i;
     assert( !Abc_ObjIsComplement(pNodeFrom) );
     assert( !Abc_ObjIsComplement(pNodeTo) );
-    assert( Abc_ObjIsNode(pNodeFrom) || Abc_ObjIsCi(pNodeFrom) );
-    assert( !Abc_ObjIsPo(pNodeTo) );
+    assert( !Abc_ObjIsPo(pNodeFrom) && !Abc_ObjIsPo(pNodeTo) );
     assert( pNodeFrom->pNtk == pNodeTo->pNtk );
     assert( pNodeFrom != pNodeTo );
     assert( Abc_ObjFanoutNum(pNodeFrom) > 0 );
@@ -264,6 +263,27 @@ void Abc_ObjReplace( Abc_Obj_t * pNodeOld, Abc_Obj_t * pNodeNew )
     Abc_NtkDeleteObj( pNodeOld );
 }
 
+/**Function*************************************************************
+
+  Synopsis    [Returns the index of the fanin in the fanin list of the fanout.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Abc_ObjFanoutFaninNum( Abc_Obj_t * pFanout, Abc_Obj_t * pFanin )
+{
+    Abc_Obj_t * pObj;
+    int i;
+    Abc_ObjForEachFanin( pFanout, pObj, i )
+        if ( pObj == pFanin )
+            return i;
+    return -1;
+}
+
 
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
diff --git a/src/base/abc/abcLatch.c b/src/base/abc/abcLatch.c
index 7bc5e264..e475fd2a 100644
--- a/src/base/abc/abcLatch.c
+++ b/src/base/abc/abcLatch.c
@@ -46,9 +46,9 @@ bool Abc_NtkLatchIsSelfFeed_rec( Abc_Obj_t * pLatch, Abc_Obj_t * pLatchRoot )
     if ( pLatch == pLatchRoot )
         return 1;
     pFanin = Abc_ObjFanin0(Abc_ObjFanin0(pLatch));
-    if ( !Abc_ObjIsBi(pFanin) || !Abc_ObjIsLatch(Abc_ObjFanin0(pFanin)) )
+    if ( !Abc_ObjIsBo(pFanin) || !Abc_ObjIsLatch(Abc_ObjFanin0(pFanin)) )
         return 0;
-    return Abc_NtkLatchIsSelfFeed_rec( Abc_ObjFanin0(pFanin), pLatchRoot );
+    return Abc_NtkLatchIsSelfFeed_rec( Abc_ObjFanin0(pFanin), pLatch );
 }
 
 /**Function*************************************************************
@@ -67,7 +67,7 @@ bool Abc_NtkLatchIsSelfFeed( Abc_Obj_t * pLatch )
     Abc_Obj_t * pFanin;
     assert( Abc_ObjIsLatch(pLatch) );
     pFanin = Abc_ObjFanin0(Abc_ObjFanin0(pLatch));
-    if ( !Abc_ObjIsBi(pFanin) || !Abc_ObjIsLatch(Abc_ObjFanin0(pFanin)) )
+    if ( !Abc_ObjIsBo(pFanin) || !Abc_ObjIsLatch(Abc_ObjFanin0(pFanin)) )
         return 0;
     return Abc_NtkLatchIsSelfFeed_rec( Abc_ObjFanin0(pFanin), pLatch );
 }
@@ -183,13 +183,32 @@ void Abc_NtkLatchPipe( Abc_Ntk_t * pNtk, int nLatches )
 ***********************************************************************/
 Vec_Int_t * Abc_NtkCollectLatchValues( Abc_Ntk_t * pNtk )
 {
-    Vec_Int_t * vArray;
+    Vec_Int_t * vValues;
+    Abc_Obj_t * pLatch;
+    int i;
+    vValues = Vec_IntAlloc( Abc_NtkLatchNum(pNtk) );
+    Abc_NtkForEachLatch( pNtk, pLatch, i )
+        Vec_IntPush( vValues, Abc_LatchIsInit1(pLatch) );
+    return vValues;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Strashes one logic node using its SOP.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Abc_NtkInsertLatchValues( Abc_Ntk_t * pNtk, Vec_Int_t * vValues )
+{
     Abc_Obj_t * pLatch;
     int i;
-    vArray = Vec_IntAlloc( Abc_NtkLatchNum(pNtk) );
     Abc_NtkForEachLatch( pNtk, pLatch, i )
-        Vec_IntPush( vArray, Abc_LatchIsInit1(pLatch) );
-    return vArray;
+        pLatch->pData = (void *)(vValues? (Vec_IntEntry(vValues,i)? ABC_INIT_ONE : ABC_INIT_ZERO) : ABC_INIT_DC);
 }
 
 
diff --git a/src/base/abc/abcLib.c b/src/base/abc/abcLib.c
index be0d34b7..218df6ef 100644
--- a/src/base/abc/abcLib.c
+++ b/src/base/abc/abcLib.c
@@ -148,11 +148,11 @@ int Abc_LibDeriveBlackBoxes( Abc_Ntk_t * pNtk, Abc_Lib_t * pLib )
     {
         // go through the fanin nets
         Abc_ObjForEachFanin( pObj, pFanin, k )
-            Abc_ObjInsertBetween( pFanin, pObj, ABC_OBJ_BO );
+            Abc_ObjInsertBetween( pFanin, pObj, ABC_OBJ_BI );
         // go through the fanout nets
         Abc_ObjForEachFanout( pObj, pFanout, k )
         {
-            Abc_ObjInsertBetween( pObj, pFanout, ABC_OBJ_BI );
+            Abc_ObjInsertBetween( pObj, pFanout, ABC_OBJ_BO );
             // if the name is not given assign name
             if ( pFanout->pData == NULL )
             {
diff --git a/src/base/abc/abcNetlist.c b/src/base/abc/abcNetlist.c
index 30fab9a3..5ea9b369 100644
--- a/src/base/abc/abcNetlist.c
+++ b/src/base/abc/abcNetlist.c
@@ -19,7 +19,7 @@
 ***********************************************************************/
 
 #include "abc.h"
-#include "seq.h"
+//#include "seq.h"
 
 ////////////////////////////////////////////////////////////////////////
 ///                        DECLARATIONS                              ///
diff --git a/src/base/abc/abcNtk.c b/src/base/abc/abcNtk.c
index 96f489bd..a3ce5145 100644
--- a/src/base/abc/abcNtk.c
+++ b/src/base/abc/abcNtk.c
@@ -22,7 +22,7 @@
 #include "abcInt.h"
 #include "main.h"
 #include "mio.h"
-#include "seqInt.h"
+//#include "seqInt.h"
 
 ////////////////////////////////////////////////////////////////////////
 ///                        DECLARATIONS                              ///
@@ -343,7 +343,7 @@ Abc_Ntk_t * Abc_NtkDup( Abc_Ntk_t * pNtk )
                 Abc_NtkDupObj(pNtkNew, pObj, 0);
         // reconnect all objects (no need to transfer attributes on edges)
         Abc_NtkForEachObj( pNtk, pObj, i )
-            if ( !Abc_ObjIsBox(pObj) && !Abc_ObjIsBi(pObj) )
+            if ( !Abc_ObjIsBox(pObj) && !Abc_ObjIsBo(pObj) )
                 Abc_ObjForEachFanin( pObj, pFanin, k )
                     Abc_ObjAddFanin( pObj->pCopy, pFanin->pCopy );
     }
@@ -357,6 +357,92 @@ Abc_Ntk_t * Abc_NtkDup( Abc_Ntk_t * pNtk )
 
 /**Function*************************************************************
 
+  Synopsis    [Duplicate the network.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Abc_Ntk_t * Abc_NtkDouble( Abc_Ntk_t * pNtk )
+{
+    char Buffer[500];
+    Abc_Ntk_t * pNtkNew; 
+    Abc_Obj_t * pObj, * pFanin;
+    int i, k;
+    assert( Abc_NtkIsLogic(pNtk) );
+
+    // start the network
+    pNtkNew = Abc_NtkAlloc( pNtk->ntkType, pNtk->ntkFunc, 1 );
+    sprintf( Buffer, "%s%s", pNtk->pName, "_doubled" );
+    pNtkNew->pName = Extra_UtilStrsav(Buffer);
+
+    // clean the node copy fields
+    Abc_NtkCleanCopy( pNtk );
+    // clone CIs/CIs/boxes
+    Abc_NtkForEachPi( pNtk, pObj, i )
+        Abc_NtkDupObj( pNtkNew, pObj, 0 );
+    Abc_NtkForEachPo( pNtk, pObj, i )
+        Abc_NtkDupObj( pNtkNew, pObj, 0 );
+    Abc_NtkForEachAssert( pNtk, pObj, i )
+        Abc_NtkDupObj( pNtkNew, pObj, 0 );
+    Abc_NtkForEachBox( pNtk, pObj, i )
+        Abc_NtkDupBox( pNtkNew, pObj, 0 );
+    // copy the internal nodes
+    // duplicate the nets and nodes (CIs/COs/latches already dupped)
+    Abc_NtkForEachObj( pNtk, pObj, i )
+        if ( pObj->pCopy == NULL )
+            Abc_NtkDupObj(pNtkNew, pObj, 0);
+    // reconnect all objects (no need to transfer attributes on edges)
+    Abc_NtkForEachObj( pNtk, pObj, i )
+        if ( !Abc_ObjIsBox(pObj) && !Abc_ObjIsBo(pObj) )
+            Abc_ObjForEachFanin( pObj, pFanin, k )
+                Abc_ObjAddFanin( pObj->pCopy, pFanin->pCopy );
+
+    // clean the node copy fields
+    Abc_NtkCleanCopy( pNtk );
+    // clone CIs/CIs/boxes
+    Abc_NtkForEachPi( pNtk, pObj, i )
+        Abc_NtkDupObj( pNtkNew, pObj, 0 );
+    Abc_NtkForEachPo( pNtk, pObj, i )
+        Abc_NtkDupObj( pNtkNew, pObj, 0 );
+    Abc_NtkForEachAssert( pNtk, pObj, i )
+        Abc_NtkDupObj( pNtkNew, pObj, 0 );
+    Abc_NtkForEachBox( pNtk, pObj, i )
+        Abc_NtkDupBox( pNtkNew, pObj, 0 );
+    // copy the internal nodes
+    // duplicate the nets and nodes (CIs/COs/latches already dupped)
+    Abc_NtkForEachObj( pNtk, pObj, i )
+        if ( pObj->pCopy == NULL )
+            Abc_NtkDupObj(pNtkNew, pObj, 0);
+    // reconnect all objects (no need to transfer attributes on edges)
+    Abc_NtkForEachObj( pNtk, pObj, i )
+        if ( !Abc_ObjIsBox(pObj) && !Abc_ObjIsBo(pObj) )
+            Abc_ObjForEachFanin( pObj, pFanin, k )
+                Abc_ObjAddFanin( pObj->pCopy, pFanin->pCopy );
+
+    // assign names
+    Abc_NtkForEachCi( pNtk, pObj, i )
+    {
+        Abc_ObjAssignName( Abc_NtkCi(pNtkNew,                      i), "1_", Abc_ObjName(pObj) );
+        Abc_ObjAssignName( Abc_NtkCi(pNtkNew, Abc_NtkCiNum(pNtk) + i), "2_", Abc_ObjName(pObj) );
+    }
+    Abc_NtkForEachCo( pNtk, pObj, i )
+    {
+        Abc_ObjAssignName( Abc_NtkCo(pNtkNew,                      i), "1_", Abc_ObjName(pObj) );
+        Abc_ObjAssignName( Abc_NtkCo(pNtkNew, Abc_NtkCoNum(pNtk) + i), "2_", Abc_ObjName(pObj) );
+    }
+
+    // perform the final check
+    if ( !Abc_NtkCheck( pNtkNew ) )
+        fprintf( stdout, "Abc_NtkDup(): Network check has failed.\n" );
+    return pNtkNew;
+}
+
+/**Function*************************************************************
+
   Synopsis    [Attaches the second network at the bottom of the first.]
 
   Description [Returns the first network. Deletes the second network.]
diff --git a/src/base/abc/abcObj.c b/src/base/abc/abcObj.c
index ca86565a..dc3ff73c 100644
--- a/src/base/abc/abcObj.c
+++ b/src/base/abc/abcObj.c
@@ -129,10 +129,10 @@ Abc_Obj_t * Abc_NtkCreateObj( Abc_Ntk_t * pNtk, Abc_ObjType_t Type )
             Vec_PtrPush( pNtk->vCos, pObj );
             break;
         case ABC_OBJ_BI:     
-            if ( pNtk->vCis ) Vec_PtrPush( pNtk->vCis, pObj );
+            if ( pNtk->vCos ) Vec_PtrPush( pNtk->vCos, pObj );
             break;
         case ABC_OBJ_BO:     
-            if ( pNtk->vCos ) Vec_PtrPush( pNtk->vCos, pObj );
+            if ( pNtk->vCis ) Vec_PtrPush( pNtk->vCis, pObj );
             break;
         case ABC_OBJ_ASSERT:     
             Vec_PtrPush( pNtk->vAsserts, pObj );
@@ -171,11 +171,11 @@ void Abc_NtkDeleteObj( Abc_Obj_t * pObj )
     Abc_Ntk_t * pNtk = pObj->pNtk;
     Vec_Ptr_t * vNodes;
     int i;
+    assert( !Abc_ObjIsComplement(pObj) );
     // remove from the table of names
     if ( Nm_ManFindNameById(pObj->pNtk->pManName, pObj->Id) )
         Nm_ManDeleteIdName(pObj->pNtk->pManName, pObj->Id);
     // delete fanins and fanouts
-    assert( !Abc_ObjIsComplement(pObj) );
     vNodes = Vec_PtrAlloc( 100 );
     Abc_NodeCollectFanouts( pObj, vNodes );
     for ( i = 0; i < vNodes->nSize; i++ )
@@ -210,10 +210,10 @@ void Abc_NtkDeleteObj( Abc_Obj_t * pObj )
             Vec_PtrRemove( pNtk->vCos, pObj );
             break;
         case ABC_OBJ_BI:     
-            if ( pNtk->vCis ) Vec_PtrRemove( pNtk->vCis, pObj );
+            if ( pNtk->vCos ) Vec_PtrRemove( pNtk->vCos, pObj );
             break;
         case ABC_OBJ_BO:     
-            if ( pNtk->vCos ) Vec_PtrRemove( pNtk->vCos, pObj );
+            if ( pNtk->vCis ) Vec_PtrRemove( pNtk->vCis, pObj );
             break;
         case ABC_OBJ_ASSERT:     
             Vec_PtrRemove( pNtk->vAsserts, pObj );
@@ -253,7 +253,6 @@ void Abc_NtkDeleteObj( Abc_Obj_t * pObj )
 ***********************************************************************/
 void Abc_NtkDeleteObj_rec( Abc_Obj_t * pObj, int fOnlyNodes )
 {
-    Abc_Ntk_t * pNtk = pObj->pNtk;
     Vec_Ptr_t * vNodes;
     int i;
     assert( !Abc_ObjIsComplement(pObj) );
@@ -280,6 +279,33 @@ void Abc_NtkDeleteObj_rec( Abc_Obj_t * pObj, int fOnlyNodes )
 
 /**Function*************************************************************
 
+  Synopsis    [Deletes the node and MFFC of the node.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Abc_NtkDeleteAll_rec( Abc_Obj_t * pObj )
+{
+    Vec_Ptr_t * vNodes;
+    int i;
+    assert( !Abc_ObjIsComplement(pObj) );
+    assert( Abc_ObjFanoutNum(pObj) == 0 );
+    // delete fanins and fanouts
+    vNodes = Vec_PtrAlloc( 100 );
+    Abc_NodeCollectFanins( pObj, vNodes );
+    Abc_NtkDeleteObj( pObj );
+    Vec_PtrForEachEntry( vNodes, pObj, i )
+        if ( Abc_ObjFanoutNum(pObj) == 0 )
+            Abc_NtkDeleteAll_rec( pObj );
+    Vec_PtrFree( vNodes );
+}
+
+/**Function*************************************************************
+
   Synopsis    [Duplicate the Obj.]
 
   Description []
@@ -401,7 +427,7 @@ Abc_Obj_t * Abc_NtkFindNode( Abc_Ntk_t * pNtk, char * pName )
     Num = Nm_ManFindIdByName( pNtk->pManName, pName, ABC_OBJ_PO );
     if ( Num >= 0 )
         return Abc_ObjFanin0( Abc_NtkObj( pNtk, Num ) );
-    Num = Nm_ManFindIdByName( pNtk->pManName, pName, ABC_OBJ_BO );
+    Num = Nm_ManFindIdByName( pNtk->pManName, pName, ABC_OBJ_BI );
     if ( Num >= 0 )
         return Abc_ObjFanin0( Abc_NtkObj( pNtk, Num ) );
     Num = Nm_ManFindIdByName( pNtk->pManName, pName, ABC_OBJ_NODE );
@@ -474,7 +500,7 @@ Abc_Obj_t * Abc_NtkFindCi( Abc_Ntk_t * pNtk, char * pName )
     Num = Nm_ManFindIdByName( pNtk->pManName, pName, ABC_OBJ_PI );
     if ( Num >= 0 )
         return Abc_NtkObj( pNtk, Num );
-    Num = Nm_ManFindIdByName( pNtk->pManName, pName, ABC_OBJ_BI );
+    Num = Nm_ManFindIdByName( pNtk->pManName, pName, ABC_OBJ_BO );
     if ( Num >= 0 )
         return Abc_NtkObj( pNtk, Num );
     return NULL;
@@ -498,7 +524,7 @@ Abc_Obj_t * Abc_NtkFindCo( Abc_Ntk_t * pNtk, char * pName )
     Num = Nm_ManFindIdByName( pNtk->pManName, pName, ABC_OBJ_PO );
     if ( Num >= 0 )
         return Abc_NtkObj( pNtk, Num );
-    Num = Nm_ManFindIdByName( pNtk->pManName, pName, ABC_OBJ_BO );
+    Num = Nm_ManFindIdByName( pNtk->pManName, pName, ABC_OBJ_BI );
     if ( Num >= 0 )
         return Abc_NtkObj( pNtk, Num );
     return NULL;
diff --git a/src/base/abc/abcShow.c b/src/base/abc/abcShow.c
index 8ed653a9..fa921391 100644
--- a/src/base/abc/abcShow.c
+++ b/src/base/abc/abcShow.c
@@ -259,7 +259,8 @@ void Abc_NtkShow( Abc_Ntk_t * pNtk, int fGateNames )
     char FileNameDot[200];
     int i;
 
-    assert( !Abc_NtkHasAig(pNtk) );
+    assert( !Abc_NtkIsStrash(pNtk) );
+    Abc_NtkLogicToSop( pNtk, 0 );
     // create the file name
     Abc_ShowGetFileName( pNtk->pName, FileNameDot );
     // check that the file can be opened
@@ -273,7 +274,8 @@ void Abc_NtkShow( Abc_Ntk_t * pNtk, int fGateNames )
     // collect all nodes in the network
     vNodes = Vec_PtrAlloc( 100 );
     Abc_NtkForEachObj( pNtk, pNode, i )
-        Vec_PtrPush( vNodes, pNode );
+//        if ( !Abc_ObjIsBi(pNode) && !Abc_ObjIsBo(pNode) )
+            Vec_PtrPush( vNodes, pNode );
     // write the DOT file
     Io_WriteDotNtk( pNtk, vNodes, NULL, FileNameDot, fGateNames );
     Vec_PtrFree( vNodes );
diff --git a/src/base/abc/abcUtil.c b/src/base/abc/abcUtil.c
index d5a4b5cb..fa1cd69a 100644
--- a/src/base/abc/abcUtil.c
+++ b/src/base/abc/abcUtil.c
@@ -22,7 +22,7 @@
 #include "main.h"
 #include "mio.h"
 #include "dec.h"
-#include "seq.h"
+//#include "seq.h"
 
 ////////////////////////////////////////////////////////////////////////
 ///                        DECLARATIONS                              ///
@@ -1038,6 +1038,28 @@ void Abc_NodeCollectFanouts( Abc_Obj_t * pNode, Vec_Ptr_t * vNodes )
 
 /**Function*************************************************************
 
+  Synopsis    [Collects all latches in the network.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Vec_Ptr_t * Abc_NtkCollectLatches( Abc_Ntk_t * pNtk )
+{
+    Vec_Ptr_t * vLatches;
+    Abc_Obj_t * pObj;
+    int i;
+    vLatches = Vec_PtrAlloc( 10 );
+    Abc_NtkForEachObj( pNtk, pObj, i )
+        Vec_PtrPush( vLatches, pObj );
+    return vLatches;
+}
+
+/**Function*************************************************************
+
   Synopsis    [Procedure used for sorting the nodes in increasing order of levels.]
 
   Description []
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index 5d6af56d..dffe4b99 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -25,7 +25,7 @@
 #include "fpga.h"
 #include "pga.h"
 #include "cut.h"
-#include "seq.h"
+//#include "seq.h"
 
 ////////////////////////////////////////////////////////////////////////
 ///                        DECLARATIONS                              ///
@@ -92,6 +92,8 @@ static int Abc_CommandEspresso       ( Abc_Frame_t * pAbc, int argc, char ** arg
 static int Abc_CommandGen            ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandXyz            ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandXsim           ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandCycle          ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandDouble         ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandTest           ( Abc_Frame_t * pAbc, int argc, char ** argv );
 
 static int Abc_CommandIStrash        ( Abc_Frame_t * pAbc, int argc, char ** argv );
@@ -138,6 +140,7 @@ static int Abc_CommandCec            ( Abc_Frame_t * pAbc, int argc, char ** arg
 static int Abc_CommandSec            ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandSat            ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandProve          ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandDebug          ( Abc_Frame_t * pAbc, int argc, char ** argv );
 
 static int Abc_CommandTraceStart     ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandTraceCheck     ( Abc_Frame_t * pAbc, int argc, char ** argv );
@@ -201,7 +204,7 @@ void Abc_Init( Abc_Frame_t * pAbc )
     Cmd_CommandAdd( pAbc, "Synthesis",    "resub",         Abc_CommandResubstitute,     1 );
     Cmd_CommandAdd( pAbc, "Synthesis",    "rr",            Abc_CommandRr,               1 );
 
-//    Cmd_CommandAdd( pAbc, "Various",      "logic",         Abc_CommandLogic,            1 );
+    Cmd_CommandAdd( pAbc, "Various",      "logic",         Abc_CommandLogic,            1 );
     Cmd_CommandAdd( pAbc, "Various",      "miter",         Abc_CommandMiter,            1 );
     Cmd_CommandAdd( pAbc, "Various",      "demiter",       Abc_CommandDemiter,          1 );
     Cmd_CommandAdd( pAbc, "Various",      "orpos",         Abc_CommandOrPos,            1 );
@@ -225,6 +228,8 @@ void Abc_Init( Abc_Frame_t * pAbc )
     Cmd_CommandAdd( pAbc, "Various",      "gen",           Abc_CommandGen,              0 );
     Cmd_CommandAdd( pAbc, "Various",      "xyz",           Abc_CommandXyz,              1 );
     Cmd_CommandAdd( pAbc, "Various",      "xsim",          Abc_CommandXsim,             0 );
+    Cmd_CommandAdd( pAbc, "Various",      "cycle",         Abc_CommandCycle,            1 );
+    Cmd_CommandAdd( pAbc, "Various",      "double",        Abc_CommandDouble,           1 );
     Cmd_CommandAdd( pAbc, "Various",      "test",          Abc_CommandTest,             0 );
 
     Cmd_CommandAdd( pAbc, "New AIG",      "istrash",       Abc_CommandIStrash,          1 );
@@ -257,7 +262,7 @@ void Abc_Init( Abc_Frame_t * pAbc )
     Cmd_CommandAdd( pAbc, "FPGA mapping", "pga",           Abc_CommandPga,              1 );
 
 //    Cmd_CommandAdd( pAbc, "Sequential",   "scut",          Abc_CommandScut,             0 );
-//    Cmd_CommandAdd( pAbc, "Sequential",   "init",          Abc_CommandInit,             1 );
+    Cmd_CommandAdd( pAbc, "Sequential",   "init",          Abc_CommandInit,             1 );
 //    Cmd_CommandAdd( pAbc, "Sequential",   "pipe",          Abc_CommandPipe,             1 );
 //    Cmd_CommandAdd( pAbc, "Sequential",   "seq",           Abc_CommandSeq,              1 );
 //    Cmd_CommandAdd( pAbc, "Sequential",   "unseq",         Abc_CommandUnseq,            1 );
@@ -271,6 +276,7 @@ void Abc_Init( Abc_Frame_t * pAbc )
     Cmd_CommandAdd( pAbc, "Verification", "sec",           Abc_CommandSec,              0 );
     Cmd_CommandAdd( pAbc, "Verification", "sat",           Abc_CommandSat,              0 );
     Cmd_CommandAdd( pAbc, "Verification", "prove",         Abc_CommandProve,            1 );
+    Cmd_CommandAdd( pAbc, "Verification", "debug",         Abc_CommandDebug,            0 );
 
 //    Cmd_CommandAdd( pAbc, "Verification", "trace_start",   Abc_CommandTraceStart,       0 );
 //    Cmd_CommandAdd( pAbc, "Verification", "trace_check",   Abc_CommandTraceCheck,       0 );
@@ -3089,14 +3095,14 @@ int Abc_CommandLogic( Abc_Frame_t * pAbc, int argc, char ** argv )
         return 1;
     }
 
-    if ( !Abc_NtkIsNetlist( pNtk ) )
+    if ( !Abc_NtkIsStrash( pNtk ) )
     {
-        fprintf( pErr, "This command is only applicable to netlists.\n" );
+        fprintf( pErr, "This command is only applicable to strashed networks.\n" );
         return 1;
     }
 
     // get the new network
-    pNtkRes = Abc_NtkNetlistToLogic( pNtk );
+    pNtkRes = Abc_NtkAigToLogicSop( pNtk );
     if ( pNtkRes == NULL )
     {
         fprintf( pErr, "Converting to a logic network has failed.\n" );
@@ -3108,7 +3114,7 @@ int Abc_CommandLogic( Abc_Frame_t * pAbc, int argc, char ** argv )
 
 usage:
     fprintf( pErr, "usage: logic [-h]\n" );
-    fprintf( pErr, "\t        transforms a netlist into a logic network\n" );
+    fprintf( pErr, "\t        transforms an AIG into a logic network with SOPs\n" );
     fprintf( pErr, "\t-h    : print the command usage\n");
     return 1;
 }
@@ -5115,6 +5121,169 @@ usage:
   SeeAlso     []
 
 ***********************************************************************/
+int Abc_CommandCycle( Abc_Frame_t * pAbc, int argc, char ** argv )
+{
+    FILE * pOut, * pErr;
+    Abc_Ntk_t * pNtk;
+    int c;
+    int nFrames;
+    int fVerbose;
+    extern void Abc_NtkCycleInitState( Abc_Ntk_t * pNtk, int nFrames, int fVerbose );
+    extern void Abc_NtkCycleInitStateSop( Abc_Ntk_t * pNtk, int nFrames, int fVerbose );
+
+    pNtk = Abc_FrameReadNtk(pAbc);
+    pOut = Abc_FrameReadOut(pAbc);
+    pErr = Abc_FrameReadErr(pAbc);
+
+    // set defaults
+    nFrames    = 50;
+    fVerbose   =  0;
+    Extra_UtilGetoptReset();
+    while ( ( c = Extra_UtilGetopt( argc, argv, "Fvh" ) ) != EOF )
+    {
+        switch ( c )
+        {
+        case 'F':
+            if ( globalUtilOptind >= argc )
+            {
+                fprintf( pErr, "Command line switch \"-F\" should be followed by an integer.\n" );
+                goto usage;
+            }
+            nFrames = atoi(argv[globalUtilOptind]);
+            globalUtilOptind++;
+            if ( nFrames < 0 ) 
+                goto usage;
+            break;
+        case 'v':
+            fVerbose ^= 1;
+            break;
+        case 'h':
+            goto usage;
+        default:
+            goto usage;
+        }
+    }
+    if ( pNtk == NULL )
+    {
+        fprintf( pErr, "Empty network.\n" );
+        return 1;
+    }
+
+    if ( !Abc_NtkIsStrash(pNtk) && !Abc_NtkIsSopLogic(pNtk) )
+    {
+        fprintf( pErr, "Only works for strashed networks or logic SOP networks.\n" );
+        return 1;
+    }
+
+    if ( Abc_NtkIsStrash(pNtk) )
+        Abc_NtkCycleInitState( pNtk, nFrames, fVerbose );
+    else
+        Abc_NtkCycleInitStateSop( pNtk, nFrames, fVerbose );
+    return 0;
+
+usage:
+    fprintf( pErr, "usage: cycle [-F num] [-vh]\n" );
+    fprintf( pErr, "\t         cycles sequiential circuit for the given number of timeframes\n" );
+    fprintf( pErr, "\t         to derive a new initial state (which may be on the envelope)\n" );
+    fprintf( pErr, "\t-F num : the number of frames to simulate [default = %d]\n", nFrames );
+    fprintf( pErr, "\t-v     : toggle printing verbose information [default = %s]\n", fVerbose? "yes": "no" );
+    fprintf( pErr, "\t-h     : print the command usage\n");
+    return 1;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Abc_CommandDouble( Abc_Frame_t * pAbc, int argc, char ** argv )
+{
+    FILE * pOut, * pErr;
+    Abc_Ntk_t * pNtk, * pNtkRes;
+    int c;
+    int nFrames;
+    int fVerbose;
+    extern Abc_Ntk_t * Abc_NtkDouble( Abc_Ntk_t * pNtk );
+
+    pNtk = Abc_FrameReadNtk(pAbc);
+    pOut = Abc_FrameReadOut(pAbc);
+    pErr = Abc_FrameReadErr(pAbc);
+
+    // set defaults
+    nFrames    = 50;
+    fVerbose   =  0;
+    Extra_UtilGetoptReset();
+    while ( ( c = Extra_UtilGetopt( argc, argv, "vh" ) ) != EOF )
+    {
+        switch ( c )
+        {
+        case 'F':
+            if ( globalUtilOptind >= argc )
+            {
+                fprintf( pErr, "Command line switch \"-F\" should be followed by an integer.\n" );
+                goto usage;
+            }
+            nFrames = atoi(argv[globalUtilOptind]);
+            globalUtilOptind++;
+            if ( nFrames < 0 ) 
+                goto usage;
+            break;
+        case 'v':
+            fVerbose ^= 1;
+            break;
+        case 'h':
+            goto usage;
+        default:
+            goto usage;
+        }
+    }
+    if ( pNtk == NULL )
+    {
+        fprintf( pErr, "Empty network.\n" );
+        return 1;
+    }
+
+    if ( !Abc_NtkIsSopLogic(pNtk) )
+    {
+        fprintf( pErr, "Only works for logic SOP networks.\n" );
+        return 1;
+    }
+
+    pNtkRes = Abc_NtkDouble( pNtk );
+    if ( pNtkRes == NULL )
+    {
+        fprintf( pErr, "Command has failed.\n" );
+        return 0;
+    }
+    Abc_FrameReplaceCurrentNetwork( pAbc, pNtkRes );
+    return 0;
+
+usage:
+    fprintf( pErr, "usage: double [-vh]\n" );
+    fprintf( pErr, "\t         puts together two parallel copies of the current network\n" );
+//    fprintf( pErr, "\t-F num : the number of frames to simulate [default = %d]\n", nFrames );
+    fprintf( pErr, "\t-v     : toggle printing verbose information [default = %s]\n", fVerbose? "yes": "no" );
+    fprintf( pErr, "\t-h     : print the command usage\n");
+    return 1;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
 int Abc_CommandTest( Abc_Frame_t * pAbc, int argc, char ** argv )
 {
     FILE * pOut, * pErr;
@@ -5692,10 +5861,10 @@ int Abc_CommandIFraig( Abc_Frame_t * pAbc, int argc, char ** argv )
 {
     FILE * pOut, * pErr;
     Abc_Ntk_t * pNtk, * pNtkRes;
-    int c, fProve, fVerbose;
+    int c, fProve, fVerbose, fDoSparse;
     int nConfLimit;
 
-    extern Abc_Ntk_t * Abc_NtkIvyFraig( Abc_Ntk_t * pNtk, int nConfLimit, int fProve, int fVerbose );
+    extern Abc_Ntk_t * Abc_NtkIvyFraig( Abc_Ntk_t * pNtk, int nConfLimit, int fDoSparse, int fProve, int fVerbose );
 
     pNtk = Abc_FrameReadNtk(pAbc);
     pOut = Abc_FrameReadOut(pAbc);
@@ -5703,10 +5872,11 @@ int Abc_CommandIFraig( Abc_Frame_t * pAbc, int argc, char ** argv )
 
     // set defaults
     nConfLimit   = 100;   
+    fDoSparse    = 0;
     fProve       = 0;
     fVerbose     = 0;
     Extra_UtilGetoptReset();
-    while ( ( c = Extra_UtilGetopt( argc, argv, "Cpvh" ) ) != EOF )
+    while ( ( c = Extra_UtilGetopt( argc, argv, "Cspvh" ) ) != EOF )
     {
         switch ( c )
         {
@@ -5721,6 +5891,9 @@ int Abc_CommandIFraig( Abc_Frame_t * pAbc, int argc, char ** argv )
             if ( nConfLimit < 0 ) 
                 goto usage;
             break;
+        case 's':
+            fDoSparse ^= 1;
+            break;
         case 'p':
             fProve ^= 1;
             break;
@@ -5744,7 +5917,7 @@ int Abc_CommandIFraig( Abc_Frame_t * pAbc, int argc, char ** argv )
         return 1;
     }
 
-    pNtkRes = Abc_NtkIvyFraig( pNtk, nConfLimit, fProve, fVerbose );
+    pNtkRes = Abc_NtkIvyFraig( pNtk, nConfLimit, fDoSparse, fProve, fVerbose );
     if ( pNtkRes == NULL )
     {
         fprintf( pErr, "Command has failed.\n" );
@@ -5755,10 +5928,11 @@ int Abc_CommandIFraig( Abc_Frame_t * pAbc, int argc, char ** argv )
     return 0;
 
 usage:
-    fprintf( pErr, "usage: ifraig [-C num] [-pvh]\n" );
+    fprintf( pErr, "usage: ifraig [-C num] [-spvh]\n" );
     fprintf( pErr, "\t         performs fraiging using a new method\n" );
     fprintf( pErr, "\t-C num : limit on the number of conflicts [default = %d]\n", nConfLimit );
-    fprintf( pErr, "\t-p     : toggle proving miter outputs [default = %s]\n", fProve? "yes": "no" );
+    fprintf( pErr, "\t-s     : toggle considering sparse functions [default = %s]\n", fDoSparse? "yes": "no" );
+    fprintf( pErr, "\t-p     : toggle proving the miter outputs [default = %s]\n", fProve? "yes": "no" );
     fprintf( pErr, "\t-v     : toggle verbose printout [default = %s]\n", fVerbose? "yes": "no" );
     fprintf( pErr, "\t-h     : print the command usage\n");
     return 1;
@@ -6133,17 +6307,17 @@ int Abc_CommandFraig( Abc_Frame_t * pAbc, int argc, char ** argv )
     memset( pParams, 0, sizeof(Fraig_Params_t) );
     pParams->nPatsRand  = 2048; // the number of words of random simulation info
     pParams->nPatsDyna  = 2048; // the number of words of dynamic simulation info
-    pParams->nBTLimit   = 99;   // the max number of backtracks to perform
-    pParams->fFuncRed   =  1;   // performs only one level hashing
-    pParams->fFeedBack  =  1;   // enables solver feedback
-    pParams->fDist1Pats =  1;   // enables distance-1 patterns
-    pParams->fDoSparse  =  0;   // performs equiv tests for sparse functions 
-    pParams->fChoicing  =  0;   // enables recording structural choices
-    pParams->fTryProve  =  0;   // tries to solve the final miter
-    pParams->fVerbose   =  0;   // the verbosiness flag
-    pParams->fVerboseP  =  0;   // the verbosiness flag
+    pParams->nBTLimit   =  100; // the max number of backtracks to perform
+    pParams->fFuncRed   =    1; // performs only one level hashing
+    pParams->fFeedBack  =    1; // enables solver feedback
+    pParams->fDist1Pats =    1; // enables distance-1 patterns
+    pParams->fDoSparse  =    0; // performs equiv tests for sparse functions 
+    pParams->fChoicing  =    0; // enables recording structural choices
+    pParams->fTryProve  =    0; // tries to solve the final miter
+    pParams->fVerbose   =    0; // the verbosiness flag
+    pParams->fVerboseP  =    0; // the verbosiness flag
     Extra_UtilGetoptReset();
-    while ( ( c = Extra_UtilGetopt( argc, argv, "RDBrscpvaeh" ) ) != EOF )
+    while ( ( c = Extra_UtilGetopt( argc, argv, "RDCrscpvaeh" ) ) != EOF )
     {
         switch ( c )
         {
@@ -6169,10 +6343,10 @@ int Abc_CommandFraig( Abc_Frame_t * pAbc, int argc, char ** argv )
             if ( pParams->nPatsDyna < 0 ) 
                 goto usage;
             break;
-        case 'B':
+        case 'C':
             if ( globalUtilOptind >= argc )
             {
-                fprintf( pErr, "Command line switch \"-B\" should be followed by an integer.\n" );
+                fprintf( pErr, "Command line switch \"-C\" should be followed by an integer.\n" );
                 goto usage;
             }
             pParams->nBTLimit = atoi(argv[globalUtilOptind]);
@@ -6247,15 +6421,15 @@ int Abc_CommandFraig( Abc_Frame_t * pAbc, int argc, char ** argv )
 
 usage:
     sprintf( Buffer, "%d", pParams->nBTLimit );
-    fprintf( pErr, "usage: fraig [-R num] [-D num] [-B num] [-rscpvah]\n" );
+    fprintf( pErr, "usage: fraig [-R num] [-D num] [-C num] [-rscpvah]\n" );
     fprintf( pErr, "\t         transforms a logic network into a functionally reduced AIG\n" );
     fprintf( pErr, "\t-R num : number of random patterns (127 < num < 32769) [default = %d]\n",     pParams->nPatsRand );
     fprintf( pErr, "\t-D num : number of systematic patterns (127 < num < 32769) [default = %d]\n", pParams->nPatsDyna );
-    fprintf( pErr, "\t-B num : number of backtracks for one SAT problem [default = %s]\n",    pParams->nBTLimit==-1? "infinity" : Buffer );
+    fprintf( pErr, "\t-C num : number of backtracks for one SAT problem [default = %s]\n",    pParams->nBTLimit==-1? "infinity" : Buffer );
     fprintf( pErr, "\t-r     : toggle functional reduction [default = %s]\n",                 pParams->fFuncRed? "yes": "no" );
     fprintf( pErr, "\t-s     : toggle considering sparse functions [default = %s]\n",         pParams->fDoSparse? "yes": "no" );
     fprintf( pErr, "\t-c     : toggle accumulation of choices [default = %s]\n",              pParams->fChoicing? "yes": "no" );
-    fprintf( pErr, "\t-p     : toggle proving the final miter [default = %s]\n",              pParams->fTryProve? "yes": "no" );
+    fprintf( pErr, "\t-p     : toggle proving the miter outputs [default = %s]\n",              pParams->fTryProve? "yes": "no" );
     fprintf( pErr, "\t-v     : toggle verbose output [default = %s]\n",                       pParams->fVerbose?  "yes": "no" );
     fprintf( pErr, "\t-e     : toggle functional sweeping using EXDC [default = %s]\n",       fExdc? "yes": "no" );
     fprintf( pErr, "\t-a     : toggle between all nodes and DFS nodes [default = %s]\n",      fAllNodes? "all": "dfs" );
@@ -7699,7 +7873,8 @@ int Abc_CommandSeq( Abc_Frame_t * pAbc, int argc, char ** argv )
     }
 
     // get the new network
-    pNtkRes = Abc_NtkAigToSeq( pNtk );
+//    pNtkRes = Abc_NtkAigToSeq( pNtk );
+    pNtkRes = NULL;
     if ( pNtkRes == NULL )
     {
         fprintf( pErr, "Converting to sequential AIG has failed.\n" );
@@ -7772,7 +7947,8 @@ int Abc_CommandUnseq( Abc_Frame_t * pAbc, int argc, char ** argv )
 //        Seq_NtkShareFanouts(pNtk);
 
     // get the new network
-    pNtkRes = Abc_NtkSeqToLogicSop( pNtk );
+//    pNtkRes = Abc_NtkSeqToLogicSop( pNtk );
+    pNtkRes = NULL;
     if ( pNtkRes == NULL )
     {
         fprintf( pErr, "Converting sequential AIG into an SOP logic network has failed.\n" );
@@ -7804,24 +7980,26 @@ usage:
 int Abc_CommandRetime( Abc_Frame_t * pAbc, int argc, char ** argv )
 {
     FILE * pOut, * pErr;
-    Abc_Ntk_t * pNtk, * pNtkTemp;
+    Abc_Ntk_t * pNtk, * pNtkRes;
     int c, nMaxIters;
-    int fInitial;
+    int fForward;
+    int fBackward;
     int fVerbose;
     int Mode;
-    extern int Abc_NtkRetime( Abc_Ntk_t * pNtk, int Mode, int fVerbose );
+    extern int Abc_NtkRetime( Abc_Ntk_t * pNtk, int Mode, int fForwardOnly, int fBackwardOnly, int fVerbose );
 
     pNtk = Abc_FrameReadNtk(pAbc);
     pOut = Abc_FrameReadOut(pAbc);
     pErr = Abc_FrameReadErr(pAbc);
 
     // set defaults
-    Mode      = 3;
-    fInitial  = 1;
-    fVerbose  = 1;
+    Mode      =  5;
+    fForward  =  0;
+    fBackward =  0;
+    fVerbose  =  1;
     nMaxIters = 15;
     Extra_UtilGetoptReset();
-    while ( ( c = Extra_UtilGetopt( argc, argv, "Mvh" ) ) != EOF )
+    while ( ( c = Extra_UtilGetopt( argc, argv, "Mfbvh" ) ) != EOF )
     {
         switch ( c )
         {
@@ -7836,6 +8014,12 @@ int Abc_CommandRetime( Abc_Frame_t * pAbc, int argc, char ** argv )
             if ( Mode < 0 ) 
                 goto usage;
             break;
+        case 'f':
+            fForward ^= 1;
+            break;
+        case 'b':
+            fBackward ^= 1;
+            break;
         case 'v':
             fVerbose ^= 1;
             break;
@@ -7852,6 +8036,12 @@ int Abc_CommandRetime( Abc_Frame_t * pAbc, int argc, char ** argv )
         return 1;
     }
 
+    if ( fForward && fBackward )
+    {
+        fprintf( pErr, "Only one switch \"-f\" or \"-b\" can be selected at a time.\n" );
+        return 1;
+    }
+
     if ( !Abc_NtkLatchNum(pNtk) )
     {
         fprintf( pErr, "The network has no latches. Retiming is not performed.\n" );
@@ -7865,8 +8055,13 @@ int Abc_CommandRetime( Abc_Frame_t * pAbc, int argc, char ** argv )
             fprintf( pErr, "Retiming with choice nodes is not implemented.\n" );
             return 0;
         }
-        pNtk = Abc_NtkAigToLogicSop( pNtkTemp = pNtk );
-        Abc_NtkDelete( pNtkTemp );
+        // convert the network into an SOP network
+        pNtkRes = Abc_NtkAigToLogicSop( pNtk );
+        // perform the retiming
+        Abc_NtkRetime( pNtkRes, Mode, fForward, fBackward, fVerbose );
+        // replace the current network
+        Abc_FrameReplaceCurrentNetwork( pAbc, pNtkRes );
+        return 0;
     }
 
     // get the network in the SOP form
@@ -7883,19 +8078,21 @@ int Abc_CommandRetime( Abc_Frame_t * pAbc, int argc, char ** argv )
     }
 
     // perform the retiming
-    Abc_NtkRetime( pNtk, Mode, fVerbose );
+    Abc_NtkRetime( pNtk, Mode, fForward, fBackward, fVerbose );
     return 0;
 
 usage:
-    fprintf( pErr, "usage: retime [-M num] [-vh]\n" );
+    fprintf( pErr, "usage: retime [-M num] [-fbvh]\n" );
     fprintf( pErr, "\t         retimes the current network using one of the algorithms:\n" );
     fprintf( pErr, "\t             1: most forward retiming\n" );
     fprintf( pErr, "\t             2: most backward retiming\n" );
-    fprintf( pErr, "\t             3: min-area retiming\n" );
-    fprintf( pErr, "\t             4: min-delay retiming\n" );
-    fprintf( pErr, "\t             5: min-area under min-delay constraint retiming\n" );
+    fprintf( pErr, "\t             3: forward and backward min-area retiming\n" );
+    fprintf( pErr, "\t             4: forward and backward min-delay retiming\n" );
+    fprintf( pErr, "\t             5: mode 3 followed by mode 4\n" );
     fprintf( pErr, "\t-M num : the retiming algorithm to use [default = %d]\n", Mode );
-    fprintf( pErr, "\t-v     : toggles verbose output [default = %s]\n", fVerbose? "yes": "no" );
+    fprintf( pErr, "\t-f     : enables forward-only retiming in modes 3,4,5 [default = %s]\n", fForward? "yes": "no" );
+    fprintf( pErr, "\t-b     : enables backward-only retiming in modes 3,4,5 [default = %s]\n", fBackward? "yes": "no" );
+    fprintf( pErr, "\t-v     : enables verbose output [default = %s]\n", fVerbose? "yes": "no" );
     fprintf( pErr, "\t-h     : print the command usage\n");
     return 1;
 //    fprintf( pErr, "\t-I num : max number of iterations of l-value computation [default = %d]\n", nMaxIters );
@@ -7971,10 +8168,11 @@ int Abc_CommandSeqFpga( Abc_Frame_t * pAbc, int argc, char ** argv )
             return 0;
         }
 */
-        if ( Abc_NtkIsStrash(pNtk) )
-            pNtkNew = Abc_NtkAigToSeq(pNtk);
-        else
-            pNtkNew = Abc_NtkDup(pNtk);
+//        if ( Abc_NtkIsStrash(pNtk) )
+//            pNtkNew = Abc_NtkAigToSeq(pNtk);
+//        else
+//            pNtkNew = Abc_NtkDup(pNtk);
+        pNtkNew = NULL;
     }
     else
     {
@@ -7995,7 +8193,8 @@ int Abc_CommandSeqFpga( Abc_Frame_t * pAbc, int argc, char ** argv )
         }
 
         // convert into a sequential AIG
-        pNtkNew = Abc_NtkAigToSeq( pNtkRes = pNtkNew );
+//        pNtkNew = Abc_NtkAigToSeq( pNtkRes = pNtkNew );
+        pNtkNew = NULL;
         Abc_NtkDelete( pNtkRes );
         if ( pNtkNew == NULL )
         {
@@ -8007,7 +8206,8 @@ int Abc_CommandSeqFpga( Abc_Frame_t * pAbc, int argc, char ** argv )
     }
 
     // get the new network
-    pNtkRes = Seq_NtkFpgaMapRetime( pNtkNew, nMaxIters, fVerbose );
+//    pNtkRes = Seq_NtkFpgaMapRetime( pNtkNew, nMaxIters, fVerbose );
+    pNtkRes = NULL;
     if ( pNtkRes == NULL )
     {
 //        fprintf( pErr, "Sequential FPGA mapping has failed.\n" );
@@ -8095,10 +8295,11 @@ int Abc_CommandSeqMap( Abc_Frame_t * pAbc, int argc, char ** argv )
             return 0;
         }
 */
-        if ( Abc_NtkIsStrash(pNtk) )
-            pNtkNew = Abc_NtkAigToSeq(pNtk);
-        else
-            pNtkNew = Abc_NtkDup(pNtk);
+//        if ( Abc_NtkIsStrash(pNtk) )
+//            pNtkNew = Abc_NtkAigToSeq(pNtk);
+//        else
+//            pNtkNew = Abc_NtkDup(pNtk);
+        pNtkNew = NULL;
     }
     else
     {
@@ -8119,7 +8320,8 @@ int Abc_CommandSeqMap( Abc_Frame_t * pAbc, int argc, char ** argv )
         }
 
         // convert into a sequential AIG
-        pNtkNew = Abc_NtkAigToSeq( pNtkRes = pNtkNew );
+//        pNtkNew = Abc_NtkAigToSeq( pNtkRes = pNtkNew );
+        pNtkNew = NULL;
         Abc_NtkDelete( pNtkRes );
         if ( pNtkNew == NULL )
         {
@@ -8131,7 +8333,8 @@ int Abc_CommandSeqMap( Abc_Frame_t * pAbc, int argc, char ** argv )
     }
 
     // get the new network
-    pNtkRes = Seq_MapRetime( pNtkNew, nMaxIters, fVerbose );
+//    pNtkRes = Seq_MapRetime( pNtkNew, nMaxIters, fVerbose );
+    pNtkRes = NULL;
     if ( pNtkRes == NULL )
     {
 //        fprintf( pErr, "Sequential FPGA mapping has failed.\n" );
@@ -8481,7 +8684,7 @@ int Abc_CommandSec( Abc_Frame_t * pAbc, int argc, char ** argv )
     int nInsLimit;
 
     extern void Abc_NtkSecSat( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int nConfLimit, int nInsLimit, int nFrames );
-    extern void Abc_NtkSecFraig( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int nSeconds, int nFrames, int fVerbose );
+    extern int Abc_NtkSecFraig( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int nSeconds, int nFrames, int fVerbose );
 
 
     pNtk = Abc_FrameReadNtk(pAbc);
@@ -8904,6 +9107,63 @@ usage:
     return 1;
 }
 
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Abc_CommandDebug( Abc_Frame_t * pAbc, int argc, char ** argv )
+{
+    FILE * pOut, * pErr;
+    Abc_Ntk_t * pNtk;
+    int c;
+    extern void Abc_NtkAutoDebug( Abc_Ntk_t * pNtk, int (*pFuncError) (Abc_Ntk_t *) );
+    extern int Abc_NtkRetimeDebug( Abc_Ntk_t * pNtk );
+
+    pNtk = Abc_FrameReadNtk(pAbc);
+    pOut = Abc_FrameReadOut(pAbc);
+    pErr = Abc_FrameReadErr(pAbc);
+
+    // set defaults
+    Extra_UtilGetoptReset();
+    while ( ( c = Extra_UtilGetopt( argc, argv, "h" ) ) != EOF )
+    {
+        switch ( c )
+        {
+        case 'h':
+            goto usage;
+        default:
+            goto usage;
+        }
+    }
+
+    if ( pNtk == NULL )
+    {
+        fprintf( pErr, "Empty network.\n" );
+        return 1;
+    }
+    if ( !Abc_NtkIsLogic(pNtk) )
+    {
+        fprintf( pErr, "This command is applicable to logic networks.\n" );
+        return 1;
+    }
+
+    Abc_NtkAutoDebug( pNtk, Abc_NtkRetimeDebug );
+    return 0;
+
+usage:
+    fprintf( pErr, "usage: debug [-h]\n" );
+    fprintf( pErr, "\t        performs automated debugging of the given procedure\n" );
+    fprintf( pErr, "\t-h    : print the command usage\n");
+    return 1;
+}
+
 
 /**Function*************************************************************
 
@@ -9101,7 +9361,8 @@ int Abc_CommandHoward( Abc_Frame_t * pAbc, int argc, char ** argv )
         return 0;
     }
 
-    result = Seq_NtkHoward( pNtk, fVerbose );
+//    result = Seq_NtkHoward( pNtk, fVerbose );
+    result = 0;
 
     if (result < 0) {
       fprintf( pErr, "Analysis failed.\n" );
@@ -9178,7 +9439,7 @@ int Abc_CommandSkewForward( Abc_Frame_t * pAbc, int argc, char ** argv )
         return 0;
     }
 
-    Seq_NtkSkewForward( pNtk, target, fMinimize );
+//    Seq_NtkSkewForward( pNtk, target, fMinimize );
 
     return 1;
 
diff --git a/src/base/abci/abcCut.c b/src/base/abci/abcCut.c
index 7024a970..c021728a 100644
--- a/src/base/abci/abcCut.c
+++ b/src/base/abci/abcCut.c
@@ -20,7 +20,7 @@
 
 #include "abc.h"
 #include "cut.h"
-#include "seqInt.h"
+//#include "seqInt.h"
 
 ////////////////////////////////////////////////////////////////////////
 ///                        DECLARATIONS                              ///
@@ -401,6 +401,7 @@ void * Abc_NodeGetCuts( void * p, Abc_Obj_t * pObj, int fDag, int fTree )
 ***********************************************************************/
 void Abc_NodeGetCutsSeq( void * p, Abc_Obj_t * pObj, int fTriv )
 {
+/*
     int CutSetNum;
     assert( Abc_NtkIsSeq(pObj->pNtk) );
     assert( Abc_ObjFaninNum(pObj) == 2 );
@@ -408,6 +409,7 @@ void Abc_NodeGetCutsSeq( void * p, Abc_Obj_t * pObj, int fTriv )
     CutSetNum = pObj->fMarkC ? (int)pObj->pCopy : -1;
     Cut_NodeComputeCutsSeq( p, pObj->Id, Abc_ObjFaninId0(pObj), Abc_ObjFaninId1(pObj),  
         Abc_ObjFaninC0(pObj), Abc_ObjFaninC1(pObj), Seq_ObjFaninL0(pObj), Seq_ObjFaninL1(pObj), fTriv, CutSetNum );  
+*/
 }
 
 /**Function*************************************************************
diff --git a/src/base/abci/abcDebug.c b/src/base/abci/abcDebug.c
new file mode 100644
index 00000000..4d37c496
--- /dev/null
+++ b/src/base/abci/abcDebug.c
@@ -0,0 +1,198 @@
+/**CFile****************************************************************
+
+  FileName    [abcDebug.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [Network and node package.]
+
+  Synopsis    [Automated debugging procedures.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - June 20, 2005.]
+
+  Revision    [$Id: abcDebug.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "abc.h"
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+static int Abc_NtkCountFaninsTotal( Abc_Ntk_t * pNtk );
+static Abc_Ntk_t * Abc_NtkAutoDebugModify( Abc_Ntk_t * pNtk, int ObjNum, int fConst1 );
+
+extern void Io_WriteBlifLogic( Abc_Ntk_t * pNtk, char * FileName, int fWriteLatches );
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    [Takes a network and a procedure to test.]
+
+  Description [The network demonstrates the bug in the procedure.
+  Procedure should return 1 if the bug is demonstrated.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Abc_NtkAutoDebug( Abc_Ntk_t * pNtk, int (*pFuncError) (Abc_Ntk_t *) )
+{
+    Abc_Ntk_t * pNtkMod;
+    char * pFileName = "bug_found.blif";
+    int i, nSteps, nIter, ModNum, RandNum = 1, clk, clkTotal = clock();
+    assert( Abc_NtkIsLogic(pNtk) );
+    srand( 0x123123 );
+    // create internal copy of the network
+    pNtk = Abc_NtkDup(pNtk);
+    if ( !(*pFuncError)( pNtk ) )
+    {
+        printf( "The original network does not cause the bug. Quitting.\n" );
+        Abc_NtkDelete( pNtk );
+        return;
+    }
+    // perform incremental modifications
+    for ( nIter = 0; ; nIter++ )
+    {
+        clk = clock();
+        // count how many ways of modifying the network exists
+        nSteps = 2 * Abc_NtkCountFaninsTotal(pNtk);
+        // try modifying the network as many times
+        RandNum ^= rand();
+        for ( i = 0; i < nSteps; i++ )
+        {
+            // get the shifted number of bug
+            ModNum = (i + RandNum) % nSteps;
+            // get the modified network
+            pNtkMod = Abc_NtkAutoDebugModify( pNtk, ModNum/2, ModNum%2 );
+            // write the network
+            Io_WriteBlifLogic( pNtk, "bug_temp.blif", 1 );   
+            // check if the bug is still there
+            if ( (*pFuncError)( pNtkMod ) ) // bug is still there
+            {
+                Abc_NtkDelete( pNtk );
+                pNtk = pNtkMod;
+                break;
+            }
+            else // no bug
+                Abc_NtkDelete( pNtkMod );
+        }
+        printf( "Iteration %6d : Nodes = %6d. Steps = %6d. Error step = %3d.  ", nIter, Abc_NtkObjNum(pNtk), nSteps, i );
+        PRT( "Time", clock() - clk );
+        if ( i == nSteps ) // could not modify it while preserving the bug
+            break;
+    }
+    // write out the final network
+    Io_WriteBlifLogic( pNtk, pFileName, 1 );
+    printf( "Final network written into file \"%s\". ", pFileName );
+    PRT( "Total time", clock() - clkTotal );
+    Abc_NtkDelete( pNtk );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Counts the total number of fanins.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Abc_NtkCountFaninsTotal( Abc_Ntk_t * pNtk )
+{
+    Abc_Obj_t * pObj, * pFanin;
+    int i, k, Counter = 0;
+    Abc_NtkForEachObj( pNtk, pObj, i )
+        Abc_ObjForEachFanin( pObj, pFanin, k )
+        {
+            if ( Abc_NodeIsConst(pFanin) )
+                continue;
+            Counter++;
+        }
+    return Counter;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Returns the node and fanin to be modified.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Abc_NtkFindGivenFanin( Abc_Ntk_t * pNtk, int Step, Abc_Obj_t ** ppObj, Abc_Obj_t ** ppFanin )
+{
+    Abc_Obj_t * pObj, * pFanin;
+    int i, k, Counter = 0;
+    Abc_NtkForEachObj( pNtk, pObj, i )
+        Abc_ObjForEachFanin( pObj, pFanin, k )
+        {
+            if ( Abc_NodeIsConst(pFanin) )
+                continue;
+            if ( Counter++ == Step )
+            {
+                *ppObj   = pObj;
+                *ppFanin = pFanin;
+                return 1;
+            }
+        }
+    return 0;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Perform modification with the given number.]
+
+  Description [Modification consists of replacing the node by a constant.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Abc_Ntk_t * Abc_NtkAutoDebugModify( Abc_Ntk_t * pNtkInit, int Step, int fConst1 )
+{
+    Abc_Ntk_t * pNtk;
+    Abc_Obj_t * pObj, * pFanin, * pConst;
+    // copy the network
+    pNtk = Abc_NtkDup( pNtkInit );
+    assert( Abc_NtkNodeNum(pNtk) == Abc_NtkNodeNum(pNtkInit) );
+    // find the object number
+    Abc_NtkFindGivenFanin( pNtk, Step, &pObj, &pFanin );
+    // consider special case 
+    if ( Abc_ObjIsPo(pObj) && Abc_NodeIsConst(pFanin) )
+    {
+        Abc_NtkDeleteAll_rec( pObj );
+        return pNtk;
+    }
+    // plug in a constant node
+    pConst = fConst1? Abc_NtkCreateNodeConst1(pNtk) : Abc_NtkCreateNodeConst0(pNtk);
+    Abc_ObjTransferFanout( pFanin, pConst );
+    Abc_NtkDeleteAll_rec( pFanin );
+
+    Abc_NtkSweep( pNtk, 0 );
+    Abc_NtkCleanupSeq( pNtk, 0 );
+    Abc_NtkLogicToSop( pNtk, 0 );
+    Abc_NtkCycleInitStateSop( pNtk, 20, 0 );
+    return pNtk;
+}
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/base/abci/abcIvy.c b/src/base/abci/abcIvy.c
index 446eb0cc..30ed21cf 100644
--- a/src/base/abci/abcIvy.c
+++ b/src/base/abci/abcIvy.c
@@ -84,7 +84,7 @@ Ivy_Man_t * Abc_NtkIvyBefore( Abc_Ntk_t * pNtk, int fSeq, int fUseDc )
     }
     if ( fSeq && Abc_NtkCountSelfFeedLatches(pNtk) )
     {
-        printf( "Warning: The network has %d self-feeding latches. Quitting.\n", Abc_NtkCountSelfFeedLatches(pNtk) );
+        printf( "Warning: The network has %d self-feeding latches.\n", Abc_NtkCountSelfFeedLatches(pNtk) );
 //        return NULL;
     }
     // print warning about choice nodes
@@ -369,7 +369,7 @@ Abc_Ntk_t * Abc_NtkIvySat( Abc_Ntk_t * pNtk, int nConfLimit, int fVerbose )
   SeeAlso     []
 
 ***********************************************************************/
-Abc_Ntk_t * Abc_NtkIvyFraig( Abc_Ntk_t * pNtk, int nConfLimit, int fProve, int fVerbose )
+Abc_Ntk_t * Abc_NtkIvyFraig( Abc_Ntk_t * pNtk, int nConfLimit, int fDoSparse, int fProve, int fVerbose )
 {
     Ivy_FraigParams_t Params, * pParams = &Params; 
     Abc_Ntk_t * pNtkAig;
@@ -379,8 +379,9 @@ Abc_Ntk_t * Abc_NtkIvyFraig( Abc_Ntk_t * pNtk, int nConfLimit, int fProve, int f
         return NULL;
     Ivy_FraigParamsDefault( pParams );
     pParams->nBTLimitNode = nConfLimit;
-    pParams->fVerbose = fVerbose;
-    pParams->fProve = fProve;
+    pParams->fVerbose     = fVerbose;
+    pParams->fProve       = fProve;
+    pParams->fDoSparse    = fDoSparse;
     pMan = Ivy_FraigPerform( pTemp = pMan, pParams );
     Ivy_ManStop( pTemp );
     pNtkAig = Abc_NtkIvyAfter( pNtk, pMan, 0, 0 );
@@ -668,8 +669,8 @@ Abc_Ntk_t * Abc_NtkFromAigSeq( Abc_Ntk_t * pNtkOld, Ivy_Man_t * pMan, int fHaig
     Ivy_ManForEachNodeVec( pMan, vLatches, pNode, i )
     {
         pObjNew = Abc_NtkCreateLatch( pNtk );
-        pFaninNew0 = Abc_NtkCreateBo( pNtk );
-        pFaninNew1 = Abc_NtkCreateBi( pNtk );
+        pFaninNew0 = Abc_NtkCreateBi( pNtk );
+        pFaninNew1 = Abc_NtkCreateBo( pNtk );
         Abc_ObjAddFanin( pObjNew, pFaninNew0 );
         Abc_ObjAddFanin( pFaninNew1, pObjNew );
         if ( fHaig || Ivy_ObjInit(pNode) == IVY_INIT_DC )
diff --git a/src/base/abci/abcNtbdd.c b/src/base/abci/abcNtbdd.c
index a1f6b9f9..f99f7bce 100644
--- a/src/base/abci/abcNtbdd.c
+++ b/src/base/abci/abcNtbdd.c
@@ -343,7 +343,7 @@ DdManager * Abc_NtkGlobalBdds( Abc_Ntk_t * pNtk, int nBddSizeMax, int fLatchOnly
 */
     // reset references
     Abc_NtkForEachObj( pNtk, pObj, i )
-        if ( !Abc_ObjIsBox(pObj) && !Abc_ObjIsBi(pObj) )
+        if ( !Abc_ObjIsBox(pObj) && !Abc_ObjIsBo(pObj) )
             Abc_ObjForEachFanin( pObj, pFanin, k )
                 pFanin->vFanouts.nSize++;
 
diff --git a/src/base/abci/abcPrint.c b/src/base/abci/abcPrint.c
index 6af12afd..bdca4a8e 100644
--- a/src/base/abci/abcPrint.c
+++ b/src/base/abci/abcPrint.c
@@ -22,7 +22,7 @@
 #include "dec.h"
 #include "main.h"
 #include "mio.h"
-#include "seq.h"
+//#include "seq.h"
 
 ////////////////////////////////////////////////////////////////////////
 ///                        DECLARATIONS                              ///
@@ -142,7 +142,7 @@ void Abc_NtkPrintStats( FILE * pFile, Abc_Ntk_t * pNtk, int fFactored )
         fprintf( pTable, "\n" );
         fclose( pTable );
     }
-*/
+*/ 
 
 /*
     // print the statistic into a file
@@ -162,14 +162,22 @@ void Abc_NtkPrintStats( FILE * pFile, Abc_Ntk_t * pNtk, int fFactored )
 /*
     // print the statistic into a file
     {
+        static int Counter = 0;
+        extern int timeRetime;
         FILE * pTable;
-        pTable = fopen( "stats.txt", "a+" );
-        fprintf( pTable, "%s ",  pNtk->pName );
+        Counter++;
+        pTable = fopen( "sap/stats_retime.txt", "a+" );
+        fprintf( pTable, "%s ", pNtk->pName );
+        fprintf( pTable, "%d ", Abc_NtkNodeNum(pNtk) );
         fprintf( pTable, "%d ", Abc_NtkLatchNum(pNtk) );
-        fprintf( pTable, "\n" );
+        fprintf( pTable, "%d ", Abc_NtkGetLevelNum(pNtk) );
+        fprintf( pTable, "%.2f ", (float)(timeRetime)/(float)(CLOCKS_PER_SEC) );
+        if ( Counter % 4 == 0 )
+            fprintf( pTable, "\n" );
         fclose( pTable );
     }
 */
+
 /*
     s_TotalNodes += Abc_NtkNodeNum(pNtk);
     printf( "Total nodes = %6d   %6.2f Mb   Changes = %6d.\n", 
@@ -254,8 +262,18 @@ void Abc_NtkPrintLatch( FILE * pFile, Abc_Ntk_t * pNtk )
         InitNums[Init]++;
 
         pFanin = Abc_ObjFanin0(Abc_ObjFanin0(pLatch));
-        if ( !Abc_ObjIsNode(pFanin) || !Abc_NodeIsConst(pFanin) )
-            continue;
+        if ( Abc_NtkIsLogic(pNtk) )
+        {
+            if ( !Abc_NodeIsConst(pFanin) )
+                continue;
+        }
+        else if ( Abc_NtkIsStrash(pNtk) )
+        {
+            if ( !Abc_AigNodeIsConst(pFanin) )
+                continue;
+        }
+        else
+            assert( 0 );
 
         // the latch input is a constant node
         Counter0++;
diff --git a/src/base/abci/abcResub.c b/src/base/abci/abcResub.c
index 61be3dee..9fcc6979 100644
--- a/src/base/abci/abcResub.c
+++ b/src/base/abci/abcResub.c
@@ -147,9 +147,9 @@ int Abc_NtkResubstitute( Abc_Ntk_t * pNtk, int nCutMax, int nStepsMax, bool fUpd
     if ( fUpdateLevel )
         Abc_NtkStartReverseLevels( pNtk );
 
-//    if ( Abc_NtkLatchNum(pNtk) )
-//        Abc_NtkForEachLatch(pNtk, pNode, i)
-//            pNode->pNext = pNode->pData;
+    if ( Abc_NtkLatchNum(pNtk) )
+        Abc_NtkForEachLatch(pNtk, pNode, i)
+            pNode->pNext = pNode->pData;
 
     // resynthesize each node once
     nNodes = Abc_NtkObjNumMax(pNtk);
@@ -221,9 +221,9 @@ pManRes->timeTotal = clock() - clkStart;
     Abc_NtkForEachObj( pNtk, pNode, i )
         pNode->pData = NULL;
 
-//    if ( Abc_NtkLatchNum(pNtk) )
-//        Abc_NtkForEachLatch(pNtk, pNode, i)
-//            pNode->pData = pNode->pNext, pNode->pNext = NULL;
+    if ( Abc_NtkLatchNum(pNtk) )
+        Abc_NtkForEachLatch(pNtk, pNode, i)
+            pNode->pData = pNode->pNext, pNode->pNext = NULL;
 
     // put the nodes into the DFS order and reassign their IDs
     Abc_NtkReassignIds( pNtk );
diff --git a/src/base/abci/abcSweep.c b/src/base/abci/abcSweep.c
index 076bee46..db926d17 100644
--- a/src/base/abci/abcSweep.c
+++ b/src/base/abci/abcSweep.c
@@ -860,7 +860,7 @@ int Abc_NtkReplaceAutonomousLogic( Abc_Ntk_t * pNtk )
                 continue;
             // skip constants and latches fed by constants
             if ( Abc_NtkCheckConstant_rec(pFanin) != -1 ||
-                 (Abc_ObjIsBi(pFanin) && Abc_NtkCheckConstant_rec(Abc_ObjFanin0(Abc_ObjFanin0(pFanin))) != -1) )
+                 (Abc_ObjIsBo(pFanin) && Abc_NtkCheckConstant_rec(Abc_ObjFanin0(Abc_ObjFanin0(pFanin))) != -1) )
             {
                 Abc_NtkSetTravId_rec( pFanin );
                 continue;
@@ -874,6 +874,7 @@ int Abc_NtkReplaceAutonomousLogic( Abc_Ntk_t * pNtk )
     Vec_PtrForEachEntry( vNodes, pNode, i )
     {
         pFanin = Abc_NtkCreatePi(pNtk);
+        Abc_ObjAssignName( pFanin, Abc_ObjName(pFanin), NULL );
         Abc_NodeSetTravIdCurrent( pFanin );
         Abc_ObjTransferFanout( pNode, pFanin );
     }
diff --git a/src/base/abci/abcUnreach.c b/src/base/abci/abcUnreach.c
index cced1c47..e4873986 100644
--- a/src/base/abci/abcUnreach.c
+++ b/src/base/abci/abcUnreach.c
@@ -95,7 +95,7 @@ int Abc_NtkExtractSequentialDcs( Abc_Ntk_t * pNtk, bool fVerbose )
     pNtk->pManGlob = NULL;
 
     // make sure that everything is okay
-    if ( !Abc_NtkCheck( pNtk->pExdc ) )
+    if ( pNtk->pExdc && !Abc_NtkCheck( pNtk->pExdc ) )
     {
         printf( "Abc_NtkExtractSequentialDcs: The network check has failed.\n" );
         Abc_NtkDelete( pNtk->pExdc );
diff --git a/src/base/abci/abcVerify.c b/src/base/abci/abcVerify.c
index 594cc2d6..ad58e35c 100644
--- a/src/base/abci/abcVerify.c
+++ b/src/base/abci/abcVerify.c
@@ -286,7 +286,7 @@ void Abc_NtkSecSat( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int nConfLimit, int nI
   SeeAlso     []
 
 ***********************************************************************/
-void Abc_NtkSecFraig( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int nSeconds, int nFrames, int fVerbose )
+int Abc_NtkSecFraig( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int nSeconds, int nFrames, int fVerbose )
 {
     Fraig_Params_t Params;
     Fraig_Man_t * pMan;
@@ -299,7 +299,7 @@ void Abc_NtkSecFraig( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int nSeconds, int nF
     if ( pMiter == NULL )
     {
         printf( "Miter computation has failed.\n" );
-        return;
+        return 0;
     }
     RetValue = Abc_NtkMiterIsConstant( pMiter );
     if ( RetValue == 0 )
@@ -310,13 +310,13 @@ void Abc_NtkSecFraig( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int nSeconds, int nF
         Abc_NtkVerifyReportErrorSeq( pNtk1, pNtk2, pMiter->pModel, nFrames );
         FREE( pMiter->pModel );
         Abc_NtkDelete( pMiter );
-        return;
+        return 0;
     }
     if ( RetValue == 1 )
     {
         Abc_NtkDelete( pMiter );
         printf( "Networks are equivalent after structural hashing.\n" );
-        return;
+        return 1;
     }
 
     // create the timeframes
@@ -325,7 +325,7 @@ void Abc_NtkSecFraig( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int nSeconds, int nF
     if ( pFrames == NULL )
     {
         printf( "Frames computation has failed.\n" );
-        return;
+        return 0;
     }
     RetValue = Abc_NtkMiterIsConstant( pFrames );
     if ( RetValue == 0 )
@@ -336,13 +336,13 @@ void Abc_NtkSecFraig( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int nSeconds, int nF
 //        Abc_NtkVerifyReportErrorSeq( pNtk1, pNtk2, pFrames->pModel, nFrames );
         FREE( pFrames->pModel );
         Abc_NtkDelete( pFrames );
-        return;
+        return 0;
     }
     if ( RetValue == 1 )
     {
         Abc_NtkDelete( pFrames );
         printf( "Networks are equivalent after framing.\n" );
-        return;
+        return 1;
     }
 
     // convert the miter into a FRAIG
@@ -372,6 +372,7 @@ void Abc_NtkSecFraig( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int nSeconds, int nF
     Fraig_ManFree( pMan );
     // delete the miter
     Abc_NtkDelete( pFrames );
+    return RetValue == 1;
 }
 
 /**Function*************************************************************
diff --git a/src/base/abci/abcXsim.c b/src/base/abci/abcXsim.c
index 1d56ba36..d17ab1dd 100644
--- a/src/base/abci/abcXsim.c
+++ b/src/base/abci/abcXsim.c
@@ -24,9 +24,9 @@
 ///                        DECLARATIONS                              ///
 ////////////////////////////////////////////////////////////////////////
 
-#define XVS0   1
-#define XVS1   2
-#define XVSX   3
+#define XVS0   ABC_INIT_ZERO
+#define XVS1   ABC_INIT_ONE
+#define XVSX   ABC_INIT_DC
 
 static inline void Abc_ObjSetXsim( Abc_Obj_t * pObj, int Value )  { pObj->pCopy = (void *)Value;  }
 static inline int  Abc_ObjGetXsim( Abc_Obj_t * pObj )             { return (int)pObj->pCopy;      }
@@ -157,6 +157,49 @@ void Abc_NtkXValueSimulate( Abc_Ntk_t * pNtk, int nFrames, int fInputs, int fVer
     }
 }
 
+/**Function*************************************************************
+
+  Synopsis    [Cycles the circuit to create a new initial state.]
+
+  Description [Simulates the circuit with random input for the given 
+  number of timeframes to get a better initial state.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Abc_NtkCycleInitState( Abc_Ntk_t * pNtk, int nFrames, int fVerbose )
+{
+    Abc_Obj_t * pObj;
+    int i, f;
+    assert( Abc_NtkIsStrash(pNtk) );
+    srand( 0x12341234 );
+    // initialize the values
+    Abc_ObjSetXsim( Abc_AigConst1(pNtk), XVS1 );
+    Abc_NtkForEachPi( pNtk, pObj, i )
+        Abc_ObjSetXsim( pObj, Abc_XsimRand2() );
+    Abc_NtkForEachLatch( pNtk, pObj, i )
+        Abc_ObjSetXsim( Abc_ObjFanout0(pObj), Abc_LatchIsInit1(pObj)? XVS1 : XVS0 );
+    // simulate for the given number of timeframes
+    for ( f = 0; f < nFrames; f++ )
+    {
+        Abc_AigForEachAnd( pNtk, pObj, i )
+            Abc_ObjSetXsim( pObj, Abc_XsimAnd(Abc_ObjGetXsimFanin0(pObj), Abc_ObjGetXsimFanin1(pObj)) );
+        Abc_NtkForEachCo( pNtk, pObj, i )
+            Abc_ObjSetXsim( pObj, Abc_ObjGetXsimFanin0(pObj) );
+        // assign input values
+        Abc_NtkForEachPi( pNtk, pObj, i )
+            Abc_ObjSetXsim( pObj, Abc_XsimRand2() );
+        // transfer the latch values
+        Abc_NtkForEachLatch( pNtk, pObj, i )
+            Abc_ObjSetXsim( Abc_ObjFanout0(pObj), Abc_ObjGetXsim(Abc_ObjFanin0(pObj)) );
+    }
+    // set the final values
+    Abc_NtkForEachLatch( pNtk, pObj, i )
+        pObj->pData = (void *)Abc_ObjGetXsim(Abc_ObjFanout0(pObj));
+}
+
 ///////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/base/abci/module.make b/src/base/abci/module.make
index 50a40393..7db26629 100644
--- a/src/base/abci/module.make
+++ b/src/base/abci/module.make
@@ -6,6 +6,7 @@ SRC +=    src/base/abci/abc.c \
     src/base/abci/abcClpBdd.c \
     src/base/abci/abcClpSop.c \
     src/base/abci/abcCut.c \
+    src/base/abci/abcDebug.c \
     src/base/abci/abcDsd.c \
     src/base/abci/abcEspresso.c \
     src/base/abci/abcExtract.c \
diff --git a/src/base/io/io.c b/src/base/io/io.c
index 9c1b94ab..7a661664 100644
--- a/src/base/io/io.c
+++ b/src/base/io/io.c
@@ -40,6 +40,7 @@ static int IoCommandReadTruth   ( Abc_Frame_t * pAbc, int argc, char **argv );
 static int IoCommandWriteBaf    ( Abc_Frame_t * pAbc, int argc, char **argv );
 static int IoCommandWriteBlif   ( Abc_Frame_t * pAbc, int argc, char **argv );
 static int IoCommandWriteBench  ( Abc_Frame_t * pAbc, int argc, char **argv );
+static int IoCommandWriteCellNet( Abc_Frame_t * pAbc, int argc, char **argv );
 static int IoCommandWriteCnf    ( Abc_Frame_t * pAbc, int argc, char **argv );
 static int IoCommandWriteDot    ( Abc_Frame_t * pAbc, int argc, char **argv );
 static int IoCommandWriteEqn    ( Abc_Frame_t * pAbc, int argc, char **argv );
@@ -84,6 +85,7 @@ void Io_Init( Abc_Frame_t * pAbc )
     Cmd_CommandAdd( pAbc, "I/O", "write_baf",     IoCommandWriteBaf,     0 );
     Cmd_CommandAdd( pAbc, "I/O", "write_blif",    IoCommandWriteBlif,    0 );
     Cmd_CommandAdd( pAbc, "I/O", "write_bench",   IoCommandWriteBench,   0 );
+    Cmd_CommandAdd( pAbc, "I/O", "write_cellnet", IoCommandWriteCellNet, 0 );
     Cmd_CommandAdd( pAbc, "I/O", "write_cnf",     IoCommandWriteCnf,     0 );
     Cmd_CommandAdd( pAbc, "I/O", "write_dot",     IoCommandWriteDot,     0 );
     Cmd_CommandAdd( pAbc, "I/O", "write_eqn",     IoCommandWriteEqn,     0 );
@@ -1189,6 +1191,68 @@ usage:
   SeeAlso     []
 
 ***********************************************************************/
+int IoCommandWriteCellNet( Abc_Frame_t * pAbc, int argc, char **argv )
+{
+    Abc_Ntk_t * pNtk;
+    char * FileName;
+    int c;
+    extern void Io_WriteCellNet( Abc_Ntk_t * pNtk, char * pFileName );
+
+    Extra_UtilGetoptReset();
+    while ( ( c = Extra_UtilGetopt( argc, argv, "h" ) ) != EOF )
+    {
+        switch ( c )
+        {
+            case 'h':
+                goto usage;
+            default:
+                goto usage;
+        }
+    }
+
+    pNtk = pAbc->pNtkCur;
+    if ( pNtk == NULL )
+    {
+        fprintf( pAbc->Out, "Empty network.\n" );
+        return 0;
+    }
+
+    if ( argc != globalUtilOptind + 1 )
+    {
+        goto usage;
+    }
+    // get the input file name
+    FileName = argv[globalUtilOptind];
+
+    if ( !Abc_NtkIsLogic(pNtk) )
+    {
+        fprintf( pAbc->Out, "The network should be a logic network (if it an AIG, use command \"logic\")\n" );
+        return 0;
+    }
+
+    // derive the netlist
+    Io_WriteCellNet( pNtk, FileName );
+    return 0;
+
+usage:
+    fprintf( pAbc->Err, "usage: write_cellnet [-h] <file>\n" );
+    fprintf( pAbc->Err, "\t         write the network is the cellnet format\n" );
+    fprintf( pAbc->Err, "\t-h     : print the help massage\n" );
+    fprintf( pAbc->Err, "\tfile   : the name of the file to write\n" );
+    return 1;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
 int IoCommandWriteCnf( Abc_Frame_t * pAbc, int argc, char **argv )
 {
     char * FileName;
diff --git a/src/base/io/ioReadBaf.c b/src/base/io/ioReadBaf.c
index 15d75ba8..a6e0c2e2 100644
--- a/src/base/io/ioReadBaf.c
+++ b/src/base/io/ioReadBaf.c
@@ -100,10 +100,10 @@ Abc_Ntk_t * Io_ReadBaf( char * pFileName, int fCheck )
         pObj = Abc_NtkCreateLatch(pNtkNew);
         Abc_ObjAssignName( pObj, pCur, NULL );  while ( *pCur++ ); 
 
-        pNode0 = Abc_NtkCreateBo(pNtkNew);
+        pNode0 = Abc_NtkCreateBi(pNtkNew);
         Abc_ObjAssignName( pNode0, pCur, NULL );  while ( *pCur++ ); 
 
-        pNode1 = Abc_NtkCreateBi(pNtkNew);
+        pNode1 = Abc_NtkCreateBo(pNtkNew);
         Abc_ObjAssignName( pNode1, pCur, NULL );  while ( *pCur++ ); 
         Vec_PtrPush( vNodes, pNode1 );
 
diff --git a/src/base/io/ioReadBench.c b/src/base/io/ioReadBench.c
index aa7f82e3..72dd2b52 100644
--- a/src/base/io/ioReadBench.c
+++ b/src/base/io/ioReadBench.c
@@ -142,6 +142,8 @@ Abc_Ntk_t * Io_ReadBenchNetwork( Extra_FileReader_t * p )
                     Abc_ObjSetData( pNode, Abc_SopCreateBuf(pNtk->pManFunc) );
                 else if ( strcmp(pType, "NOT") == 0 )
                     Abc_ObjSetData( pNode, Abc_SopCreateInv(pNtk->pManFunc) );
+                else if ( strncmp(pType, "MUX", 3) == 0 )
+                    Abc_ObjSetData( pNode, Abc_SopRegister(pNtk->pManFunc, "1-0 1\n-11 1\n") );
                 else 
                 {
                     printf( "Cannot determine gate type \"%s\" in line %d.\n", pType, Extra_FileReaderGetLineNumber(p, 0) );
diff --git a/src/base/io/ioReadBlif.c b/src/base/io/ioReadBlif.c
index 8b7e015b..d7f456ff 100644
--- a/src/base/io/ioReadBlif.c
+++ b/src/base/io/ioReadBlif.c
@@ -354,7 +354,7 @@ int Io_ReadBlifNetworkAsserts( Io_ReadBlif_t * p, Vec_Ptr_t * vTokens )
 
 ***********************************************************************/
 int Io_ReadBlifNetworkLatch( Io_ReadBlif_t * p, Vec_Ptr_t * vTokens )
-{
+{ 
     Abc_Ntk_t * pNtk = p->pNtkCur;
     Abc_Obj_t * pLatch;
     int ResetValue;
diff --git a/src/base/io/ioUtil.c b/src/base/io/ioUtil.c
index f2f07b14..dff27dd1 100644
--- a/src/base/io/ioUtil.c
+++ b/src/base/io/ioUtil.c
@@ -120,13 +120,13 @@ Abc_Obj_t * Io_ReadCreateLatch( Abc_Ntk_t * pNtk, char * pNetLI, char * pNetLO )
     // get the LI net
     pNet = Abc_NtkFindOrCreateNet( pNtk, pNetLI );
     // add the BO terminal
-    pTerm = Abc_NtkCreateBo( pNtk );
+    pTerm = Abc_NtkCreateBi( pNtk );
     Abc_ObjAddFanin( pTerm, pNet );
     // add the latch box
     pLatch = Abc_NtkCreateLatch( pNtk );
     Abc_ObjAddFanin( pLatch, pTerm  );
     // add the BI terminal
-    pTerm = Abc_NtkCreateBi( pNtk );
+    pTerm = Abc_NtkCreateBo( pNtk );
     Abc_ObjAddFanin( pTerm, pLatch );
     // get the LO net
     pNet = Abc_NtkFindOrCreateNet( pNtk, pNetLO );
diff --git a/src/base/io/ioWriteDot.c b/src/base/io/ioWriteDot.c
index 05539c40..3cc3fcfe 100644
--- a/src/base/io/ioWriteDot.c
+++ b/src/base/io/ioWriteDot.c
@@ -19,7 +19,9 @@
 ***********************************************************************/
 
 #include "io.h"
-#include "seqInt.h"
+#include "main.h"
+#include "mio.h"
+//#include "seqInt.h"
 
 ////////////////////////////////////////////////////////////////////////
 ///                        DECLARATIONS                              ///
@@ -292,6 +294,10 @@ void Io_WriteDotAig( Abc_Ntk_t * pNtk, Vec_Ptr_t * vNodes, Vec_Ptr_t * vNodesSho
     {
         if ( Abc_ObjFaninNum(pNode) == 0 )
             continue;
+
+        if ( Abc_ObjIsBo(pNode) )
+            continue;
+
         if ( fMulti && Abc_ObjIsNode(pNode) )
         {
             Vec_Ptr_t * vSuper;
@@ -305,6 +311,10 @@ void Io_WriteDotAig( Abc_Ntk_t * pNtk, Vec_Ptr_t * vNodes, Vec_Ptr_t * vNodesSho
                 pFanin = Abc_ObjRegular(pFanin);
                 if ( !pFanin->fMarkC )
                     continue;
+
+                if ( Abc_ObjIsBi(pFanin) )
+                    continue;
+
                 fprintf( pFile, "Node%d",  pNode->Id );
                 fprintf( pFile, " -> " );
                 fprintf( pFile, "Node%d%s",  pFanin->Id, (Abc_ObjIsLatch(pFanin)? "_out":"") );
@@ -316,7 +326,7 @@ void Io_WriteDotAig( Abc_Ntk_t * pNtk, Vec_Ptr_t * vNodes, Vec_Ptr_t * vNodesSho
             continue;
         }
         // generate the edge from this node to the next
-        if ( Abc_ObjFanin0(pNode)->fMarkC )
+        if ( Abc_ObjFanin0(pNode)->fMarkC && !Abc_ObjIsBi(Abc_ObjFanin0(pNode)) )
         {
             fprintf( pFile, "Node%d%s",  pNode->Id, (Abc_ObjIsLatch(pNode)? "_in":"") );
             fprintf( pFile, " -> " );
@@ -331,7 +341,7 @@ void Io_WriteDotAig( Abc_Ntk_t * pNtk, Vec_Ptr_t * vNodes, Vec_Ptr_t * vNodesSho
         if ( Abc_ObjFaninNum(pNode) == 1 )
             continue;
         // generate the edge from this node to the next
-        if ( Abc_ObjFanin1(pNode)->fMarkC )
+        if ( Abc_ObjFanin1(pNode)->fMarkC && !Abc_ObjIsBi(Abc_ObjFanin1(pNode)) )
         {
             fprintf( pFile, "Node%d",  pNode->Id );
             fprintf( pFile, " -> " );
@@ -392,7 +402,7 @@ void Io_WriteDotNtk( Abc_Ntk_t * pNtk, Vec_Ptr_t * vNodes, Vec_Ptr_t * vNodesSho
     int LevelMin, LevelMax, fHasCos, Level, i, k, fHasBdds;
     int Limit = 300;
 
-    assert( !Abc_NtkHasAig(pNtk) );
+    assert( !Abc_NtkIsStrash(pNtk) );
 
     if ( vNodes->nSize < 1 )
     {
@@ -606,7 +616,7 @@ void Io_WriteDotNtk( Abc_Ntk_t * pNtk, Vec_Ptr_t * vNodes, Vec_Ptr_t * vNodesSho
         fprintf( pFile, "  rank = same;\n" );
         // the labeling node of this level
         fprintf( pFile, "  Level%d;\n",  LevelMin );
-        // generat the PO nodes
+        // generate the PO nodes
         Vec_PtrForEachEntry( vNodes, pNode, i )
         {
             if ( !Abc_ObjIsCi(pNode) )
@@ -653,6 +663,11 @@ void Io_WriteDotNtk( Abc_Ntk_t * pNtk, Vec_Ptr_t * vNodes, Vec_Ptr_t * vNodesSho
         {
             if ( !Abc_ObjFanin0(pNode)->fMarkC )
                 continue;
+
+            // added to fix the bug after adding boxes
+            if ( Abc_ObjIsBo(pNode) || Abc_ObjIsBi(pFanin) )
+                continue;
+
             // generate the edge from this node to the next
             fprintf( pFile, "Node%d%s",  pNode->Id, (Abc_ObjIsLatch(pNode)? "_in":"") );
             fprintf( pFile, " -> " );
diff --git a/src/base/io/ioWriteList.c b/src/base/io/ioWriteList.c
index c2bea884..a92c2eff 100644
--- a/src/base/io/ioWriteList.c
+++ b/src/base/io/ioWriteList.c
@@ -19,7 +19,7 @@
 ***********************************************************************/
 
 #include "io.h"
-#include "seqInt.h"
+//#include "seqInt.h"
 
 /*
 -------- Original Message --------
@@ -159,7 +159,8 @@ void Io_WriteListEdge( FILE * pFile, Abc_Obj_t * pObj )
     {
         fprintf( pFile, " %s", Abc_ObjName(pFanout) );
         fprintf( pFile, " ([%s_to_", Abc_ObjName(pObj) );
-        fprintf( pFile, "%s] = %d)", Abc_ObjName(pFanout), Seq_ObjFanoutL(pObj, pFanout) );
+//        fprintf( pFile, "%s] = %d)", Abc_ObjName(pFanout), Seq_ObjFanoutL(pObj, pFanout) );
+        fprintf( pFile, "%s] = %d)", Abc_ObjName(pFanout), 0 );
         if ( i != Abc_ObjFanoutNum(pObj) - 1 )
             fprintf( pFile, "," );
     }
@@ -204,6 +205,83 @@ void Io_WriteListHost( FILE * pFile, Abc_Ntk_t * pNtk )
 }
 
 
+/**Function*************************************************************
+
+  Synopsis    [Writes the adjacency list for a sequential AIG.]
+
+  Description []
+  
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Io_WriteCellNet( Abc_Ntk_t * pNtk, char * pFileName )
+{
+    FILE * pFile;
+    Abc_Obj_t * pObj, * pFanout;
+    int i, k;
+
+    assert( Abc_NtkIsLogic(pNtk)  );
+
+    // start the output stream
+    pFile = fopen( pFileName, "w" );
+    if ( pFile == NULL )
+    {
+        fprintf( stdout, "Io_WriteCellNet(): Cannot open the output file \"%s\".\n", pFileName );
+        return;
+    }
+
+    fprintf( pFile, "# CellNet file for network \"%s\" written by ABC on %s\n", pNtk->pName, Extra_TimeStamp() );
+
+    // the only tricky part with writing is handling latches:
+    // each latch comes with (a) single-input latch-input node, (b) latch proper, (c) single-input latch-output node
+    // we arbitrarily decide to use the interger ID of the latch-input node to represent the latch in the file
+    // (this ID is used for both the cell and the net driven by that cell)
+
+    // write the PIs
+    Abc_NtkForEachPi( pNtk, pObj, i )
+        fprintf( pFile, "cell %d is 0\n", pObj->Id );
+    // write the POs
+    Abc_NtkForEachPo( pNtk, pObj, i )
+        fprintf( pFile, "cell %d is 1\n", pObj->Id );
+    // write the latches (use the ID of latch input)
+    Abc_NtkForEachLatch( pNtk, pObj, i )
+        fprintf( pFile, "cell %d is 2\n", Abc_ObjFanin0(pObj)->Id );
+    // write the logic nodes
+    Abc_NtkForEachNode( pNtk, pObj, i )
+        fprintf( pFile, "cell %d is %d\n", pObj->Id, 3+Abc_ObjFaninNum(pObj) );
+
+    // write the nets driven by PIs
+    Abc_NtkForEachPi( pNtk, pObj, i )
+    {
+        fprintf( pFile, "net %d  %d 0", pObj->Id, pObj->Id );
+        Abc_ObjForEachFanout( pObj, pFanout, k )
+            fprintf( pFile, "  %d %d", pFanout->Id, 1 + Abc_ObjFanoutFaninNum(pFanout, pObj) );
+        fprintf( pFile, "\n" );
+    }
+    // write the nets driven by latches
+    Abc_NtkForEachLatch( pNtk, pObj, i )
+    {
+        fprintf( pFile, "net %d  %d 0", Abc_ObjFanin0(pObj)->Id, Abc_ObjFanin0(pObj)->Id );
+        pObj = Abc_ObjFanout0(pObj);
+        Abc_ObjForEachFanout( pObj, pFanout, k )
+            fprintf( pFile, "  %d %d", pFanout->Id, 1 + Abc_ObjFanoutFaninNum(pFanout, pObj) );
+        fprintf( pFile, "\n" );
+    }
+    // write the nets driven by nodes
+    Abc_NtkForEachNode( pNtk, pObj, i )
+    {
+        fprintf( pFile, "net %d  %d 0", pObj->Id, pObj->Id );
+        Abc_ObjForEachFanout( pObj, pFanout, k )
+            fprintf( pFile, "  %d %d", pFanout->Id, 1 + Abc_ObjFanoutFaninNum(pFanout, pObj) );
+        fprintf( pFile, "\n" );
+    }
+
+    fprintf( pFile, "\n" );
+    fclose( pFile );
+}
+
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////
author	Alan Mishchenko <alanmi@berkeley.edu>	2006-11-11 08:01:00 -0800
committer	Alan Mishchenko <alanmi@berkeley.edu>	2006-11-11 08:01:00 -0800
commit	da5e0785dfb98335bd49a13bf9e86e736fb931be (patch)
tree	3e88084f64093c8394fddf2d96b522a4df183981 /src/base
parent	faf1265bb82f934cc14b6106ccce89e37203efbd (diff)
download	abc-da5e0785dfb98335bd49a13bf9e86e736fb931be.tar.gz abc-da5e0785dfb98335bd49a13bf9e86e736fb931be.tar.bz2 abc-da5e0785dfb98335bd49a13bf9e86e736fb931be.zip